Grothendieck Fibration

Definition

Let $\mathcal{E},\mathcal{B}$ be categories. Let $p:\mathcal{E}\Rightarrow \mathcal{B}$ be a functor. We call $p$ a bundle when it satisfies the following condition:

Definition

Let $\mathcal{E},\mathcal{B}$ be categories. Let $p:\mathcal{E}\Rightarrow \mathcal{B}$ be a functor. A morphism $\alpha :\mathcal{E}[X,Y]$ is Cartesian over $f:\mathcal{B}[pX,pY]$ iff

$$\begin{array}{rl}& \forall g:\mathcal{E}[Z,Y]\\ & \forall h:\mathcal{B}[pZ,pX]\\ & pg=f\circ h⟹\\ & \exists !\tilde{g}:\mathcal{E}[Z,X]\\ & g=\alpha \circ \tilde{g}\wedge p\tilde{g}=h\end{array}$$ Link to original

Fibration Condition

$p$ is a Grothendieck fibration iff

$$\begin{array}{rl}& \forall f:\mathcal{B}[b^{\prime },b].\\ & \forall Y:\mathcal{E}.\\ & p(Y)=b⟹\\ & \exists \alpha :\mathrm{Cartesian}[\mathrm{X},\mathrm{Y}].\\ & p\alpha =f\end{array}$$

Interpretation

• $\mathcal{E}$ is the total space (or total category).
• $\mathcal{B}$ is the base space (or base category).
• For an object $b:\mathcal{B}$, the fiber over $b$, denoted $p^{-1}(b)$ or ${\mathcal{E}}_b$, is the sub-collection of $\mathcal{E}$ mapping to $b$.
• In HoTT, a type family $B:A\to \mathcal{U}$ corresponds to a fibration ${\sum }_{x:A}B(x)\to A$.

Link to original