Discrete Cartesian Fibration

A Displayed Category $\mathcal{E}\rightarrowtriangle\mathcal{B}$ is a discrete cartesian fibration if:

• $\mathcal{E}$ has a H-Set of objects over each $I:\mathcal{B}$.
• For every $u:{{I}\to{J}}$ and $X:\mathcal{E}_{J}$, there exists a unique lift

$(u^{*}(X):\pi_{u,X}:\mathcal{E}_{I},{{u^{*}(X)}\to_{u}{X}})$.

Discrete cartesian fibrations $\mathcal{E}\rightarrowtriangle\mathcal{B}$ are the displayed analogs of a Presheaves $P:\mathcal{B}^{mathrm{op}}\to\mathrm{Sets}{.}$. The key difference is that presheaves opt to encode the functorial action of $\mathcal{B}$ on the family of sets via a function, whereas discrete cartesian fibrations encode the action using a Functional Relation.

This can have some benefits when working with the semantics of type theory, as we get to avoid Green Slime problems arising from trying to index data by the action of a substitution.

Properties

• Every morphism in $\mathcal{E}$ is Cartesian, and thus every discrete cartesian fibration is a Right Fibration.

• There is a morphism ${{X}\to_{u}{Y}}$ over $u:{{I}\to{J}}$ if and only if $u^{*}(Y)=X$.

  The "if" direction follows directly from transporting the projection $\pi_{u,Y}:{{u^{*}(Y)}\to_{u}{Y}}$ along the path $u^{*}(Y)=X$.

  For the "only if" direction, suppose we had some $p:{{X}\to_{u}{Y}}$. Note that both $(X,p)$ and $(u^{*}(Y),\pi_{u,Y})$ form candidate lifts of $Y$ along $p$, so $u^{*}(Y)=X$.