--- Day changed Mon Sep 11 2017
apostolisHello, if we have a Path Set A B, and then we transport an element from one type to the other, what would be the result?11/09 10:33
apostolisWould one get a function f : A -> B from univalence? and then apply it to the element? That is my guess.11/09 10:33
dolioIt depends what the path is.11/09 15:57
dolioBut yes, there are functions A -> B and B -> A.11/09 15:58
dolioThe univalence axiom says that any function A -> B that fits some criteria gives you a path, and when you transport along that path, it's supposed to apply that function.11/09 15:59
dolioWithout univalence, if you only path is 'refl', then the function is the identity function, and A must be B.11/09 16:00
dolioOh, he left. :P11/09 16:02
TanebI think I'm making what I'm trying to do difficult for myself ugh11/09 20:41
kclancyAgda emacs mode is highlighting the left-hand side of my definitions with a white background. What does this mean?11/09 23:51
kclancyI guess it means it's a catchall clause11/09 23:54
kclancyCatch all clauses might be a problem for programs, but if I'm just writing proofs then I'm guessing I can ignore it.11/09 23:55

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