--- Day changed Wed Jan 17 2018
Saizantomjack: any suggestion for some concrete example to use in a agda --cubical tutorial?17/01 16:53
tomjackhmm, Brunerie's number? ;)17/01 18:16
tomjackreally, dunno... the only example I have at the moment is this proof that the circle is homogeneous using Glue17/01 18:17
tomjackhttps://www.irccloud.com/pastebin/yxATxzvR/CircleHomog.agda17/01 18:17
Saizancool17/01 18:23
Saizanbtw i've just added pushouts17/01 18:23
tomjacknice, guess I will try the flattening lemma17/01 18:33
Saizantomjack: do you know if we can build the integers as the pushout of f g : Unit -> Nat, where f = g = \ _ -> 0 ? I'm afraid we might get something that's not an h-set17/01 20:14
tomjackSaizan: yeah, that works, it's Nat ∨ Nat17/01 21:48

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!