…probably. To be clear, ECIC¹ refers to Monnier and Bos’ Erasable CIC², with erasable in the sense of erasable pure type systems (EPTS)³. I’ll argue that even with erased impredicative fields, Coquand’s paradox of trees⁴ is still typeable.

ECIC

I won’t go too much into detail on the definition of ECIC, but I’ll touch on some key rules and examples. In short, ECIC is CIC, but:

• Function arguments can be erased or normal;
• Erased arguments may only appear in type annotations that are erased prior to evaluation⁵;
• Inductives may only live in Prop;
• Large arguments of constructors must be erased; and
• There are no restrictions on what inductives may be eliminated into⁶.

They claim that erasure of large arguments is what permits unrestricted inductive elimination, but I believe that this is still inconsistent.

To establish some syntax, here’s the typing rule for function types and functions with erased arguments, where $|\cdot|$ is the erasure of a term, which erases type annotations as well as erased arguments entirely.

The PTS rules $\mathcal{R}$ are $(k, \mathsf{\textcolor{#069}{Prop}}, s, s)$, $(k, \mathsf{\textcolor{#069}{Type}}_{\ell_1}, \mathsf{\textcolor{#069}{Type}}_{\ell_2}, \mathsf{\textcolor{#069}{Type}}_{\ell_1 \sqcup \ell_2})$, and most importantly, $(\mathsf{e}, \mathsf{\textcolor{#069}{Type}}_\ell, \mathsf{\textcolor{#069}{Prop}}, \mathsf{\textcolor{#069}{Prop}})$. The last rule says that if you want to use something large for a proposition, it must be erasable, and therefore only used in type annotations. A key theorem states that if a term is typeable is CIC, then it’s typeable in ECIC with additional erasure annotations, meaning that CIC inherently never uses impredicativity in computationally relevant ways.

The typing rules for inductives and especially their case expressions, as usual, are rather involved, and I won’t repeat them here. Instead, to establish its syntax, here’s an example defining propositional equality as an inductive, and a proof that it’s symmetric. From here onwards I’ll use square brackets to indicate erased arguments, omitting annotations entirely, as well as $\cdot \to \cdot$ as a shorthand for nondependent function types.

This equality is over large terms to be able to talk about both equal propositions and equal proofs⁷, so basically all arguments except for equality itself must be erased. However, it still doesn’t qualify as a large inductive, since none of the constructor arguments are large, i.g. have types in sort $\mathsf{\textcolor{#069}{Type}}$. Contrariwise, the following inductive is large, requiring its first constructor argument to be erased to justify unrestricted elimination.

Digression: Rocq’s $\mathsf{\textcolor{#069}{Prop}}$ and $\mathsf{\textcolor{#069}{Set}}$

ECIC’s $\mathsf{\textcolor{#069}{Prop}}$ is neither like Rocq’s $\mathsf{\textcolor{#069}{Prop}}$ nor like its impredicative $\mathsf{\textcolor{#069}{Set}}$, which I’ll call $\mathsf{\textcolor{#069}{rProp}}$ and $\mathsf{\textcolor{#069}{rSet}}$ to avoid confusion. Large inductives in either $\mathsf{\textcolor{#069}{rProp}}$ and $\mathsf{\textcolor{#069}{rSet}}$ are not allowed to be strongly eliminated, because this would be inconsistent. Furthermore, as members of types of sort $\mathsf{\textcolor{#069}{rProp}}$ are intended to be erased during extraction, inductives in $\mathsf{\textcolor{#069}{rProp}}$ with multiple constructors can’t be strongly eliminated either, so that case expressions only have a single branch to which they erase. This makes eCIC’s $\mathsf{\textcolor{#069}{Prop}}$, confusingly, exactly Rocq’s impredicative $\mathsf{\textcolor{#069}{Set}}$.

The paradox of trees

Coquand’s paradox of trees develops an inconsistency out of the inductive $\mathsf{\textcolor{#bf616a}{U}}$ above by showing that simultaneously all $\mathsf{\textcolor{#bf616a}{U}}$ are well founded and there exists a $\mathsf{\textcolor{#bf616a}{U}}$ that is not well founded, in particular $\mathsf{\textcolor{#bf616a}{loop}}$ below.

$\mathsf{\textcolor{#bf616a}{U}}$ is injective

Before we continue, we need an injectivity lemma saying that if two $\mathsf{\textcolor{#bf616a}{U}}$s are equal, then their components are equal too. I omit the $\mathsf{\textcolor{#069}{return}}$ expression in the body because it’s already in the type. Importantly, when matching on the $\mathsf{\textcolor{#bf616a}{U}}$s, the large, erased first argument of the constructor is only used in erased positions.

The equalities make its statement a bit convoluted, but the proof is ultimately a pair of reflexivities. It would perhaps be clearer to see the equivalent Rocq proof, which uses rew notations to make it cleaner. Here, I need to turn off universe checking when defining the inductive to prevent Rocq from disallowing its strong elimination. Notably, this is the only place where turning off universe checking is required, and the type of $\mathsf{\textcolor{#bf616a}{injU}}$ is the only place where strong elimination occurs.

Import EqNotations.

Unset Universe Checking.
Inductive U : Prop := u (X : Prop) (f : X -> U) : U.
Set Universe Checking.

Definition loop : U := u U (fun x => x).

Definition injU [u1 u2 : U] (p : u1 = u2) :
  match u1, u2 with
  | u X1 f1, u X2 f2 =>
    exists (q : X1 = X2),
      rew [fun Z => Z -> U] q in f1 = f2
  end :=
  rew dependent p in
  match u1 with
  | u _ _ => ex_intro _ eq_refl eq_refl
  end.

$\mathsf{\textcolor{#bf616a}{U}}$s are well founded

The wellfoundedness predicate is another inductive stating that a $\mathsf{\textcolor{#bf616a}{U}}$ is well founded if all of its children are. Wellfoundedness for all $\mathsf{\textcolor{#bf616a}{U}}$ is easily proven by induction.

Again, here’s the equivalent definitions in Rocq. There’s no need to turn off universe checking this time since we won’t be strongly eliminating $\mathsf{\textcolor{#bf616a}{WF}}$.

Inductive WF : U -> Prop :=
| wf : forall X f, (forall x, WF (f x)) -> WF (u X f).

Fixpoint wfU (u : U) : WF u :=
  match u with
  | u X f => wf X f (fun x => wfU (f x))
  end.

$\mathsf{\textcolor{#bf616a}{loop}}$ is not well founded

Showing nonwellfoundedness of $\mathsf{\textcolor{#bf616a}{loop}}$ is more complicated, not because it’s an inherently difficult proof, but because it requires manually unifying indices. In fact, the whole proof in Agda is quite simple.

{-# NO_UNIVERSE_CHECK #-}
data U : Set where
  u : (X : Set) → (X → U) → U

data WF : U → Set₁ where
  wf : ∀ (X : Set) (f : X → U) → (∀ x → WF (f x)) → WF (u X f)

loop = u U (λ x → x)

nwf : WF loop → ⊥
nwf (wf X f h) = nwf (h loop)

Destructing $\mathsf{\textcolor{#bf616a}{WF}} \; \mathsf{\textcolor{#bf616a}{loop}}$ as $\mathsf{\textcolor{#bf616a}{WF}} \; [X] \; f \; h$, we know that $X$ is $\mathsf{\textcolor{#bf616a}{U}}$ and $f$ is $\lambda x : \mathsf{\textcolor{#bf616a}{U}}. x$. In Rocq, we have the help of tactics and dependent induction, as well as $\mathsf{\textcolor{#bf616a}{injU}}$ proven earlier to explicitly unify indices.

Require Import Coq.Program.Equality.
Lemma nwf (u : U) (p : u = loop) (wfl : WF u) : False.
Proof.
  dependent induction wfl.
  apply injU in p as [q r].
  simpl in q. subst.
  simpl in r. subst.
  eapply H0. reflexivity.
Qed.

But writing the same proof in plain ECIC is a challenge, especially as the proof term generated for nwf is disgusting. I’ve simplified it to the following to the best of my ability, still using copious amounts of rew.

Fixpoint nwf (wfl : WF loop) : False :=
  match wfl in WF u' return loop = u' -> False with
  | wf _ f h => fun p => let (q , r) := injU p in
    (rew dependent [fun _ q => forall f,
      rew [fun Z => Z -> U] q in (fun x => x) = f
      -> (forall x, WF (f x))
      -> False] q
    in fun _ r =>
      rew [fun f => (forall x, WF (f x)) -> False] r
      in fun h => nwf (h loop)) f r h
  end eq_refl.

I won’t bother trying to typeset that in ECIC, but I hope it’s convincing enough as an argument that the corresponding definition would still type check and that erasure isn’t violated, i.e. that the $\mathsf{\textcolor{#069}{Prop}}$ argument from the $\mathsf{\textcolor{#bf616a}{WF}}$ isn’t used in the body of the proof. This proof doesn’t even use strong elimination, either: the return type of every case expression lives in $\mathsf{\textcolor{#069}{Prop}}$.

Why isn’t ECIC consistent?

The proof sketch above tells us how ECIC isn’t consistent, but we still need to understand why it isn’t consistent. ECIC’s original argument was that

forcing impredicative fields to be erasable also avoids this source of inconsistency usually avoided with the $\Gamma \vdash e \; \mathsf{small}$ constraint.

Said source refers to the ability for large impredicative inductives with strong elimination to hide a larger type within a smaller construction that’s then used later. The idea is that if the impredicative field is erased, then surely it can’t be meaningfully used later as usual to construct an inconsistency. Here, I’ve shown that it can be meaningfully used even if it can’t be used relevantly, because all we need is to be able to refer to them in propositions and proofs. It doesn’t really make sense anyway that the computational relevance of a term should have any influence on propositions, which arguably exist independently of whether they can be computed.

Then why is strong elimination inconsistent with impredicativity, if computational relevance isn’t the reason? I believe that the real connection is between impredicativity and proof irrelevance, from which computational irrelevance arises. After all, $\mathsf{\textcolor{#069}{Prop}}$ is often modelled proof-irrelevantly as a two-element set $\{ \top , \bot \}$, collapsing all of its types to truthhood or falsehood and disregarding those types’ inhabitants. Other times, $\mathsf{\textcolor{#069}{Prop}}$ is defined as the universe of mere propositions, or the universe of types such that their inhabitants (if any) are all propositionally equal.

Under this view, impredicativity is permitted, although not necessary, because referring to larger information ought to be safe so long as there’s no way to use that information to violate proof irrelevance. Strong elimination commits this violation because, as seen in $\mathsf{\textcolor{#bf616a}{injU}}$, it allows us to talk about the identity (or non-identity) of larger terms, even if the way we talk about it is proof-irrelevantly. Concretely, the contrapositive of $\mathsf{\textcolor{#bf616a}{injU}}$ lets us distinguish two $\mathsf{\textcolor{#bf616a}{U}}$s as soon as we have two provably unequal types, such as $\top$ and $\bot$, from which we can provably distinguish $\mathsf{\textcolor{#069}{Con}}(0, \mathsf{\textcolor{#bf616a}{U}}) \; [\top] \; (\lambda \_. \mathsf{\textcolor{#bf616a}{loop}})$ and $\mathsf{\textcolor{#069}{Con}}(0, \mathsf{\textcolor{#bf616a}{U}}) \; [\bot] \; (\lambda b. \mathsf{\textcolor{#069}{Case}} \; b \; \mathsf{\textcolor{#069}{of}} \; \langle \rangle)$.

Interestingly, even without strong elimination of large inductives, proof irrelevance can still be violated by strong elimination of a small inductive with two constructors, since that would enable proving the two constructors unequal. The only way an inconsistency arises is if proof irrelevance is explicitly internalized. This is why the axiom of excluded middle is inconsistent in the presence of strong elimination in this setting: Berardi’s paradox⁸ says that EM implies proof irrelevance. I think there’s something profound in this paradox that I haven’t yet grasped, because connects two different views of a proposition: as something that is definitively either true or false, or as something that carries no other information than whether it is true or false.