[Agda] universe with extensional propositional equality?

[Wouter Swierstra]

Hi Dan,

> However, I can't seem to prove that this notion of equality is
> reflexive:

In this particular case, I think you can manage to prove reflexivity  
in Agda. I haven't completed the definition, but let me sketch why I  
think it's possible.

Instead of interpreting your types as a Set, you could write:

count : Tp -> Nat
count bool = 2
count (A ⊃ B) = count B ^ count A

el : Tp -> Set
el u = Fin (count u)

You can certainly decide when two elements of Fin n are equal (and  
this equality is reflexive). It's still a bit of a challenge to write  
the function:

decode : Fin (n ^ m) -> Fin m -> Fin n

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.

Of course this doesn't work if you had added Nat to the universe  
instead of Bool. Does this answer your question?

   Wouter