Fibration

Definition

A fibration is a map equipped with a lifting property against a specified class of paths or morphisms. Let $\mathcal{E}$ and $\mathcal{B}$ be categories (or spaces). Let $p:\mathcal{E}\to \mathcal{B}$ be a functor (or continuous map). We call $p$ a fibration when it satisfies a specific lifting property, allowing movement in the base $\mathcal{B}$ to be lifted to movement in the total space $\mathcal{E}$.

Varieties

Categorical

• Grothendieck Fibration (lifts morphisms)
• (Co)Cartesian Fibration
• Discrete Fibration
• Street Fibration

Topological / Homotopical

• Kan Fibration (lifts horns)
• Serre Fibration (lifts discs)
• Hurewicz Fibration (lifts all spaces)
• (Co)Tangent Bundle (special case of vector bundle)
• Principal G-bundle

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

References

• [[Jacobs, B. (1999). Categorical Logic and Type Theory.]]
• [[Riehl, E. (2014). Categorical Homotopy Theory.]]