Product type

Given types $𝐴$ and $𝐵$ , the product type $𝐴 \times 𝐵$ contains ordered pairs $(𝑎, 𝑏)$ for $𝑎 : 𝐴$ and $𝑏 : 𝐵$ , i.e. it generalizes the cartesian product. Under propositions as types, this corresponds to conjunction, since a proof of $𝐴 \times 𝐵$ gives a proof of $𝐴$ and a proof of $𝐵$ .

Standard presentation

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

Γ ⊢ 𝐴 Γ ⊢ 𝐵 Γ ⊢ 𝐴 \times Γ 𝐵 (\times) Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝑏 : 𝐵 Γ ⊢ ⟨ 𝑎, 𝑏 ⟩' Γ, 𝐴, 𝐵 : 𝐴 \times 𝐵 (\times I)

Γ ⊢ 𝑝 : 𝐴 \times 𝐵 Γ ⊢ 𝐟 𝐬 𝐭' Γ, 𝐴, 𝐵 (𝑝) : 𝐴 (\times E 1) Γ ⊢ 𝑝 : 𝐴 \times 𝐵 Γ ⊢ 𝐬 𝐧 𝐝' Γ, 𝐴, 𝐵 (𝑝) : 𝐵 (\times E 2)

while we also have the substitution naturality rules

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

Δ ⊢ 𝛾 : Γ Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝑏 : 𝐵 Δ ⊢ ⟨ 𝑎, 𝑏 ⟩' [𝛾] = ⟨ 𝑎 [𝛾], 𝑏 [𝛾]' ⟩ : 𝐴 [𝛾] \times 𝐵 [𝛾] (\times I - N)

Δ ⊢ 𝛾 : Γ Γ ⊢ 𝑝 : 𝐴 \times 𝐵 Δ ⊢ 𝐟 𝐬 𝐭' (𝑝) [𝛾] = 𝐟 𝐬 𝐭' (𝑝 [𝛾]) : 𝐴 [𝛾] (\times E 1 - N)

Δ ⊢ 𝛾 : Γ Γ ⊢ 𝑝 : 𝐴 \times 𝐵 Δ ⊢ 𝐬 𝐧 𝐝' (𝑝) [𝛾] = 𝐬 𝐧 𝐝' (𝑝 [𝛾]) : 𝐵 [𝛾] (\times E 2 - N)

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

Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝑏 : 𝐵 Γ ⊢ 𝐟 𝐬 𝐭' (⟨ 𝑎, 𝑏 ⟩)' = 𝑎 : 𝐴 (\times 𝛽 1)

Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝑏 : 𝐵 Γ ⊢ 𝐬 𝐧 𝐝' (⟨ 𝑎, 𝑏 ⟩)' = 𝑏 : 𝐵 (\times 𝛽 2)

Γ ⊢ 𝑝 : 𝐴 \times 𝐵 Γ ⊢ 𝑝 = ⟨ 𝐟 𝐬 𝐭' (𝑝), 𝐬 𝐧 𝐝' (𝑝) ⟩' : 𝐴 \times 𝐵 (\times 𝜂)

From $Σ$ -types

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

Γ ⊢ 𝐴 Γ . 𝐴 ⊢ 𝐩 : Γ (W) Γ ⊢ 𝐵 Γ . 𝐴 ⊢ 𝐵 [𝐩] Γ ⊢ 𝚺 (𝐴, 𝐵 [𝐩]) (Σ)

and so we can define $𝐴 \times Γ 𝐵 : = 𝚺 Γ (𝐴, 𝐵 [𝐩])$ .

Derivation of above typing rules

For $\times I$ , we have

Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝑏 : 𝐵 Γ . 𝐴 ⊢ 𝑏 [𝐩] : 𝐵 [𝐩] (W) Γ ⊢ ⟨ 𝑎, 𝑏 [𝐩] ⟩ : 𝚺 (𝐴, 𝐵 [𝐩])

so we take $⟨ 𝑎, 𝑏 ⟩' Γ, 𝐴, 𝐵 : = ⟨ 𝑎, 𝑏 [𝐩] ⟩ Γ, 𝐴, 𝐵 [𝐩]$ .

For $\times E 1$ we have

Γ ⊢ 𝑝 : 𝚺 (𝐴, 𝐵 [𝐩]) Γ ⊢ 𝐟 𝐬 𝐭 (𝑝) : 𝐴

so we take $𝐟 𝐬 𝐭' Γ, 𝐴, 𝐵 : = 𝐟 𝐬 𝐭 Γ, 𝐴, 𝐵 [𝐩]$ .

For $\times E 2$ we have

Γ ⊢ 𝑝 : 𝚺 (𝐴, 𝐵 [𝐩]) Γ ⊢ 𝐬 𝐧 𝐝 (𝑝) : 𝐵 [𝐩 \circ 𝐢 𝐝 . 𝐟 𝐬 𝐭 (𝑝)] Γ ⊢ 𝐬 𝐧 𝐝 (𝑝) : 𝐵

so we take $𝐬 𝐧 𝐝' Γ, 𝐴, 𝐵 : = 𝐬 𝐧 𝐝 Γ, 𝐴, 𝐵 [𝐩]$ .

The equalities follow.

Internalizing judgemental structure

In terms of Internalizing judgemental structure, we have an operation

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

natural in $Γ$ with a family of bijections

𝜄 Γ, 𝐴, 𝐵 : T m (Γ, 𝐴 \times Γ 𝐵) ≅ T m (Γ, 𝐴) \times T m (Γ, 𝐵)

also natural in $Γ$ .

#state/tidy | #lang/en | #SemBr

Product type

Standard presentation

From Σ-types

Internalizing judgemental structure

From $Σ$ -types