[Agda] Unification of function types
Jesper at sikanda.be
Sat Sep 21 00:54:35 CEST 2013
Thank you for your answers.
I did not realize that I needed to enable injective type constructors,
thanks Andreas for pointing that out. Also I now feel very stupid for the
mistake in the equal-types code :$
When you look at the problem from a HoTT perspective (with univalence),
then indeed it doesn't seem right to have injectivity of type constructors,
or of -> for that matter. I guess I can live with the extra argument to my
cong function if it's necessary to bring the magic of HoTT to Agda.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda