Page "Fibred category" Paragraph 0

Fibred categories are abstract entities in mathematics used to provide a general framework for descent theory.

They formalise the various situations in geometry and algebra in which inverse images ( or pull-backs ) of objects such as vector bundles can be defined.

As an example, for each topological space there is the category of vector bundles on the space, and for every continuous map from a topological space X to another topological space Y is associated the pullback functor taking bundles on Y to bundles on X. Fibred categories formalise the system consisting of these categories and inverse image functors.

Similar set-ups appear in various guises in mathematics, in particular in algebraic geometry, which is the context in which fibred categories originally appeared.

Fibrations also play an important role in categorical type theory and theoretical computer science, particularly in models of dependent type theory.