If you look around for why inductive datatypes need to be strictly positive, you’ll probably end up at Vilhelm Sjöberg’s blog post Why must inductive types be strictly positive?, which gets passed around a lot as an accessible and modernized description of the inconsistency that arises from a certain large, impredicative inductive datatype that is positive but not strictly positive. This example originally comes from Coquand and Paulin-Mohring’s COLOG-88 paper Inductively defined types. A key component of the inconsistency relies on the injectivity of its constructor, but since the inductive is large, even if Rocq were to permit nonstrictly positive inductives, it would still disallow its strong elimination and therefore injectivity!

The datatype in question is the following, which I’ll continue to write in Rocq.

Inductive A : Prop := an : {_ : (A → Prop) → Prop}.

Set-theoretically, X → Prop for some set X is interpreted as the powerset of X, as the set of propositions Prop may as well be interpreted as a two-element set of truthhood and falsehood, with a particular subset of X (i.e. an element of the powerset) f : X → Prop returning true if an element of X is in it and false if not.

Supposing that A were instead in Type and therefore something that behaves set-like, injectivity of inductive datatype constructors tells us that there is a bijection between A and (A → Prop) → Prop, meaning that A as a set has the same size as its double powerset — clearly set-theoretically invalid! Here’s how you can show that injectivity.

Definition projA (a : A) : (A → Prop) → Prop :=
match a return (A → Prop) → Prop with
| an x => x
end.

Definition injA x y (p : an x = an y) : x = y :=
match p in _ = a return x = projA a with
| eq_refl => eq_refl
end.

Ignoring nonstrict positivity issues, proving injectivity relies on being able to project out the constructor argument in (A -> Prop) -> Prop. Notably, its type is Type, so if we put A back in Prop, it’s said to be large, or that the constructor has an impredicative argument. We then wouldn’t be able to define the projection, because the match expression on the A returns something in a type larger than A, which Rocq disallows¹. Indeed, we would get the following error:

Incorrect elimination of “a” in the inductive type “A”:
the return type has sort “Type” while it should be “SProp” or “Prop”.
Elimination of an inductive object of sort Prop is not allowed on a predicate in sort Type
because proofs can be eliminated only to build proofs.

Trying to trick Rocq by using pattern-matching in the extended match syntax won’t work either. Indices in the in clause can be written as constructor patterns, but they desugar to explicit match expressions in the return clause. The following yields the same elimination error message (although confusingly it refers to generated variable names).

Definition injA x y (p : an x = an y) : x = y :=
match p in _ = an z return x = z with
| eq_refl => eq_refl
end.

Therefore, even if Rocq were to allow nonstrictly positive impredicative inductives, its other existing feature of disallowing strong elimination of large impredicative inductives would prevent the paradox from going through. I therefore conjecture that any impredicative inductive can be nonstrictly positive, so long as the elimination restriction on large inductives continues to hold.

Predicative inductives, however, may not be nonstrictly positive in the presence of Prop. If we change the universe of A from Prop to Type, the projection and therefore the injectivity of A is definable. Proceeding with the rest of the paradox does require impredicativity, so a type theory without impredicativity may permit nonstrictly positive inductives, but otherwise it can’t be allowed in Rocq.

Here’s the paradox in full, again using pattern-matching indices in the match. With an A in Prop, injf will fail with an elimination error, as expected.

Require Import Coq.Unicode.Utf8_core.

Unset Positivity Checking.
Inductive A : Type := an {_: (A → Prop) → Prop}.
Set Positivity Checking.

Definition f (p : A → Prop) : A := an (λ q, q = p).

Definition injf [p q] (r : f p = f q) : p = q :=
  match r in _ = an g return g p with
  | eq_refl => eq_refl
  end.

Definition P₀ (x : A) : Prop := ∃ (P : A → Prop), x = f P ∧ ¬ (P x).
Definition x₀ : A := f P₀.

Definition notP₀x₀ (P₀x₀ : P₀ x₀) : False :=
  match P₀x₀ with
  | ex_intro _ _ (conj fP₀fP notPx₀) =>
    notPx₀ (match injf fP₀fP with eq_refl => P₀x₀ end)
  end.

Definition false : False :=
  notP₀x₀ (ex_intro _ P₀ (conj eq_refl notP₀x₀)).

Impredicativity is needed to define P₀ in Prop (since it contains an existential predicate) so that it can be applied to f. P₀ is a predicate that expresses some notion of a set not containing itself, and x₀ is a set that simultaneously does and does not contain itself, hence the contradiction.

I don’t have a concrete explanation for why these combinations of features are consistent or inconsistent, but I believe the intuition is that types in Type (and Set) are intended to behave like sets, and a Prop universe permits predicates that allow manipulating those types as if they internally behave like sets. Meanwhile, types in Prop aren’t intended to be set-like at all, which aligns with the impredicativity of System F also not being set-theoretic.