$𝚷$ -types

$𝚷$ -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 $(\to)$ so that the codomain can depend on the input.
$𝚷$ -types correspond to spaces of sections.
$𝚷$ -types correspond to universal quantification $(\forall)$ over elements of some type.

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

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

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

while we also have the substitution naturality rules²

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

Δ ⊢ 𝛾 : Γ Γ . 𝐴 ⊢ 𝑏 : 𝐵 Δ ⊢ 𝜆 (𝑏) [𝛾] = 𝜆 (𝑏 [𝛾 . 𝐴]) : 𝚷 (𝐴, 𝐵) [𝛾] (Π I - N)

Δ ⊢ 𝛾 : Γ Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝑓 : 𝚷 (𝐴, 𝐵) Δ ⊢ 𝐚 𝐩 𝐩 (𝑓, 𝑎) [𝛾] = 𝐚 𝐩 𝐩 (𝑓 [𝛾], 𝑎 [𝛾]) : 𝐵 [𝛾 . 𝑎 [𝛾]] (Π E - N)

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

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

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

Meta-well-typed

To show that $Π E - N$ is meta-well-typed, we show that both terms have the claimed type. First note,

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

and by ^P2, $𝐢 𝐝 . 𝑎 \circ 𝛾 = 𝛾 . 𝑎 [𝛾]$ . On the other hand,

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

Now ^P2 gives $𝐢 𝐝 . 𝑎 \circ 𝛾 = 𝛾 . 𝑎 [𝛾]$ , and ^P1 gives $𝛾 . 𝐴 \circ 𝐢 𝐝 . 𝑎 [𝛾] = 𝛾 . 𝑎 [𝛾]$ , so the types agree.

To see that $Π 𝜂$ is meta-well-typed, note

(V) Γ . 𝐴 ⊢ 𝐚 𝐩 𝐩 (𝑓 [𝐩], 𝐪) : 𝐵 [𝐩 . 𝐴 \circ 𝐢 𝐝 . 𝐪] (Π E) Γ . 𝐴 ⊢ 𝐚 𝐩 𝐩 (𝑓 [𝐩], 𝐪) : 𝐵 (= *) Γ ⊢ 𝜆 (𝐚 𝐩 𝐩 (𝑓 [𝐩], 𝐪)) : Π (𝐴, 𝐵) (Π I)

where $= *$ is conversion along the equality

𝐩 . 𝐴 \circ 𝐢 𝐝 . 𝐪 = (𝐩 \circ 𝐢 𝐝) . 𝐪 [𝐢 𝐝] = 𝐢 𝐝

which follows from ^P1 and $𝜂 𝐩 𝐪$ .

Internalizing judgemental structure

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 (Γ, 𝚷 Γ (𝐴, 𝐵)) ≅ T m (Γ . 𝐴, 𝐵)

also natural in $Γ$ . Translation directly into inference rules gives us almost exactly those given above, except that $Π E$ would look more like

Γ ⊢ 𝑓 : 𝚷 (𝐴, 𝐵) Γ . 𝐴 ⊢ 𝜆 - 1 Γ, 𝐴, 𝐵 (𝑓) : 𝐵 (Π E')

with the naturality rule

Δ ⊢ 𝛾 : Γ Γ ⊢ 𝑓 : 𝚷 (𝐴, 𝐵) Δ . 𝐴 [𝛾] ⊢ 𝜆 - 1 (𝑓) [𝛾 . 𝐴] = 𝜆 - 1 (𝑓 [𝛾]) : 𝐵 [𝛾 . 𝐴] (Π E' - N)

and the judgemental equality rules

Γ . 𝐴 ⊢ 𝑏 : 𝐵 Γ . 𝐴 ⊢ 𝜆 - 1 (𝜆 (𝑏)) = 𝑏 : 𝐵 (Π 𝛽')

Γ ⊢ 𝑓 : 𝚷 (𝐴, 𝐵) Γ ⊢ 𝑓 = 𝜆 (𝜆 - 1 (𝑓)) : 𝚷 (𝐴, 𝐵) (Π 𝜂')

These are however more awkward to use since they restrict the shape of contexts. The rules presented above are derivable from these by defining $𝐚 𝐩 𝐩 Γ, 𝐴, 𝐵 (𝑓, 𝑎) : = 𝜆 - 1 Γ, 𝐴, 𝐵 (𝑓) [𝐢 𝐝 . 𝑎]$ :

Proof

The derivation

Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝐢 𝐝 . 𝑎 : Γ . 𝐴 Γ ⊢ 𝑓 : 𝚷 (𝐴, 𝐵) Γ . 𝐴 ⊢ 𝜆 - 1 (𝑓) : 𝐵 (Π E') Γ ⊢ 𝜆 - 1 (𝑓) [𝐢 𝐝 . 𝑎] : 𝐵 [𝐢 𝐝 . 𝑎] Γ ⊢ 𝐚 𝐩 𝐩 (𝑓, 𝑎) : 𝐵 [𝐢 𝐝 . 𝑎] (=)

gives $Π E$ .

Noting that $𝛾 . 𝐴 \circ 𝐢 𝐝 . 𝑎 [𝛾] = 𝛾 . 𝑎 [𝛾] = 𝐢 𝐝 . 𝑎 \circ 𝛾$ by ^P1 and ^P2, the derivation

(Π - N) Δ ⊢ 𝜆 - 1 (𝑓) [𝛾 . 𝐴 \circ 𝐢 𝐝 . 𝑎 [𝛾]] = 𝜆 - 1 (𝑓 [𝛾]) [𝐢 𝐝 . 𝑎 [𝛾]] : 𝐵 [𝛾 . 𝐴 \circ 𝐢 𝐝 . 𝑎 [𝛾]] Δ ⊢ 𝜆 - 1 (𝑓) [𝐢 𝐝 . 𝑎 \circ 𝛾] = 𝜆 - 1 (𝑓 [𝛾]) [𝐢 𝐝 . 𝑎 [𝛾]] : 𝐵 [𝛾 . 𝑎 [𝛾]] (=) Δ ⊢ 𝐚 𝐩 𝐩 (𝑓, 𝑎) [𝛾] = 𝐚 𝐩 𝐩 (𝑓 [𝛾], 𝑎 [𝛾]) : 𝐵 [𝛾 . 𝑎 [𝛾]] (=)

gives $Π E - N$ .

The derivation

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

gives $Π 𝜂$ .

Noting $𝐢 𝐝 = 𝐩 . 𝐪 = 𝐩 . 𝐴 \circ 𝐢 𝐝 . 𝐪$ by ^P1, the derivation

(Π 𝜂') Γ ⊢ 𝑓 = 𝜆 (𝜆 - 1 (𝑓)) [𝐩 . 𝐴 \circ 𝐢 𝐝 . 𝐪] : 𝚷 (𝐴, 𝐵) (=) Γ ⊢ 𝑓 = 𝜆 (𝜆 - 1 (𝑓 [𝐩]) [𝐢 𝐝 . 𝐪]) : 𝚷 (𝐴, 𝐵) Γ ⊢ 𝑓 = 𝜆 (𝐚 𝐩 𝐩 (𝑓 [𝐩], 𝐪)) : 𝚷 (𝐴, 𝐵) (=)

gives $Π 𝜂'$ .

#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. ↩

𝚷-types

Standard presentation

Internalizing judgemental structure

Footnotes

$𝚷$ -types