[Agda] Equivalence axiom => extensionality

[Thorsten Altenkirch]

Hi Dan,

thank you for your reply. Could you explain why the equivalence axiom implies not UIP? 

I think there were some sheds unfilled in your agda file. Do you have a complete proof for the above result? 

If you don't want to assume UIP this means that you just shouldn't use pattern matching on equality proofs (and actually not for any non-linear inductive family over a potentially undecidable indexing type) but only use J.

Cheers,
Thorsten

On 16 Jun 2010, at 18:57, Dan Licata wrote:

> 
> 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