<p>Yes, it's consistent. Probably the easiest account is in my 2013 CSL paper with Derek Dreyer, <a href="https://www.cl.cam.ac.uk/~nk480/final-csl-internalizing-parametricity.pdf" rel="noreferrer"><em>Internalizing Parametricity in the Extensional Calculus of Construction</em></a>, which is all about adding this style of parametricity axiom to the CoC.</p>

CC BY-SA 4.0
2020-03-19T14:38:36.293Z
Thanks! That's good to know. I had a small question about that paper: at the end of 5.3 it says "Details are given in the appendix.", but I am unable to find these details in the appendix.
Labbekak
CC BY-SA 4.0
2020-03-19T13:54:23.817Z
2020-03-19T13:54:23.817Z
Neel Krishnaswami
<p>If we start with the Calculus of Constructions, and then use the following definitions for the Church-encoded Unit:</p>

<pre><code>UnitType = (t : *) -&gt; t -&gt; t
Unit = \(t : *) (x : t). x
</code></pre>

<p>And the add the following construct <code>indUnit</code>:</p>

<pre><code>G |- P : UnitType -&gt; *
G |- pu : P Unit
G |- u : UnitType
--------------
G |- indUnit P pu u : P u
</code></pre>

<p>With reduction rule:</p>

<pre><code>indUnit P pu Unit ~&gt; pu
</code></pre>

<p>Basically this adds induction over the Church-encoded unit type.</p>

<ol>
<li>Is this consistent?</li>
<li>If we change the reduction rule to:</li>
</ol>

<pre><code>indUnit P pu x ~&gt; x (P x) pu (if x is a closed term)
</code></pre>

<p>Is it still consistent?</p>

<p>It seems to me that this is consistent.</p>

<type-theory><calculus-of-constructions>
Church-style CoC with axiom for induction over Church-encoded unit, is it consistent?
Labbekak
# Church-style CoC with axiom for induction over Church-encoded unit, is it consistent?

(Asked by: username_0 on 2020-03-19)

If we start with the Calculus of Constructions, and then use the following definitions for the Church-encoded Unit:
UnitType = (t : *) -> t -> t
Unit = \(t : *) (x : t). x

And the add the following construct indUnit:
G |- P : UnitType -> *
G |- pu : P Unit
G |- u : UnitType
--------------
G |- indUnit P pu u : P u

With reduction rule:
indUnit P pu Unit ~> pu

Basically this adds induction over the Church-encoded unit type.

Is this consistent?
If we change the reduction rule to:

indUnit P pu x ~> x (P x) pu (if x is a closed term)

Is it still consistent?
It seems to me that this is consistent.

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


---

## 1 answers

### Answer by username_1 on 2020-03-19. Score: 7 | Accepted answer

Yes, it's consistent. Probably the easiest account is in my 2013 CSL paper with Derek Dreyer, [*Internalizing Parametricity in the Extensional Calculus of Construction*](https://www.cl.cam.ac.uk/~nk480/final-csl-internalizing-parametricity.pdf), which is all about adding this style of parametricity axiom to the CoC.

> **Comments:**
> **username_0**: Thanks! That's good to know. I had a small question about that paper: at the end of 5.3 it says "Details are given in the appendix.", but I am unable to find these details in the appendix.  

---

