$Σ$ -types

$𝚺$ -types, also known as dependent pair types or dependent sums, are motivated in several ways:

$𝚺$ -types internalize context extension.
$𝚺$ -types generize binary coproducts $(+)$ to a coproduct of a family of types indexed by another type.
$𝚺$ -types generalize binary products $(\times)$ so that the type of the right element can depend on the type of the left input.
$𝚺$ -types correspond to total spaces of a fibration.
$𝚺$ -types correspond to existential quantification $(\exists)$ over elements of some type.

The core idea is that given a type family (fibration) $Γ, 𝑥 : 𝐴 ⊢ 𝐵 (𝑥)$ , a term

Γ ⊢ 𝑝 : \sum 𝑥 : 𝐴 𝐵 (𝑥)

corresponds to a pair of terms $Γ ⊢ 𝐟 𝐬 𝐭 (𝑝) : 𝐴$ and $Γ ⊢ 𝐬 𝐧 𝐝 (𝑝) : 𝐵 (𝐟 𝐬 𝐭 (𝑝))$ , and vice versa.

Standard presentation

Here we give a formal presentation of $𝚺$ -types in the cartesian calculus of substitutions, following Principles of dependent type theory. #m/def/type The formation, introduction, and elimination rules are given by¹

Γ . 𝐴 ⊢ 𝐵 Γ ⊢ 𝚺 Γ (𝐴, 𝐵) (Σ) Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝑏 : 𝐵 [𝐢 𝐝 . 𝑎] Γ ⊢ ⟨ 𝑎, 𝑏 ⟩ Γ, 𝐴, 𝐵 : Σ (𝐴, 𝐵) (Σ I)

Γ ⊢ 𝑝 : 𝚺 (𝐴, 𝐵) Γ ⊢ 𝐟 𝐬 𝐭 Γ, 𝐴, 𝐵 (𝑝) : 𝐴 (Σ E 1) Γ ⊢ 𝑝 : 𝚺 (𝐴, 𝐵) Γ ⊢ 𝐬 𝐧 𝐝 Γ, 𝐴, 𝐵 (𝑝) : 𝐵 [𝐢 𝐝 . 𝐟 𝐬 𝐭 (𝑝)] (Σ E 2)

while we also have the substitution naturality rules²

Δ ⊢ 𝛾 : Γ Γ . 𝐴 ⊢ 𝐵 Δ ⊢ 𝚺 (𝐴, 𝐵) [𝛾] = 𝚺 (𝐴 [𝛾] . 𝐵 [𝛾 . 𝐴]) (𝚺 - N)

Δ ⊢ 𝛾 : Γ Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝑏 : 𝐵 [𝐢 𝐝 . 𝑎] Δ ⊢ ⟨ 𝑎, 𝑏 ⟩ [𝛾] = ⟨ 𝑎 [𝛾], 𝑏 [𝛾] ⟩ : 𝚺 (𝐴, 𝐵) [𝛾] (Σ I - N)

Δ ⊢ 𝛾 : Γ Γ ⊢ 𝑝 : 𝚺 (𝐴, 𝐵) Δ ⊢ 𝐟 𝐬 𝐭 (𝑝) [𝛾] = 𝐟 𝐬 𝐭 (𝑝 [𝛾]) : 𝐴 [𝛾] (Σ E 1 - N)

Δ ⊢ 𝛾 : Γ Γ ⊢ 𝑝 : 𝚺 (𝐴, 𝐵) Δ ⊢ 𝐬 𝐧 𝐝 (𝑝) [𝛾] = 𝐬 𝐧 𝐝 (𝑝 [𝛾]) : 𝐵 [𝐢 𝐝 . 𝐟 𝐬 𝐭 (𝑝) \circ 𝛾] (Σ E 2 - N)

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

Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝑏 : 𝐵 [𝐢 𝐝 . 𝑎] Γ ⊢ 𝐟 𝐬 𝐭 (⟨ 𝑎, 𝑏 ⟩) = 𝑎 : 𝐴 (Σ 𝛽 1) Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝑏 : 𝐵 [𝐢 𝐝 . 𝑎] Γ ⊢ 𝐬 𝐧 𝐝 (⟨ 𝑎, 𝑏 ⟩) = 𝑏 : 𝐵 [𝐢 𝐝 . 𝑎] (Σ 𝛽 2)

Γ ⊢ 𝑝 : 𝚺 (𝐴, 𝐵) Γ ⊢ 𝑝 = ⟨ 𝐟 𝐬 𝐭 (𝑝), 𝐬 𝐧 𝐝 (𝑝) ⟩ : 𝚺 (𝐴, 𝐵) (Σ 𝜂)

In terms of Internalizing judgemental structure, we can formalize the correspondence described in the core idea with an operation

𝚺 Γ : ⎛ ⎜ ⎜ ⎝ ∐ 𝐴 \in T y (Γ) T y (Γ . 𝐴) ⎞ ⎟ ⎟ ⎠ \to T y (Γ)

natural in $Γ$ with a family of bijections

𝜄 Γ, 𝐴, 𝐵 : T m (Γ, 𝚺 Γ (𝐴, 𝐵)) ≅ ∐ 𝑎 \in T m (Γ, 𝐴) T m (Γ, 𝐵 [𝐢 𝐝 . 𝑎])

also natural in $Γ$ .

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

For brevity and laziness, the premisses of the $𝚺$ formation rule will be considered presuppositions. ↩
Where we invoke Substitution extension by a type. ↩