[Agda] Unification of function types

Jesper Cockx 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.

Best regards,
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130921/873c1ab9/attachment.html

More information about the Agda mailing list