[Agda] Equivalence axiom => extensionality

[Thorsten Altenkirch]

Hi Dan,

thank you for this clear explanation.

Indeed, for finite sets weak equivalence (i.e. a bijection) is the same as isomorphism. And as you say if you identify all isomorphisms on Bool you are in trouble. 

An alternative to "weak equivalence" would be isomorphism. Certainly isomorphism implies weak equivalence but not vice versa (for infinite sets). Does the proof of extensionality rely on using weak equivalence or would it work for isomorphism as well?

What are weak counterexamples for sets that are weakly equivalent but not provably isomorphic?

To me weak equivalence looks very classical. I am a bit puzzled that this should be the right notion for equality of sets.

Cheers,
Thorsten


On 21 Jun 2010, at 16:56, Dan Licata wrote:

> On Jun21, Thorsten Altenkirch wrote:
>> Hi Dan,
>> 
>> thank you for your reply. Could you explain why the equivalence axiom
>> implies not UIP?
> 
> (1) The equivalence axiom states that weak equivalence is weakly
>    equivalent to identity.  As a corollary weak equiv. and identity
>    are interprovable.  Therefore we can substitute (WEq x y) for (Id
>    x y) in any context.
> (2) Identity has UIP. By substituting weak equivalence for identity
>    in this theorem, all proofs of weak equivalence are identical.  
> (3) There are two computationally different proofs of weak
>    equivalence between bool and itself, the identity and negation.
> (4) But by (2) these two proofs are identical. 
>    Therefore (\x -> x) = not, from which we get a contradiction.
> 
>> I think there were some sheds unfilled in your agda file. Do you have
>> a complete proof for the above result?
> 
> Yes, I've updated the code with a simplified and fully filled in
> version:
> http://www.cs.cmu.edu/~drl/tmp/equivax.tgz
> 
> It does still use --type-in-type just to state the equivalence axiom,
> but I conjecture that you could sort out the universe levels instead
> (Voevodsky's Coq code does this).  The reason this comes up is that the
> equivalence axiom is stated as a weak equivalence between weak
> equivalence and identity, and identity of Sets is a Set1.
> 
>> 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.
> 
> That makes sense. It's just a shame that there is no way to force
> yourself not to use such pattern matching.  
> 
> -Dan
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda