The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Fri, Jan 20, 2012 at 11:43 AM, Dan Doel <dan.doel AT gmail.com> wrote:

I think the main reason positive-but-not-strictly types are rejected
is that they aren't set theoretic in general. That is, you can
construct types such that:

   T ~ (T -> 2) -> 2

but there is no such set. So if you're committed to your models being
set theoretic, you can't have such types (this is, I think, the
same/similar observation as Reynolds' original paper on models of
polymorphic type theory in sets).

Replace 2 with Prop, and the existence of such a type T is inconsistent.  First, no function f : P(T) -> T can be injective, by the following variation of Cantor diagonalization: consider S0 = { f(S) : ~(f(S) in S) } = { t:T | exists S:P(T), f(S) = t /\ ~ (t in S) }.  Then f(S0) in S0 -> exists S, f(S) = f(S0) /\ ~ (f(S0) in S).  By the injectivity of f, this implies a contradiction ~(f(S0) in S0); so overall, we know ~(f(S0) in S0).  But then f(S0) in S0 because f(S0) = f(S0) /\ ~ (f(S0) in S0).  So the assumption that f is injective leads to a contradiction.

Now if we have an injective map ((T -> Prop) -> Prop) -> T, which must exist if T ~ (T -> Prop) -> Prop, then @eq (T -> Prop) : (T -> Prop) -> ((T -> Prop) -> Prop) is also injective; so the composition : (T -> Prop) -> T is injective, contradicting the previous paragraph.
--
Daniel Schepler