CCCs and typed λ-calculi

Andrzej Filinski Draft of July 1, 1992 (16:17)

Definition 1 (Type/object)

A ::= A_{prim} | 1 | A_{1} × A_{2} | [A_{1}→A_{2}]

Definition 2 (Simply-typed λ-calculus) Syntax:

e ::= x | () | (e_{1}, e_{2}) | π_{1}(e) | π_{2}(e) | λx:A. e | e_{1} e_{2}
Γ ::= • | Γ, x:A

Typing:

\overline{Γ, x:A ⊢ x : A} ; \frac{Γ ⊢ x : A}{Γ, y:B ⊢ x : A} ; \overline{Γ ⊢ () : 1}  \frac{Γ ⊢ e_{1} : A  Γ ⊢ e_{2} : B}{Γ ⊢ (e_{1}, e_{2}) : A × B} ; \frac{Γ ⊢ e : A × B}{Γ ⊢ π_{1}(e) : A} ; \frac{Γ ⊢ e : A × B}{Γ ⊢ π_{2}(e) : B}  \frac{Γ, x:A ⊢ e : B}{Γ ⊢ λx:A. e : [A→B]} ; \frac{Γ ⊢ e_{1} : [A→B]  Γ ⊢ e_{2} : A}{Γ ⊢ e_{1} e_{2} : B}

Equality (congruence):

\overline{e =_{l} e} ; \frac{e =_{l} e′  e′ =_{l} e′′}{e =_{l} e′′} ; \frac{e =_{l} e′}{e′ =_{l} e′}  \frac{e_{1} =_{l} e′_{1}  e_{2} =_{l} e′_{2}}{(e_{1}, e_{2}) =_{l} (e′_{1}, e′_{2})} ; \frac{e =_{l} e′}{π_{1}(e) =_{l} π_{1}(e′)} ; \frac{e =_{l} e′}{π_{2}(e) =_{l} π_{2}(e′)}  \frac{e =_{l} e′}{λx. e =_{l} λx. e′} ; \frac{e_{1} =_{l} e′_{1}  e_{2} =_{l} e′_{2}}{e_{1} e_{2} =_{l} e′_{1} e′_{2}}

Equality (proper equations):

\overline{() =_{l} e} ; \overline{π_{1}((e_{1}, e_{2})) =_{l} e_{1}}  \overline{π_{2}((e_{1}, e_{2})) =_{l} e_{2}} ; \overline{(π_{1}(e), π_{2}(e) =_{l} e}  \overline{(λx. e_{1}) e_{2} =_{l} e_{1}[e_{2}/x]}_{\overline{λx. e x =_{l} e} (x∉F V (e_{2}))}

Definition 3 (Cartesian closed category) Syntax:

f = id | f_{1} ∘ f_{2} | ⟨⟩ | ⟨f_{1}, f_{2}⟩ | fst | snd | cur(f) | app

Typing:

\overline{id : A → A} ; \frac{f : A → B  g : B → C}{g ∘ f : A → C} ; \overline{⟨⟩ : A → 1}  \frac{f : C → A  g : C → B}{⟨f, g⟩ : C → A × B} ; \overline{fst : A × B → A} ; \overline{snd : A × B → B}  \frac{f : A × B → C}{cur(f) : A → [B→C]} ; \overline{app : [B→C] × B → C}

Equality (congruence):

\overline{f =_{c} f} ; \frac{f =_{c} f′  f′ =_{c} f′′}{f =_{c} f′′}  \frac{f =_{c} f′}{f′ =_{c} f′} ; \frac{f =_{c} f′  g =_{c} g′}{g ∘ f =_{c} g′ ∘ f′}  \frac{f =_{c} f′  g =_{c} g′}{⟨f, g⟩ =_{c} ⟨f′, g′⟩} ; \frac{f =_{c} f′}{cur(f) =_{c} cur(f′)}

Equality (proper equations):

\overline{id ∘ f =_{c} f} \overline{f ∘ id =_{c} f} \overline{h ∘ (g ∘ f) =_{c} (h ∘ g) ∘ f} \overline{⟨⟩ =_{c} f} \overline{fst ∘ ⟨f, g⟩ =_{c} f} \overline{snd ∘ ⟨f, g⟩ =_{c} g} \overline{⟨fst ∘ h, snd ∘ h⟩ =_{c} h}

app ∘ ⟨cur(f) ∘ fst, snd⟩ =_{c} f
cur(app ∘ ⟨f ∘ fst, snd⟩) =_{c} f

Note: For compactness, we will omit proof cases for second projections and nullary product (terminal object), and congruence. All these are included in the machine-verifiable proof. We will also elide explicit typings in most cases.

Lemma 1 The following are some useful consequences of the categorical equations:

⟨f, g⟩ ∘ h =_{c} ⟨f ∘ h, g ∘ h⟩
app ∘ ⟨cur(f) ∘ g, h⟩ =_{c} f ∘ ⟨g, h⟩
cur(f) ∘ g =_{c} cur(f ∘ ⟨g ∘ fst, snd⟩)

Proof: (Each result uses the previous one)

⟨f, g⟩ ∘ h

= ⟨fst ∘ (⟨f, g⟩ ∘ h), snd ∘ (⟨f, g⟩ ∘ h)⟩
= ⟨(fst ∘ ⟨f, g⟩) ∘ h, (snd ∘ ⟨f, g⟩) ∘ h⟩
= ⟨f ∘ h, g ∘ h⟩

app ∘ ⟨cur(f) ∘ g, h⟩

= app ∘ ⟨cur(f) ∘ (fst ∘ ⟨g, h⟩), snd ∘ ⟨g, h⟩⟩
= app ∘ ⟨(cur(f) ∘ fst) ∘ ⟨g, h⟩, snd ∘ ⟨g, h⟩⟩
= app ∘ (⟨cur(f) ∘ fst, snd⟩ ∘ ⟨g, h⟩)
= (app ∘ ⟨cur(f) ∘ fst, snd⟩) ∘ ⟨g, h⟩
= f ∘ ⟨g, h⟩

cur(f) ∘ g
= cur(app ∘ ⟨(cur(f) ∘ g) ∘ fst, snd⟩)
= cur(app ∘ ⟨cur(f) ∘ (g ∘ fst), snd⟩)
= cur(f ∘ ⟨g ∘ fst, snd⟩)

Note: in the following, we will usually not write out the reassociation steps in proofs. □

Definition 4 To every environment Γ, we associate an object [[Γ]]; to every Γ-variable x : A, a morphism [[Γ ⊢_{v} x]] : [[Γ]] → A; and to every Γ-expression e : A, a morphism [[Γ ⊢ e]] : [[Γ]] → A as follows:

[[•]] = 1
[[Γ, x:A]] = [[Γ]] × A
[[Γ, x ⊢_{v} x]] = snd
[[Γ, y ⊢_{v} x]] = [[Γ ⊢_{v} x]] ∘ fst
[[Γ ⊢ x]] = [[Γ ⊢_{v} x]]
[[Γ ⊢ ()]] = ⟨⟩
[[Γ ⊢ (e_{1}, e_{2})]] = ⟨[[Γ ⊢ e_{1}]], [[Γ ⊢ e_{2}]]⟩
[[Γ ⊢ π_{1}(e)]] = fst ∘ [[Γ ⊢ e]]
[[Γ ⊢ π_{2}(e)]] = snd ∘ [[Γ ⊢ e]]
[[Γ ⊢ λx. e]] = cur([[Γ, x ⊢ e]])
[[Γ ⊢ e_{1} e_{2}]] = app ∘ ⟨[[Γ ⊢ e_{1}]], [[Γ ⊢ e_{2}]]⟩

(Easy to check that translation is well-typed).

We can now formulate a key result, relating substitution of λ-terms to categorical composition:

Lemma 2 (substitution extension) For all Γ-expressions e, substitutions σ assigning Δexpressions to Γ-vars, and morphisms f : [[Δ]] → [[Γ]]:

(∀x ∈ Γ. [[Γ ⊢_{v} x]] ∘ f = [[Δ ⊢ x[σ]]]) ⇒ [[Γ ⊢ e]] ∘ f = [[Δ ⊢ e[σ]]]

Proof: It is convenient to distinguish a weaker form of the lemma, in which the range of σ is restricted to Δ-variables, not full expressions. The proof in both cases proceeds by structural induction on e:

[[Γ ⊢ x]] ∘ f

= [[Γ ⊢_{v} x]] ∘ f
= [[Δ ⊢ x[σ]]]

[[Γ ⊢ (e_{1}, e_{2})]] ∘ f

= ⟨[[Γ ⊢ e_{1}]], [[Γ ⊢ e_{2}]]⟩ ∘ f
= ⟨[[Γ ⊢ e_{1}]] ∘ f, [[Γ ⊢ e_{2}]] ∘ f⟩
= ⟨[[Δ ⊢ e_{1}[σ]]], [[Δ ⊢ e_{2}[σ]]]⟩
= [[Δ ⊢ (e_{1}[σ], e_{2}[σ])]]
= [[Δ ⊢ (e_{1}, e_{2})[σ]]]

[[Γ ⊢ π_{1}(e)]] ∘ f

= fst ∘ [[Γ ⊢ e]] ∘ f
= fst ∘ [[Δ ⊢ e[σ]]]
= [[Δ ⊢ π_{1}(e[σ])]]
= [[Δ ⊢ π_{1}(e)[σ]]]

[[Γ ⊢ λx. e]] ∘ f
= cur([[Γ, x ⊢ e]]) ∘ f
= cur([[Γ, x ⊢ e]] ∘ ⟨f ∘ fst, snd⟩)
=^{∗} cur([[Δ, x ⊢ e[σ]]])
= [[Δ ⊢ λx. e[σ]]]
= [[Δ ⊢ (λx. e)[σ]]]
[[Γ ⊢ e_{1} e_{2}]] ∘ f
= app ∘ ⟨[[Γ ⊢ e_{1}]], [[Γ ⊢ e_{2}]]⟩ ∘ f
= app ∘ ⟨[[Γ ⊢ e_{1}]] ∘ f, [[Γ ⊢ e_{2}]] ∘ f⟩
= app ∘ ⟨[[Δ ⊢ e_{1}[σ]]], [[Δ ⊢ e_{2}[σ]]]⟩
= [[Δ ⊢ e_{1}[σ] e_{2}[σ]]]
= [[Δ ⊢ (e_{1} e_{2})[σ]]]

∗Pick x s.t. it does not occur in Γ, Δ, nor σ (in particular, x[σ] = x). To use the induction hypothesis here we need to prove:

∀y ∈ (Γ, x). [[Γ, x ⊢_{v} y]] ∘ ⟨f ∘ fst, snd⟩ = [[Δ, x ⊢ y[σ]]]

Two cases (y = x or y ≠ x, y ∈ Γ):

[[Γ, x ⊢_{v} x]] ∘ ⟨f ∘ fst, snd⟩
= snd ∘ ⟨f ∘ fst, snd⟩
= snd
= [[Δ, x ⊢_{v} x]]
= [[Δ, x ⊢ x]]
= [[Δ, x ⊢ x[σ]]]

[[Γ, x ⊢_{v} y]] ∘ ⟨f ∘ fst, snd⟩
= [[Γ ⊢_{v} y]] ∘ fst ∘ ⟨f ∘ fst, snd⟩
= [[Γ ⊢_{v} y]] ∘ f ∘ fst
= [[Δ ⊢ y[σ]]] ∘ fst
=^{+} [[Δ, x ⊢ y[σ]]]
= [[Δ, x ⊢ y[σ]]]

+ In the weak form of the lemma, y[σ] is itself a variable (which cannot be x because x is not a Δ-variable), and the equation holds trivially by definition of [[⊢]]. In the general (strong) case, the equation follows from corollary 1 below (which is proved using only the weak form, of course). □

Corollary 1 (weakening) Let e be a Γ-expression, and x a variable not in Γ. Then

[[Γ, x ⊢ e]] = [[Γ ⊢ e]] ∘ fst

Proof: Take Δ = (Γ, x), f = fst, σ = id. To use the lemma (weak form), we must show that

∀y ∈ Γ. [[Γ ⊢_{v} y]] ∘ fst = [[Γ, x ⊢ y[id]]]

But this follows immediately from the definition of [[⊢]]:

[[Γ, x ⊢ y[id]]] = [[Γ, x ⊢ y]] = [[Γ, x ⊢_{v} y]] = [[Γ ⊢_{v} y]] ∘ fst

(y cannot be x because x ∉ Γ.) □

Corollary 2 (substitution) For expressions e_{1} and e_{2},

[[Δ, x ⊢ e_{2}]] ∘ ⟨id, [[Δ ⊢ e_{1}]]⟩ = [[Δ ⊢ e_{2}[e_{1}/x]]]

Proof: Take e = e_{2}, Γ = (Δ, x), f = ⟨id, [[Δ ⊢ e_{1}]]⟩, and σ = e_{1}/x. The result follows directly from the lemma (strong form) if we can prove:

∀y ∈ (Δ, x). [[Δ, x ⊢_{v} y]] ∘ ⟨id, [[Δ ⊢ e_{1}]]⟩ = [[Δ ⊢ y[e_{1}/x]]]

Two cases (y = x or y ≠ x, y ∈ Δ):

[[Δ, x ⊢_{v} x]] ∘ ⟨id, [[Δ ⊢ e_{1}]]⟩
= snd ∘ ⟨id, [[Δ ⊢ e_{1}]]⟩
= [[Δ ⊢ e_{1}]]
= [[Δ ⊢ x[e_{1}/x]]]

[[Δ, x ⊢_{v} y]] ∘ ⟨id, [[Δ ⊢ e_{1}]]⟩
= [[Δ ⊢_{v} y]] ∘ fst ∘ ⟨id, [[Δ ⊢ e_{1}]]⟩
= [[Δ ⊢_{v} y]]
= [[Δ ⊢ y[e_{1}/x]]]
□

Proposition 1 If e =_{l} e′ then [[Γ ⊢ e]] =_{c} [[Γ ⊢ e′]].

Proof: Congruence is immediate since the translation is compositional in e. We only have to check that the proper equations are preserved:

[[Γ ⊢ π_{1}((e_{1}, e_{2}))]]
= fst ∘ [[Γ ⊢ (e_{1}, e_{2})]]
= fst ∘ ⟨[[Γ ⊢ e_{1}]], [[Γ ⊢ e_{2}]]⟩
= [[Γ ⊢ e_{1}]]
[[Γ ⊢ (π_{1}(e), π_{2}(e))]]
= ⟨[[Γ ⊢ π_{1}(e)]], [[Γ ⊢ π_{2}(e)]]⟩
= ⟨fst ∘ [[Γ ⊢ e]], snd ∘ [[Γ ⊢ e]]⟩
= [[Γ ⊢ e]]

[[Γ ⊢ (λx. e_{1}) e_{2}]]
= app ∘ ⟨[[Γ ⊢ λx. e_{1}]], [[Γ ⊢ e_{2}]]⟩
= app ∘ ⟨cur([[Γ, x ⊢ e_{1}]]), [[Γ ⊢ e_{2}]]⟩
= [[Γ, x ⊢ e_{1}]] ∘ ⟨id, [[Γ ⊢ e_{2}]]⟩
= [[Γ ⊢ e_{1}[e_{2}/x]]]
[[Γ ⊢ λx. e x]] (x ∉ F V (e))
= cur([[Γ, x ⊢ e x]])
= cur(app ∘ ⟨[[Γ, x ⊢ e]], [[Γ, x ⊢ x]]⟩)
= cur(app ∘ ⟨[[Γ ⊢ e]] ∘ fst, snd⟩)
= [[Γ ⊢ e]]
□

Definition 5 To every CCC combinator f : A → B, we associate a λ-expression ⟨|f|⟩·x : B with a free variable x : A as follows:

⟨|id|⟩·x = x
⟨|g ∘ f|⟩·x = ⟨|g|⟩·(⟨|f|⟩·x)

⟨|⟨⟩|⟩·x = ()
⟨|⟨f, g⟩|⟩·x = (⟨|f|⟩·x, ⟨|g|⟩·x)
⟨|fst|⟩·x = π_{1}(x)
⟨|snd|⟩·x = π_{2}(x)
⟨|cur(f)|⟩·x = λy. ⟨|f|⟩·(x, y)
⟨|app|⟩·x = π_{1}(x) π_{2}(x)

Proposition 2 If f =_{c} f′ then ⟨|f|⟩·x =_{l} ⟨|f′|⟩·x. Proof: Again, the congruence cases for f = f′ are immediate. For the proper equations we verify:

⟨|id ∘ f|⟩·x

= ⟨|id|⟩·(⟨|f|⟩·x)
= ⟨|f|⟩·x

⟨|f ∘ id|⟩·x

= ⟨|f|⟩·(⟨|id|⟩·x)
= ⟨|f|⟩·x

⟨|h ∘ (g ∘ f)|⟩·x

= ⟨|h|⟩·(⟨|g ∘ f|⟩·x)
= ⟨|h|⟩·(⟨|g|⟩·(⟨|f|⟩·x))
= ⟨|h ∘ g|⟩·(⟨|f|⟩·x)
= ⟨|(h ∘ g) ∘ f|⟩·x

⟨|fst ∘ ⟨f, g⟩|⟩·x

= ⟨|fst|⟩·(⟨|⟨f, g⟩|⟩·x)
= π_{1}((⟨|f|⟩·x, ⟨|g|⟩·x))
= ⟨|f|⟩·x

⟨|⟨fst ∘ f, snd ∘ f⟩|⟩·x

= (⟨|fst ∘ f|⟩·x, ⟨|snd ∘ f|⟩·x)
= (π_{1}(⟨|f|⟩·x), π_{2}(⟨|f|⟩·x))
= ⟨|f|⟩·x

⟨|app ∘ ⟨cur(f) ∘ fst, snd⟩|⟩·x
= ⟨|app|⟩·(⟨|⟨cur(f) ∘ fst, snd⟩|⟩·x)
= ⟨|app|⟩·(⟨|cur(f) ∘ fst|⟩·x, ⟨|snd|⟩·x)
= ⟨|app|⟩·(⟨|cur(f)|⟩·(π_{1}(x)), π_{2}(x))
= ⟨|app|⟩·(λy. ⟨|f|⟩·(π_{1}(x), y), π_{2}(x))
= \begin{matrix}[π_{1}((λy. ⟨|f|⟩·(π_{1}(x), y), π_{2}(x)))] \\ [π_{2}((λy. ⟨|f|⟩·(π_{1}(x), y), π_{2}(x)))] \end{matrix}
= [λy. ⟨|f|⟩·(π_{1}(x), y)] [π_{2}(x)]
= ⟨|f|⟩·(π_{1}(x), π_{2}(x))
= ⟨|f|⟩·x
⟨|cur(app ∘ ⟨f ∘ fst, snd⟩)|⟩·x
= λy. ⟨|app ∘ ⟨f ∘ fst, snd⟩|⟩·(x, y)
= λy. ⟨|app|⟩·(⟨|⟨f ∘ fst, snd⟩|⟩·(x, y))
= λy. ⟨|app|⟩·(⟨|f ∘ fst|⟩·(x, y), ⟨|snd|⟩·(x, y))
= λy. ⟨|app|⟩·(⟨|f|⟩·(π_{1}((x, y))), π_{2}((x, y)))
= λy. \begin{matrix}[π_{1}((⟨|f|⟩·(π_{1}((x, y))), π_{2}((x, y))))] \\ [π_{2}((⟨|f|⟩·(π_{1}((x, y))), π_{2}((x, y))))] \end{matrix}
= λy. [⟨|f|⟩·(π_{1}((x, y)))] [π_{2}((x, y))]
= λy. (⟨|f|⟩·x) y
= ⟨|f|⟩·x
□

Definition 6 For any environment Γ, we define a Γ-expression \overline{Γ} : [[Γ]] as follows:

\overline{•} = ()
\overline{Γ, x:A} = (\overline{Γ}, x)

Proposition 3 Then for any Γ-expression e, ⟨|[[Γ ⊢ e]]|⟩·\overline{Γ} =_{l} e Proof: We first show that for any Γ-variable x,

⟨|[[Γ ⊢_{v} x]]|⟩·\overline{Γ} = x

This is easily verified by structural induction on the derivation of [[Γ ⊢_{v} x]]:

⟨|[[Γ′, x ⊢_{v} x]]|⟩·\overline{(Γ′, x)}_{= ⟨|snd|⟩·(\overline{Γ′}, x)}_{= π_{2}((\overline{Γ′}, x))}_{= x} ⟨|[[Γ′, y ⊢_{v} x]]|⟩·\overline{(Γ′, y)}

= ⟨|[[Γ′ ⊢_{v} x]] ∘ fst|⟩·(\overline{Γ′}, y)
= ⟨|[[Γ′ ⊢_{v} x]]|⟩·(π_{1}((\overline{Γ′}, y)))
= ⟨|[[Γ′ ⊢_{v} x]]|⟩·\overline{Γ′}
= x

We can now prove the main result by structural induction on e:

⟨|[[Γ ⊢ x]]|⟩·\overline{Γ}

= ⟨|[[Γ ⊢_{v} x]]|⟩·\overline{Γ}
= x

⟨|[[Γ ⊢ (e_{1}, e_{2})]]|⟩·\overline{Γ}

= ⟨|⟨[[Γ ⊢ e_{1}]], [[Γ ⊢ e_{2}]]⟩|⟩·\overline{Γ}
= (⟨|[[Γ ⊢ e_{1}]]|⟩·\overline{Γ}, ⟨|[[Γ ⊢ e_{2}]]|⟩·\overline{Γ})
= (e_{1}, e_{2})

⟨|[[Γ ⊢ π_{1}(e)]]|⟩·\overline{Γ}

= ⟨|fst ∘ [[Γ ⊢ e]]|⟩·\overline{Γ}
= π_{1}(⟨|[[Γ ⊢ e]]|⟩·\overline{Γ})
= π_{1}(e)

⟨|[[Γ ⊢ λx. e]]|⟩·\overline{Γ}

= ⟨|cur([[Γ, x ⊢ e]])|⟩·\overline{Γ}
= λx. ⟨|[[Γ, x ⊢ e]]|⟩·(\overline{Γ}, x)
= λx. ⟨|[[Γ, x ⊢ e]]|⟩·\overline{Γ, x}
= λx. e

⟨|[[Γ ⊢ e_{1} e_{2}]]|⟩·\overline{Γ}

= ⟨|app ∘ ⟨[[Γ ⊢ e_{1}]], [[Γ ⊢ e_{2}]]⟩|⟩·\overline{Γ}
= ⟨|app|⟩·(⟨|[[Γ ⊢ e_{1}]]|⟩·\overline{Γ}, ⟨|[[Γ ⊢ e_{2}]]|⟩·\overline{Γ})

= [π_{1}((⟨|[[Γ ⊢ e_{1}]]|⟩·\overline{Γ}, ⟨|[[Γ ⊢ e_{2}]]|⟩·\overline{Γ}))]

[π_{2}((⟨|[[Γ ⊢ e_{1}]]|⟩·\overline{Γ}, ⟨|[[Γ ⊢ e_{2}]]|⟩·\overline{Γ}))]

= [⟨|[[Γ ⊢ e_{1}]]|⟩·\overline{Γ}] [⟨|[[Γ ⊢ e_{2}]]|⟩·\overline{Γ}]
= e_{1} e_{2}

□

Definition 7 For any expression e : B with a free variable x : A, we define a morphism [[x ⊢⊢ e]] : A → B as

[[x ⊢⊢ e]] = [[•, x ⊢ e]] ∘ ⟨⟨⟩, id⟩

Proposition 4 For any morphism f

[[x ⊢⊢ ⟨|f|⟩·x]] =_{c} f

Proof: We first show that for any envioronment Γ and Γ-expression e,

[[Γ ⊢ ⟨|f|⟩·e]] = f ∘ [[Γ ⊢ e]]

by structural induction on f:

[[Γ ⊢ ⟨|id|⟩·e]]

= [[Γ ⊢ e]]
= id ∘ [[Γ ⊢ e]]

[[Γ ⊢ ⟨|g ∘ f|⟩·e]]

= [[Γ ⊢ ⟨|g|⟩·(⟨|f|⟩·e)]]
= g ∘ [[Γ ⊢ ⟨|f|⟩·e]]
= g ∘ f ∘ [[Γ ⊢ e]]

[[Γ ⊢ ⟨|⟨f, g⟩|⟩·e]]

= [[Γ ⊢ (⟨|f|⟩·e, ⟨|g|⟩·e)]]
= ⟨[[Γ ⊢ ⟨|f|⟩·e]], [[Γ ⊢ ⟨|g|⟩·e]]⟩
= ⟨f ∘ [[Γ ⊢ e]], g ∘ [[Γ ⊢ e]]⟩
= ⟨f, g⟩ ∘ [[Γ ⊢ e]]

[[Γ ⊢ ⟨|fst|⟩·e]]

= [[Γ ⊢ π_{1}(e)]]
= fst ∘ [[Γ ⊢ e]]

[[Γ ⊢ ⟨|cur(f)|⟩·e]]
= [[Γ ⊢ λy. ⟨|f|⟩·(e, y)]]
= cur([[Γ, y ⊢ ⟨|f|⟩·(e, y)]])
= cur(f ∘ [[Γ, y ⊢ (e, y)]])
= cur(f ∘ ⟨[[Γ, y ⊢ e]], [[Γ, y ⊢ y]]⟩)
= cur(f ∘ ⟨[[Γ ⊢ e]] ∘ fst, snd⟩)
= cur(f) ∘ [[Γ ⊢ e]]
[[Γ ⊢ ⟨|app|⟩·e]]
= [[Γ ⊢ π_{1}(e) π_{2}(e)]]
= app ∘ ⟨[[Γ ⊢ π_{1}(e)]], [[Γ ⊢ π_{2}(e)]]⟩
= app ∘ ⟨fst ∘ [[Γ ⊢ e]], snd ∘ [[Γ ⊢ e]]⟩
= app ∘ [[Γ ⊢ e]]

The proposition now follows directly, taking Γ = (•, x) and e = x: [[x ⊢⊢ ⟨|f|⟩·x]] = [[•, x ⊢ ⟨|f|⟩·x]] ∘ ⟨⟨⟩, id⟩ = f ∘ [[•, x ⊢ x]] ∘ ⟨⟨⟩, id⟩ = f ∘ snd ∘ ⟨⟨⟩, id⟩ = f

□

Summarizing, we have: Theorem 1 (Equivalence) The following holds of the translations:

1. Γ ⊢ e =_{l} e′ : A iff [[Γ ⊢ e]] =_{c} [[Γ ⊢ e′]] : [[Γ]] → A.

2. f =_{c} f′ : A → B iff x:A ⊢ ⟨|f|⟩·x =_{l} ⟨|f′|⟩·x : B.

3. Γ ⊢ ⟨|[[Γ ⊢ e]]|⟩·\overline{Γ} =_{l} e : A.

4. [[x:A ⊢⊢ ⟨|f|⟩·x]] =_{c} f : A → B. Proof: Most of the results have already been explicitly proven above. The “if” direction in 1 follows from “only if” in 2 and the equality in 3: if [[Γ ⊢ e]] = [[Γ ⊢ e′]] then

e = ⟨|[[Γ ⊢ e]]|⟩·\overline{Γ} = (⟨|[[Γ ⊢ e]]|⟩·x)[\overline{Γ}/x] = (⟨|[[Γ ⊢ e′]]|⟩·x)[\overline{Γ}/x] = ⟨|[[Γ ⊢ e′]]|⟩·\overline{Γ} = e′ Analogously, if ⟨|f|⟩·x = ⟨|f′|⟩·x then f = [[x ⊢⊢ ⟨|f|⟩·x]] = [[•, x ⊢ ⟨|f|⟩·x]]∘⟨⟨⟩, id⟩ = [[•, x ⊢ ⟨|f′|⟩·x]]∘⟨⟨⟩, id⟩ = [[x ⊢⊢ ⟨|f′|⟩·x]] = f′

□