<p>Consider the Church encoding of booleans in CoC
<span class="math-container">$$
Bool := \forall t : * . t \to t \to t \\
T := \lambda t : * . \lambda x : t . \lambda y : t . x \\
F := \lambda t : * . \lambda x: t . \lambda y : t . y \\
$$</span>
and the following terms:
<span class="math-container">$$
A := (\lambda t : * . \lambda x : t . x \ Bool) \\
B := \lambda b : Bool . b \\
C := \lambda b : Bool . (b \ Bool \ T \ F) \\
D := \lambda b : Bool . \lambda t : * . \lambda x : t . \lambda y : t . (b \ t \ x \ y)
$$</span>
We can see that they essentially refer to the same thing. Additionally, we have
<span class="math-container">$$
A \to_\beta B \\
D \to_\eta^* B \textit{ or }B \to_\tilde{\eta}^* D \\
$$</span>
But as far as I know we can only relate <span class="math-container">$C$</span> to the others in the meta theory. Now, my idea is that we could try to formulate a conversion rule (I'll call it <span class="math-container">$\tau$</span> for now, because it concerns the handling of types), which would give <span class="math-container">$C \to_\tau D$</span> either directly or by also using <span class="math-container">$\beta\eta$</span> steps. The way this can make sense is by noticing that in <span class="math-container">$C$</span> we apply <span class="math-container">$b$</span> to the <span class="math-container">$Bool$</span> type and then two values of that type, whereas in <span class="math-container">$D$</span> we destructure the <span class="math-container">$Bool$</span> type first, so that <span class="math-container">$b$</span> can be applied to the type variable <span class="math-container">$t$</span> instead, and the values <span class="math-container">$T$</span> and <span class="math-container">$F$</span> are replaced by <span class="math-container">$x$</span> and <span class="math-container">$y$</span>, which could be obtained in a more generic way for example as <span class="math-container">$(T \ t \ x \ y)$</span> and <span class="math-container">$(F \ t \ x \ y)$</span>, respectively.</p>
<p>For example this works also for the case of a function <span class="math-container">$Bool \to Nat$</span>
<span class="math-container">$$
\lambda b : Bool . (b \ Nat \ 0 \ 1) \to_\tau \lambda b : Bool . \lambda t : * . \lambda s : t \to t . \lambda z : t . (b \ t \ (0 \ t \ s \ z) \ (1 \ t \ s \ z)) \\
\to_\beta^* \lambda b : Bool . \lambda t : * . \lambda s : t \to t . \lambda z : t . (b \ t \ z \ (s z))
$$</span></p>
<p>Can this be formalized for the general case to obtain a new conversion rule for CoC? Has something like this been done already?</p>

CC BY-SA 4.0
2021-12-04T09:44:23.987Z
Lookup systems with "internal parametricity", there you can prove these things internally.
Labbekak
CC BY-SA 4.0
2021-12-05T21:43:17.697Z
Thank you. It's a line of research that I had not seen before and it seems indeed relevant for my question, and also very interesting in general.
Cristian Gratie
<type-systems><calculus-of-constructions>
Can this be formalized as a conversion rule for CoC?
Cristian Gratie
# Can this be formalized as a conversion rule for CoC?

(Asked by: username_0 on 2021-12-03)

Consider the Church encoding of booleans in CoC
$$
Bool := \forall t : \* . t \to t \to t \\
T := \lambda t : \* . \lambda x : t . \lambda y : t . x \\
F := \lambda t : \* . \lambda x: t . \lambda y : t . y \\
$$
and the following terms:
$$
A := (\lambda t : \* . \lambda x : t . x \ Bool) \\
B := \lambda b : Bool . b \\
C := \lambda b : Bool . (b \ Bool \ T \ F) \\
D := \lambda b : Bool . \lambda t : \* . \lambda x : t . \lambda y : t . (b \ t \ x \ y)
$$
We can see that they essentially refer to the same thing. Additionally, we have
$$
A \to\_\beta B \\
D \to\_\eta^\* B \textit{ or }B \to\_\tilde{\eta}^\* D \\
$$
But as far as I know we can only relate $C$ to the others in the meta theory. Now, my idea is that we could try to formulate a conversion rule (I'll call it $\tau$ for now, because it concerns the handling of types), which would give $C \to\_\tau D$ either directly or by also using $\beta\eta$ steps. The way this can make sense is by noticing that in $C$ we apply $b$ to the $Bool$ type and then two values of that type, whereas in $D$ we destructure the $Bool$ type first, so that $b$ can be applied to the type variable $t$ instead, and the values $T$ and $F$ are replaced by $x$ and $y$, which could be obtained in a more generic way for example as $(T \ t \ x \ y)$ and $(F \ t \ x \ y)$, respectively.

For example this works also for the case of a function $Bool \to Nat$
$$
\lambda b : Bool . (b \ Nat \ 0 \ 1) \to\_\tau \lambda b : Bool . \lambda t : \* . \lambda s : t \to t . \lambda z : t . (b \ t \ (0 \ t \ s \ z) \ (1 \ t \ s \ z)) \\
\to\_\beta^\* \lambda b : Bool . \lambda t : \* . \lambda s : t \to t . \lambda z : t . (b \ t \ z \ (s z))
$$

Can this be formalized for the general case to obtain a new conversion rule for CoC? Has something like this been done already?

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

> **Comments:**
> **username_1**: Lookup systems with "internal parametricity", there you can prove these things internally.  
> **username_0**: Thank you. It's a line of research that I had not seen before and it seems indeed relevant for my question, and also very interesting in general.  

---

## 0 answers

