$𝚷$ -type

$𝚷$ -types, also known as dependent function types or dependent products, are motivated in several ways:

$𝚷$ -types internalize hypothetical judgements.
$𝚷$ -types generalize binary products $(\times)$ to a product of a family of types indexed by another type.
$𝚷$ -types generalize functions so that the codomain can depend on the input.
$𝚷$ -types correspond to spaces of sections.

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

Γ ⊢ 𝑓 : \prod 𝑥 : 𝐴 𝐵 (𝑥)

corresponds to a section

Γ, 𝑥 : 𝐴 ⊢ 𝑓 (𝑥) : 𝐵 (𝑥)

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. The formation, introduction, and elimination rules are given by¹

Γ . 𝐴 ⊢ 𝐵 Γ ⊢ 𝚷 Γ (𝐴 . 𝐵) (Π) Γ . 𝐴 ⊢ 𝑏 : 𝐵 Γ ⊢ 𝜆 Γ, 𝐴, 𝐵 (𝑏) : 𝚷 (𝐴 . 𝐵) (Π 𝐼)

Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝑓 : 𝚷 (𝐴 . 𝐵) Γ ⊢ 𝐚 𝐩 𝐩 Γ, 𝐴, 𝐵 (𝑓, 𝑎) : 𝐵 [𝐢 𝐝 . 𝑎] (Π 𝐸)

while we also have the substitution naturality rules

Δ ⊢ 𝛾 : Γ Γ . 𝐴 ⊢ 𝐵 Δ ⊢ 𝚷 (𝐴 . 𝐵) [𝛾] = 𝚷 (𝐴 [𝛾] . 𝐵 [(𝛾 \circ 𝐩) . 𝐪])

Δ ⊢ 𝛾 : Γ Γ . 𝐴 ⊢ 𝑏 : 𝐵 Δ ⊢ 𝜆 (𝑏) [𝛾] = 𝜆 (𝑏 [(𝛾 \circ 𝐩) . 𝐪]) : 𝚷 (𝐴 . 𝐵) [𝛾]

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

and judgemental computation rules for β-reduction and η-conversion

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

Γ ⊢ 𝑓 : 𝚷 (𝐴 . 𝐵) Γ ⊢ 𝑓 = 𝜆 (𝐚 𝐩 𝐩 (𝑓 [𝐩, 𝐪])) : 𝚷 (𝐴 . 𝐵) (Π 𝜂)

In terms of Internalizing judgemental structure, we can formalize the notion of the correspondence outlined above as an operation

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

natural in $Γ$ with a family of bijections

𝜄 Γ, 𝐴, 𝐵 : T m (Γ, 𝚷 Γ (𝐴, 𝐵)) ≅ T m (Γ . 𝐴, 𝐵)

also natural in $Γ$ . This gives the inference rules above.

For brevity and laziness, the $𝚷$ formation rule will be considered a _presuppositi ↩