[Agda] Unification of function types

[Jesper Cockx]

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,
Jesper
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130921/873c1ab9/attachment.html