[Agda] universe with extensional propositional equality?

[Peter Morris]

Hi,

2009/4/8 Wouter Swierstra <wss at cs.nott.ac.uk>

>
> I think there may be something about this decode function in the lecture
> notes Peter Morris, Conor McBride, and Thorsten Altenkirch wrote for a
> Spring School on Generic Programming. A quick web search didn't turn up the
> document I had in mind, so I may be mistaken.
>
>
No, you are right, the notes are here:
http://www.cs.nott.ac.uk/~txa/publ/ssgp06.pdf and the relevant part is in
section 3. The 'decode' view is actually left as (a somewhat nasty)
exercise, though.

I had an agda file with this stuff in a one point, I'll see if I can dig it
up..

Peter
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090408/ca246b17/attachment.html