The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

I don't know where propositional extensionality is used in the proof
that I'd summarised of deceq -> lem.

It doesn't. Andrej was merely suggesting a different proof of the same statement.
 

As I understand it is possible to prove deceq -> lem using setoids as
quotients, without assuming propositional extensionality.  I'll try
that.

Well, not really. You have to change the definition of deceq for the proof to pass. Replacing Coq's native equality (which is pretty meaningless in the context of setoids) with  the setoid equality. Which is essentially the same thing as proving decequiv -> lem.
 

> Another way to do this without propositional extensionality and
> without quotients is to rephrase deceq so that it says that
> equivalence relations are decidable, not just equality (if we have
> deceq and quotients then it follows that equivalence relations are
> decidable as well):

My goal is to prove deceq -> lem.  So I'll still have to prove in Coq
that deceq -> decequiv.  It looks like I'll have to use
setoids/quotients for that anyway.

Andrej's point is that deceq -> decequiv with quotients but not without. Without quotient or propositional extensionality, only decequiv -> lem is provable (essentially it is the content of Blass's proof).

The bottom line is: there is nothing special about Coq's native equality (except that it's pretty damn useful, of course). When you want to model a mathematical universe in Coq, you also have to think about how you map equality (that's also the whole idea of using setoids to model sets).


On a related note, homotopy type theory has a native notion of quotient (named higher-inductive types), although the implementations are not very stable yet. You'd be ill-advised to add deceq to homotopy type theory, though (at least not without care). The statement forall (A:Type) (x y:A), {x=y}+~{x<>y} is inconsistent (it implies that forall (A:Type) (x y:A) (p q:x=y), p=q, which is contradicted by the univalence principle). On the one hand it makes things easy to prove indeed, on the other hand, it shows quite clearly that there is nothing special about Coq's native equality.