Dependent Types and Fibrations

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)$.

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$.

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$.

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$ has the objects mapping to $B$ and the arrows mapping to $\mathrm{id}_B$.

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