Dependent Types and Fibrations

Appendix C

3 min read

Dependent Types and Fibrations

Types that vary with context require machinery that tracks the variation. A query valid against one schema is nonsense against another; a recommendation "best" for one user is irrelevant to the next. This appendix provides the formal vocabulary: dependent types from type theory and fibrations from category theory.

Dependent Types

Dependent Type

A dependent type is a family of types indexed by values of another type. If $B$ is a type and $P : B \to \mathcal{U}$ assigns a type $P(b)$ to each $b : B$ , then $P$ is a dependent type over $B$ . The fiber over $b$ is the type $P(b)$ .

Π-Type (Dependent Product)

Given $B$ and $P : B \to \mathcal{U}$ , the Π-type $\Pi_{b : B} P(b)$ is the type of functions that, given any $b : B$ , return a value of type $P(b)$ . When $P$ is constant, this reduces to the ordinary function type $B \to P$ .

Σ-Type (Dependent Sum)

The Σ-type $\Sigma_{b : B} P(b)$ is the type of pairs $(b, p)$ where $b : B$ and $p : P(b)$ . When $P$ is constant, this reduces to the ordinary product $B \times P$ .

Π-types correspond to universal quantification ( $\forall b.\, P(b)$ ); Σ-types to existential quantification ( $\exists b.\, P(b)$ ) with a witness. This is the propositions-as-types correspondence.

Fibrations

Fibration

A functor $p : \mathcal{E} \to \mathcal{B}$ is a fibration if it satisfies the lifting property: for every morphism $f : B' \to B$ in $\mathcal{B}$ and every object $E$ in $\mathcal{E}$ with $p(E) = B$ , there exists a cartesian lift of $f$ to $\mathcal{E}$ . The fiber over $B$ is the subcategory $\mathcal{E}_B$ of objects mapping to $B$ .

Reindexing

Given a fibration $p : \mathcal{E} \to \mathcal{B}$ and morphism $f : B' \to B$ , the reindexing functor $f^* : \mathcal{E}_B \to \mathcal{E}_{B'}$ sends objects in the fiber over $B$ to objects in the fiber over $B'$ . This is the functorial version of substitution.

Correspondence

Type Theory	Fibration
Type family $P : B \to \mathcal{U}$	Fibration $p : \mathcal{E} \to \mathcal{B}$
Fiber $P(b)$	Fiber category $\mathcal{E}_b$
Substitution $P[f]$	Reindexing $f^*$
Π-type $\Pi_{b:B} P(b)$	Right adjoint to reindexing
Σ-type $\Sigma_{b:B} P(b)$	Left adjoint to reindexing

The Third Mode's predicates are fibered: "valid query" depends on schema, "best option" depends on preference context, "permitted action" depends on authorization context. Fibrations make this dependence explicit and reindexing coherent. See A14.

← Back to Appendices Back to The Proofs →