[Agda] Polymorphism is not (always) naturality

Andrea Vezzosi sanzhiyan at gmail.com
Tue Oct 6 15:42:47 CEST 2015


On Tue, Oct 6, 2015 at 3:14 PM, effectfully <effectfully at gmail.com> wrote:
> Is this related?
>
> https://personal.cis.strath.ac.uk/conor.mcbride/NoYo.agda

Yes, there it's the naturality of com that fails and so the yoneda
isomorphism with it.


More information about the Agda mailing list