Simple Fibration

Let $\mathcal{C}$ be a Cartesian Category. The simple fibration $\mathrm{Simple}(\mathcal{C})\to\mathcal{C}$ is defined as:

• Objects: $\mathrm{Simple}(\mathcal{C})_{\Gamma}=\mathcal{C}_{0}$
• Morphisms: $\mathrm{\mathcal{C}}_{f}(X,Y)$ over $\sigma:\Gamma\to\Delta$ are morphisms $\mathcal{C}(\Gamma\times X,Y)$.
• The identity morphism is given by $\pi_{1}:\Gamma\times X\to X$.
• Composites of $f:\Delta\times Y\to Z$, $g:\Gamma\times X\to Y$ over $\sigma:\Delta\to\Theta$, $\delta:\Gamma\to\Delta$ are given by $f\circ\langle\delta\circ\pi_{0},g\rangle:\Gamma\times X\to Z$.

As the choice of names suggests, this fibration models a sort of simple type theory; morphisms in the base are substitutions, and morphisms upstairs are terms. Note that contexts play the role of types; this can be further refined by introducing the notion of CT-Structure, which essentially introduces an abstract Fibrancy condition to pick out the contexts that ought to be considered as types.

Cartesian Morphisms

A morphism $f:\Gamma\times X\to Y$ over $\sigma:\Gamma\to\Delta$ is Cartesian if and only if $\langle\pi_{0},f\rangle:\Gamma\times X\to\Gamma\times Y$ is invertible.