The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Friday, January 20, 2012 06:14:32 PM Dan Doel wrote:
> On Fri, Jan 20, 2012 at 8:00 PM, Daniel Schepler 
> <dschepler AT gmail.com>
>  
wrote:
> > I probably know even less about Agda than you do about Coq, so I'm not
> > sure I understand the question, or all the details of what you were
> > saying below.  The only eliminator restrictions in Coq, afaik, are that
> > you can't eliminate most Props unless the result is also a Prop (notable
> > exceptions being eq and Acc).
> 
> That's the kind of thing I mean. There's another restriction when
> --impredicative-set is on that circumvents the fact that strong
> impredicative sums (and therefore impredicative inductive types) are
> inconsistent. The restriction prevents you from projecting out the
> large parts, at least usefully.
> 
> Prop isn't large compared to Type, though, so I don't think that
> restriction would matter here.
> 
> 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).  
But then, I guess it's fairly well-known that classic mathematics is 
inconsistent with an impredicative type system, at least if you want to be 
able to have "constructor discrimination".
-- 
Daniel Schepler