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
p : E → B	—	Fibration	Projection
E_b	—	Fiber	Over b
f*	—	Reindex	Pullback functor
Cart	—	Cartesian	Lifting morphism

Metatheory. Grothendieck construction: fibrations ≃ pseudofunctors B^op → Cat. Equivalence: fibrations ↔ indexed categories. Comprehension categories. Classifying fibrations. Descent theory. Internal language.

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

Limitations. Abstract. Size issues. Strictness vs weakness. Category theory prerequisite.