Fibrations

Origin. Grothendieck (SGA1, 1961); Bénabou systematized the theory (1985). Also called fibered categories. Indexed categories via fibered categories. Dependent types categorically. Foundation for categorical type theory.

Models. Total category E fibered over base B. Fibers E_b over objects b. Cartesian morphisms: reindexing. Dependent sums and products as adjoints.

Formalism.

Fibration: p : E → B functor Cartesian lifting for all f : a → b and e ∈ E_b.

Cartesian morphism: g : e' → e in E is Cartesian over f : a → b iff any h : e'' → e with p(h) = f ∘ k factors uniquely.

Fiber: E_b = p⁻¹(b): objects over b. Forms category.

Reindexing: f : a → b gives f* : E_b → E_a Pulling back along f.

Cleavage: Choice of Cartesian liftings. Pseudofunctorial: f* ∘ g* ≅ (g ∘ f)*

Split fibration: Cleavage strictly functorial. f* ∘ g* = (g ∘ f)*

Type theory: Contexts B, types over contexts E. Substitution = reindexing. Dependent products/sums = adjoints.

Simple fibration: B × C → B projection. Non-dependent types.

Comprehension: {}: E → B/p (slice category) Types as objects with display maps.

Display maps: Distinguished fibrations for type theory. Context extension by a type.

Symbols.

Symbol	Unicode	Name	Meaning
→	U+2192	Arrow	A functor or a morphism, as in p : E → B
∘	U+2218	Composition	Composite of morphisms, or of reindexing functors
≅	U+2245	Isomorphism	The coherence iso f* ∘ g* ≅ (g ∘ f)* of a cleavage
≃	U+2243	Equivalence	Fibrations over B ≃ pseudofunctors B^op → Cat
∈	U+2208	Membership	An object e of the fibre E_b
×	U+00D7	Product	The simple fibration B × C → B
⁻	U+207B	Superscript minus	In the fibre notation p⁻¹(b)
¹	U+00B9	Superscript one	In the fibre notation p⁻¹(b)
p : E → B	—	Fibration	Projection from total category to base
E_b	—	Fibre	The category of objects over b
f*	—	Reindexing	Pullback functor E_b → E_a along f : a → b
Cart	—	Cartesian	Lifting morphism with the universal factorization
B^op	—	Opposite category	Source of the indexing pseudofunctor
Cat	—	Category of categories	Target of the indexing pseudofunctor
{ }	—	Comprehension	Functor sending a type to its display map
B/p	—	Slice	Objects of the base equipped with a map

Metatheory. The Grothendieck construction is an equivalence of 2-categories between fibrations over B equipped with a cleavage and pseudofunctors B^op → Cat; split fibrations correspond to strict functors. Every fibration is equivalent to a split one, and the inclusion of split fibrations into fibrations has both a left and a right adjoint, which is what makes strictification possible. The codomain functor cod : B^→ → B is a fibration exactly when B has pullbacks, and it is not split, since pullbacks are determined only up to isomorphism — this is the coherence problem for the semantics of dependent type theory, addressed by Curien (1993) and Hofmann (1994). Jacobs' comprehension categories (1993) and his Categorical Logic and Type Theory (1999) give the fibrational account; split comprehension categories with unit, categories with families (Dybjer 1996) and contextual categories (Cartmell 1978) are equivalent presentations. The Bénabou–Roubaud theorem (1970) identifies descent along an effective descent morphism with monadicity of reindexing.

Applies to. Dependent type theory. Categorical logic. Algebraic geometry. Stack theory. Topos theory.

Limitations. Choosing a cleavage requires the axiom of choice, so the correspondence with indexed categories is not available without it. The codomain fibration, the one that naturally models dependent types, is not split: substitution is only pseudofunctorial, and the interpretation of type theory is ill-defined until a splitting is imposed, which replaces the concrete fibres by larger presheaf-style ones. Dependent sums and products exist only when reindexing has adjoints, and the Beck–Chevalley condition relating them to substitution must be imposed as a separate axiom rather than following from the fibration structure. Over a large base neither the fibres nor the total category are small, so the theory is not internalizable without size restrictions — Bénabou's objection to indexed category theory. The framework is 1-categorical, and the (∞,1)-analogue requires straightening and unstraightening rather than the Grothendieck construction.