Function types

Given types $𝐴$ and $𝐵$ , the function type $𝐴 \to 𝐵$ contains mappings whose inputs are in $𝐴$ and outputs are in $𝐵$ , i.e. functions. Under propositions as types, this corresponds to implication, since a term of $𝐴 \to 𝐵$ takes proofs of $𝐴$ to proofs of $𝐵$ .

Standard presentation

In the cartesian calculus of substitutions we can introduce function types with the following typing rules. The formation, introduction, and elimination rules are

Γ ⊢ 𝐴 Γ ⊢ 𝐵 Γ ⊢ 𝐴 \to Γ 𝐵 (\to) Γ ⊢ 𝐵 Γ . 𝐴 ⊢ 𝑏 : 𝐵 [𝐩] Γ ⊢ 𝜆' Γ, 𝐴, 𝐵 (𝑏) : 𝐴 \to 𝐵 (\to I)

Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝑓 : 𝐴 \to 𝐵 Γ ⊢ 𝐚 𝐩 𝐩' Γ, 𝐴, 𝐵 (𝑓, 𝑎) : 𝐵 (\to E)

while we also have the substitution naturality rules

Δ ⊢ 𝛾 : Γ Γ ⊢ 𝐴 Γ ⊢ 𝐵 Δ ⊢ (𝐴 \to 𝐵) [𝛾] = 𝐴 [𝛾] \to 𝐵 [𝛾] (\to - N)

Δ ⊢ 𝛾 : Γ Γ ⊢ 𝐵 Γ . 𝐴 ⊢ 𝑏 : 𝐵 [𝐩] Γ ⊢ 𝜆' (𝑏) [𝛾] = 𝜆' (𝑏 [𝛾 . 𝐴]) : 𝐴 [𝛾] \to 𝐵 [𝛾] (\to I - N)

Δ ⊢ 𝛾 : Γ Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝑓 : 𝐴 \to 𝐵 Δ ⊢ 𝐚 𝐩 𝐩' (𝑓, 𝑎) [𝛾] = 𝐚 𝐩 𝐩' (𝑓 [𝛾], 𝑎 [𝛾]) : 𝐵 [𝛾]

and judgemental computation rules for $𝛽$ -computation and $𝜂$ -unicity

Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝐵 Γ . 𝐴 ⊢ 𝑏 : 𝐵 [𝐩] Γ ⊢ 𝐚 𝐩 𝐩' (𝜆' (𝑏), 𝑎) = 𝑏 [𝐢 𝐝 . 𝑎] : 𝐵 (\to 𝛽)

Γ ⊢ 𝑓 : 𝐴 \to 𝐵 Γ ⊢ 𝑓 = 𝜆' (𝐚 𝐩 𝐩' (𝑓 [𝐩], 𝐪)) : 𝐴 \to 𝐵 (\to 𝜂)

From $Π$ -types

In the Cartesian calculus of substitutions with $Π$ -types, it is not necessary to give separate typing rules to establish function types. Instead we have

Γ ⊢ 𝐴 Γ . 𝐴 ⊢ 𝐩 : Γ (W) Γ ⊢ 𝐵 Γ . 𝐴 ⊢ 𝐵 [𝐩] Γ ⊢ 𝚷 (𝐴, 𝐵 [𝐩]) (Π)

and so we can define $𝐴 \to 𝐵 : = 𝚷 (𝐴, 𝐵 [𝐩])$ .

Derivation of above typing rules

For $\to I$ we have

Γ . 𝐴 ⊢ 𝑏 : 𝐵 [𝐩] Γ ⊢ 𝜆 (𝑏) : 𝚷 (𝐴, 𝐵 [𝐩]) (Π I)

so we take $𝜆' Γ, 𝐴, 𝐵 (𝑏) = 𝜆 Γ, 𝐴, 𝐵 [𝐩] (𝑏)$ .

For $\to E$ we have

Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝑓 : 𝚷 (𝐴, 𝐵 [𝐩]) Γ ⊢ 𝐚 𝐩 𝐩 (𝑓, 𝑎) : 𝐵 [𝐩 \circ 𝐢 𝐝 . 𝑎] (Π E) Γ ⊢ 𝐚 𝐩 𝐩 (𝑓, 𝑎) : 𝐵 (= 𝛽 𝐩)

so we take $𝐚 𝐩 𝐩' Γ, 𝐴, 𝐵 (𝑓, 𝑎) = 𝐚 𝐩 𝐩 Γ, 𝐴, 𝐵 [𝐩] (𝑓, 𝑎)$ .

The derivations of $\to - N$ , $\to I - N$ , $\to E - N$ , $\to 𝛽$ , and $\to 𝜂$ follow directly from those of the $𝚷$ -type taking into account the equalities

𝐩 \circ 𝐢 𝐝 . 𝑎 = 𝐢 𝐝, 𝐩 \circ 𝛾 . 𝑎 [𝛾] = 𝛾

which follow from $𝛽 𝐩$ .

Internalizing judgemental structure

In terms of Internalizing judgemental structure, we have an operation

(\to Γ) : T y (Γ) \times T y (Γ) \to T y (Γ)

natural in $Γ$ with a family of bijections

𝜄 Γ, 𝐴, 𝐵 : T m (Γ, 𝐴 \to Γ 𝐵) ≅ T m (Γ . 𝐴, 𝐵 [𝐩])

also natural in $Γ$ . Cf. the corresponding discussion for $𝚷$ -types.

#state/develop | #lang/en | #SemBr

Function types

Standard presentation

From Π-types

Internalizing judgemental structure

From $Π$ -types