The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Saturday, January 21, 2012 08:29:13 AM 
roconnor AT theorem.ca
 wrote:
> On Fri, 20 Jan 2012, Daniel Schepler wrote:
> >> And your experiment substituting Prop with Type is essentially the
> >> situation in Agda. It only has the predicative hierarchy, and nothing
> >> comparable to Prop.
> > 
> > Ah, OK.  Another issue is that if you go back and replace Prop with bool
> > in the original example, then injectivity of a map ((T->bool)->bool) ->
> > T is inconsistent with the axiom "classic_dec : forall P:Prop, {P} +
> > {~P}".  The proof is pretty much the same, where you use classic_dec to
> > convert certain Props to bools.
> > 
> > I don't know whether that would be much of an issue in Agda; but in Coq,
> > I wouldn't want to lose the ability to formalize classical mathematics
> > (and have the results be meaningful instead of just following from an
> > inconsistency).
> 
> You can already formalize essentially all classical mathematics in Coq
> without using classic_dec or any other axioms via a double negation
> embedding.

Sure, plus using setoids everywhere instead of plain old types if your 
development depends on quotients, or proof irrelevance, or functional 
extensionality; with function types replaced by respectful sigma types, etc.  
And probably throw in the singleton monad if you ever use 
constructive_definite_description.  And what about if you use the axiom of 
choice?  I find all that extra overhead would just make things less clear if 
my 
target audience is classical mathematicians anyway.

As an example, I'd be interested in seeing what encoding of the basic 
classical statement "any two well-orderings are comparable" would be valid in 
axiom-free Coq.
-- 
Daniel Schepler