Is CoC inconsistent with cnat_ind axiom? It is not possible to derive induction for Church-encoded datatypes on the Calculus of Constructions (source). Moreover, according to the accepted answer to another question, it is also not possible to derive induction for Church-encoded datatypes on CoIC, despite the presence of inductive datatypes. As such, I wonder if we assume induction for Church-encoded Nat, cnat_ind; that is:

cnat_ind :
  (n : CNat) -&gt;
  (P : CNat -&gt; Type) -&gt;
  (S : ∀ (n : CNat) -&gt; P n -&gt; P (csucc n)) -&gt;
  (Z : P czero) -&gt;
  P n


where CNat, csucc and czero are the usual Church-encoded Nat type and constructors, would that allow us to inhabit the empty type ∀ (P : *) -&gt; P?
One way to show that it is consistent to add cnat_ind is to internalize parametricity, i.e., we extend the type system with enough structure so that it can prove its own parametricity, from which it then follows that the Church encoding of natural numbers does indeed give natural numbers. See for instance the PhD dissertation Internalizing Parametricity by Guilhem Moulin.