The Coq mailing list

["N. Raghavendra" <raghu AT hri.res.in>]

At 2013-09-27T12:33:03+09:00, Andrej Bauer wrote:

> In ordinary mathematics (such as in Blass's paper) we have
> propositional extensionality, which says that logically equivalent
> propositions are equal.

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

> With that in hand it is easy to finish your exercise without fussing
> with quotients (although I am sure Blass has a good reason to do it
> his way, probably to stick close to set theory):

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

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

Thanks and best regards,
Raghu.

-- 
N. Raghavendra 
<raghu AT hri.res.in>,
 http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/