[Agda] Equivalence axiom => extensionality

[Dan Licata]

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