A fibered category is a small fibration if it is equivalent to a fibered category which is obtained via a specific construction: the input is an internal category in a category with pullbacks, and the output is a fibered category , whose fiber over an object (“index set”) in is the small category whose object part is and morphism part is ; and the structure maps of are obtained by postcomposing with structure maps of .
Conventions for the internal category : the composition takes arguments in Leibniz convention, and source map is the right leg of the span ; the projection have . Thus .
Consider objects and in fibers over and . Morphisms in are pairs where and are morphisms in satisfying , . The interesting part of the construction is the composition: given also and , their composition is where is the composition and is the map given by the universal property of the fibered product and and . One checks that so defined composition is associative.
Finally, the projection is rather obvious: , and in notation from above, . One checks that is a fibered category with a canonical cleavage: the chosen cartesian morphism over with given target is . Indeed, for any object over and a morphism with , one can decompose where is a morphism in with .
The basic example is the small fibration of set-indexed families of objects in , for a small category . The objects in the fiber , that is the functions , are the -indexed families of objects in . A map is a map together with an -indexed family of morphisms in . The composition is .