Fibration

A fibration is a family of related notions in which some structure lies over a base, and movement or data in the base can be lifted, reindexed, or transported in the total object. The word is used differently in topology, category theory, simplicial homotopy theory, and type theory. These notions share a fibrewise intuition, but they are not all instances of one elementary definition.

Main meanings

Category theory

• Grothendieck Fibration: a functor $p:\mathcal{E}\to \mathcal{B}$ with cartesian lifts of morphisms in the base. See extra structure: Cloven Fibration, Split Fibration.
• Opfibration: the dual notion, using cocartesian lifts.
• Discrete Fibration: a special case where lifts are unique.
• Cartesian Fibration: higher-categorical generalisation (e.g. in ∞-categories).
• Cocartesian Fibration: the dual higher-categorical notion.
• Street Fibration: a 2-categorical generalisation.
• Examples: Codomain Fibration, Simple Fibration, Family Fibration.

Topology and homotopy theory

• Topological Fibration: overview of fibration notions in topology.
• Hurewicz Fibration: a continuous map with the homotopy lifting property against all spaces.
• Serre Fibration: a continuous map with the homotopy lifting property against disks/CW-complexes.
• Kan Fibration: a map of simplicial sets with horn fillers.
• Fibre Bundle: a locally trivial fibration with specified fibre and structure group.

Type theory

• A dependent type $B:A\to \mathcal{U}$ may be regarded as a fibration over $A$.
• The associated projection is ${\pi }_1:{\sum }_{x:A}B(x)\to A.$

Sets

• A function $p:E\to B$ determines fibres $E_b=p^{-1}(b)$.
• This is better treated as a Set-Indexed Family or Family of Sets unless a specific source calls it a fibration.

Common intuition

The base object indexes fibres, and the fibration structure controls how data over one base point relates to data over another (via lifting, reindexing, or transport).