<p>One way to show that it is consistent to add <code>cnat_ind</code> 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 <a href="https://research.chalmers.se/publication/235758" rel="noreferrer">Internalizing Parametricity</a> by Guilhem Moulin.</p>

CC BY-SA 4.0
2019-01-24T16:01:36.543Z
Is there by chance any simplified implementation of this proposal available? I was following along until the part of hypercubes and so on. The notation from page 31 onwards is kinda cryptic...
MaiaVictor
CC BY-SA 4.0
2019-01-25T08:08:32.330Z
I don't know about "implementation" but you could try the corresponding paper [A Presheaf Model of Parametric Type Theory](https://publications.lib.chalmers.se/records/fulltext/230735/local_230735.pdf).
Andrej Bauer
CC BY-SA 4.0
2019-01-24T07:32:20.907Z
2019-01-24T07:32:20.907Z
Andrej Bauer
<p>It is not possible to derive induction for Church-encoded datatypes on the Calculus of Constructions (<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.4355" rel="noreferrer">source</a>). Moreover, according to the accepted answer to <a href="https://stackoverflow.com/questions/48233736/is-it-possible-to-derive-induction-for-the-church-encoded-nat">another question</a>, 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, <code>cnat_ind</code>; that is:</p>

<pre><code>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
</code></pre>

<p>where <code>CNat</code>, <code>csucc</code> and <code>czero</code> are the usual Church-encoded Nat type and constructors, would that allow us to inhabit the empty type <code>∀ (P : *) -&gt; P</code>?</p>

CC BY-SA 4.0
2019-02-03T19:25:20.453Z
Probably worth noting that `cnat_ind` is inhabited in the "simple" proof-irrelevant model (where `cnat` only has one inhabitant. This gives a simple proof of consistency, but is a little usatisfying, since we also would like this to hold in the presence of `czero =/= (csucc czero)` (or some large elimination axiom).
cody
<type-theory><calculus-of-constructions>
Is CoC inconsistent with cnat_ind axiom?
MaiaVictor
# Is CoC inconsistent with cnat_ind axiom?

(Asked by: username_0 on 2019-01-23)

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) ->
  (P : CNat -> Type) ->
  (S : ∀ (n : CNat) -> P n -> P (csucc n)) ->
  (Z : P czero) ->
  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 : *) -> P?

**Tags:** type-theory, calculus-of-constructions

> **Comments:**
> **username_1**: Probably worth noting that `cnat_ind` is inhabited in the "simple" proof-irrelevant model (where `cnat` only has one inhabitant. This gives a simple proof of consistency, but is a little usatisfying, since we also would like this to hold in the presence of `czero =/= (csucc czero)` (or some large elimination axiom).  

---

## 1 answers

### Answer by username_2 on 2019-01-24. Score: 10 | Accepted answer

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](https://research.chalmers.se/publication/235758) by Guilhem Moulin.

> **Comments:**
> **username_0**: Is there by chance any simplified implementation of this proposal available? I was following along until the part of hypercubes and so on. The notation from page 31 onwards is kinda cryptic...  
> **username_2**: I don't know about "implementation" but you could try the corresponding paper [A Presheaf Model of Parametric Type Theory](https://publications.lib.chalmers.se/records/fulltext/230735/local_230735.pdf).  

---

