--- Day changed Wed Jan 17 2018 | ||

Saizan | tomjack: any suggestion for some concrete example to use in a agda --cubical tutorial? | 17/01 16:53 |
---|---|---|

tomjack | hmm, Brunerie's number? ;) | 17/01 18:16 |

tomjack | really, dunno... the only example I have at the moment is this proof that the circle is homogeneous using Glue | 17/01 18:17 |

tomjack | https://www.irccloud.com/pastebin/yxATxzvR/CircleHomog.agda | 17/01 18:17 |

Saizan | cool | 17/01 18:23 |

Saizan | btw i've just added pushouts | 17/01 18:23 |

tomjack | nice, guess I will try the flattening lemma | 17/01 18:33 |

Saizan | tomjack: 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-set | 17/01 20:14 |

tomjack | Saizan: yeah, that works, it's Nat ∨ Nat | 17/01 21:48 |

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