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.