The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

According to the paper "Inductively Defined Types", Coq requires
*strictly* positive types because non-strictly positive types can be
used together with impredicativity to introduce a Russel-style paradox.

More specifically, the paradox goes along the lines of
[ I here work off of
  
http://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/
  rather than Coquand and Paulin(-Mohring)'s paper since that paper is
  behind a paywall.  ]

- Define `Inductive A : Type = introA : ((A → Prop) → Prop) → A`.
- Introduce an injective function `i : ∀X, X → (X → Prop)`.
- By composing `i` and `introA` we get an injective `f : (A → Prop) → A`.
- Define a suitable `P0 : A → Prop` and show that `P0 (f P0)` is both
  true and not.

In the development, the definition used for `P0` would live in Type if
it weren't for impredicativity.  Which seems like "the culprit".

But I also notice that the development defines `i` as an alias for Coq's
equality type.  But this also only works because Coq's equality type
always lives in Prop, contrary to Agda and HoTT where it would live in
Type (because it's an equality between objects that themselves live in
Type).  This is linked to the treatment of inductive type's indices
which are treated "impredicatively" in Coq but not in Agda.

Would it be possible to define an injective function from `X : Type` to
`X → Prop` if it weren't for Coq's impredicative treatment of indices?

If not, would that imply that non-strictly positive inductive types
would be safe even in the presence of Prop-style impredicativity?


        Stefan