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 PaulinMohring’s COLOG88 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}.
Settheoretically, 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 twoelement 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 setlike,
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 settheoretically 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^{1}. 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 patternmatching 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 patternmatching 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 setlike at all,
which aligns with the impredicativity of System F also not being settheoretic.

This disallowed elimination, known as strong elimination of large inductives, can itself yield an inconsistency even without nonstrict positivity; see, for instance, Coquand’s paradox of trees. ↩