[Agda] universe with extensional propositional equality?

[Peter Morris]

I wasn't there, but it seems that Thorsten posted this on the fplunch blog,
which contains the relevant 'decode', here called 'fapp':

http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=98

Peter

2009/4/8 Peter Morris <morrispwj at gmail.com>

> 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<http://www.cs.nott.ac.uk/%7Etxa/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/be7521e8/attachment.html