The Coq mailing list

[Dan Doel <dan.doel AT gmail.com>]

On Fri, Jan 20, 2012 at 4:55 PM, Daniel Schepler 
<dschepler AT gmail.com>
 wrote:
> Actually, I guess that also gives an example of a positive, but not strictly
> positive, inductive definition which would lead to a contradiction:
>
> Inductive X : Type :=
> | X_const : ((X->Prop)->Prop) -> X.
>
> If Coq allowed that definition, then X_const, being a constructor, would
> automatically be injective, leading to the contradiction from my previous
> message.  (Plus, I'm not at all sure what X_rect or X_ind would look like in
> that case.)

I don't know Coq particularly well. Would that normally be subject to
eliminator restrictions, or not, because X : Type?

This actually reminds me of the injective type constructors discussion
(naturally). If you have impredicativity, you can prove that I in
(something like):

    Inductive X (F : Set -> Set) : Set

is not injective. So it's a problem if it is. Your diagonalization
fails in Agda for the same reason that injective type constructors
turned out to not technically be a problem there:

    data X : Set₁ where
      roll : (X → Set) → X

    module M (f : (X → Set) → X) where
      S0 : X → Set₁
      S0 t = Σ[ S ∶ (X → Set) ] (f S ≡ t) × (¬ (S t))

S0 : X -> Set1, so f S0 is not well typed.

The System F/CoC encoding, of course, won't allow you to prove
injectivity of roll. You can't even write:

    out : X -> ((X -> *) -> *)

because ((X -> *) -> *) : * fails. I don't know if Coq has comparable
elimination restrictions that would restrict this type sufficiently.

-- Dan