[Agda] Equivalence axiom => extensionality

[Dan Licata]

On Jun16, Thorsten Altenkirch wrote:
> 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).

It is quite important to only use J, as the equivalence axiom is
inconsistent if you also have uniqueness of identity proofs.  This
shouldn't be surprising: the equivalence axiom lets you use isomorphisms
as equalities, and UIP says that all equalities are themselves equal.
But of course you can tell different isomorphisms apart by applying them
and seeing what they do.

When Voevodsky was visiting CMU this winter, I transcribed a little of
his Coq code into Agda (you can find it here:
http://www.cs.cmu.edu/~drl/tmp/equivax.tgz ).  The code just transcribes
the basic definitions, and then gets a contradiction from UIP.  I
started off by postulating a type of 'Paths' with just refl and J,
knowing that I didn't want pattern-matching because of UIP, and thinking
that this would save me.  However, this postulated identity type ends up
being interprovable with standard propositional equality, so it
satisifies UIP anyway, even though you don't want it to.

-Dan