[Agda] Equivalence axiom => extensionality

[Thorsten Altenkirch]

Hi,

Vladimir Voevodsky has shown that his "equivalence axiom" implies  
extensionality and has formalized this in Coq (modulo some problems  
with universe polymorphism) - see
http://www.math.ias.edu/~vladimir/Site3/home_files/2010_3_3_foundations_post.v
It is roughly saying that equality of sets is bijective to the  
existence of a bijection between the sets.

Attached you find a formalisation in Agda - it would be interesting to  
reprove and maybe simplify the construction. The proof should only use  
J for equality types (not general pattern matching or K).

Cheers,
Thorsten & Thierry

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Equivalence.agda
Type: application/octet-stream
Size: 1108 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100616/708a8e2c/Equivalence.obj
-------------- next part --------------