In the familiar predicate calculus, propositions may depend on elements of sets, but sets do not depend on the actual proofs of propositions. The technology used to take advantage of this separation principle predates the formal study of syntax: it was introduced for algebraic geometry in 1960 by Alexander Grothendieck [Gro64, Exposé VI], to handle the way in which an arbitrary mathematical structure (rather than simply a predicate) varies over an indexing space. John Gray developed the category theory [Gra66]. In 1970, Bill Lawvere applied it to what we would now call type theory, and Jean Bénabou used it to account for the infinitary aspects of category theory.
Separating propositions from types Instead of beginning, as is usual, with the formal definition of fibrations, let us first consider the feature of the predicate calculus which lies behind it (Remark 9.1.1(b)); Bart Jacobs called this a propositional situation [Jac90].
DEFINITION 9.2.1 Let S = S_{type}+S_{prop} be a partition of the class of types of a generalised algebraic theory L (Definition 8.1.10), the members of the second class being styled ``propositions.'' Then L is said to admit a division of contexts if



So certain converses of weakening hold. Using the exchange rule,


The point is that every jumbled context is isomorphic to a divided one.
We shall study the full subcategory Cn^{×}_{typeprop} Ì Cn^{×}_{L} of divided contexts. The conditions say that this inclusion is an equivalence, so our results about divided contexts actually apply to the whole category.
We shall write ® for the display maps corresponding to the types and \hookrightarrow for the propositions (Notation 9.1.3). According to the predicate convention, the latter are not necessarily monos.
LEMMA 9.2.2 Every pair of displays GfX® [l = 2.5em]^{[^(x)]}Gf\hookrightarrow [l = 2.5em]^{[^(y)]}G is part of a ( P) pullback,

PROOF: GfX º GX¢f by (a) and the R equation (Remark 8.2.8). The second diagram follows from (b) and uniqueness from (c). []
Parts (b) and (c) of Definition 9.2.1 say that, given a morphism of divided contexts, we may erase all propositional information: this is well defined as a functor, the fibration. So the tree structure in John Cartmell's contextual categories (Remark 8.3.9) may be pruned to the types. We write ® for the fibration, as it ``displays'' propositions over types.
PROPOSITION 9.2.3 Let Cn^{×}_{type} be the full subcategory consisting of those contexts which only involve types. Then there are adjoint functors,
omitted diagram environment
where P forgets the propositional part of a divided context and T gives an empty propositional part to a typeonly context. Cn^{×}_{typeprop} is called the total category and P the fibration.
For each object G of Cn^{×}_{type } (known as the base category), the fibre is the relative slice Cn^{x}¯ G, whose objects are contexts of the form [GF] and whose morphism act as the identity on G. TG º [G] is the terminal object of the fibre over G.
u^{*}: Cn^{x}¯ G® Cn^{x}¯ D for u:D® G; moreover
(u;)^{*} f = u^{*}(^{*}f) and id^{*}f = f.
PROOF: Notice that P cannot be defined for types which depend on the omitted propositional variables. The other two parts of Definition 9.2.1 are needed to define P on morphisms involving type operationsymbols, such that the laws are respected. The substitution functors were defined in Section 8.2 and TG is terminal in the relative slice by Lemma 8.2.10. []
S = S_{type}+S_{prop} such that Definition 9.2.1(b) holds, ie if K\triangleright t Î S_{type} then already \dgmK_{type} º KÇS_{type}\triangleright t. Let L_{ type} be S_{type} with the restriction of \triangleright . Then there is a division of the contexts in the classifying semilattice of L (Theorem 3.9.1).
EXAMPLE 9.2.5 An Iindexed family of objects (\typeX_{i})_{i Î I} is a context

Jean Bénabou explained how the dependent sum Si:I.X[i] and product Pi:I.X[i], which we study in the next two sections, give an elementary axiomatisation of coproducts and products of infinitary indexed families of sets or other mathematical objects. We regard X[i] and Si.X[i] as idiomatic notation for the associated display map. The previous chapter developed this notation and its formal interpretation.
In practice, more than one such suffix (i:I, j:J, ...) is often needed, so it is better to write [G  x:X] than to collect I, J, ... as a single type IxJ or Si:I.J[i] (category theory exists to eliminate suffixes from mathematics). There may also be several Iindexed families (\typeX_{i}), (\typeY_{i}), ..., from which we may for example need to select tuples, so these too we keep together in the manytype divided context [GF].
I find this example very confusing as the main use used to demonstrate the theory of fibrations, for one thing because the category of sets is too special to illustrate many of the difficulties, such as the BeckChevalley condition and quantification over equality (Remark 8.3.5). But, in terms of our definition, lemma and proposition above, how can the principle of independence possibly apply, when the types on both sides of the division are of the same kind (sets)? Making such a division cannot be expressing any semantic fact about the theory of sets: it is a convention:
we don't use elements of indexed sets as indices.
In the process of inventing a formal language with divided contexts that uses displays of sets on both sides, we ``taint'' the displays by their use in the two roles: we take the same class twice, or one class and a subclass M of it, and mark the copies as ``types'' and ``propositions.'' Then the formal language ( ie the arguments we permit ourselves to write in it), is artificially restricted according to the rules in Definition 9.2.1. The axiom of comprehension forgets this restriction (Section 9.5).
Fibrations The ``substitution'' functors have a universal property, which (like adjunctions) we may capture without making choices of them.
DEFINITION 9.2.6 Let P:C® S be any functor.
PF = PY = G and Pg = \id_{G} in C is called vertical. The subcategory P^{1}(G) is known as the fibre over G; its objects are those F Î obC with
PF = G and its maps are the vertical ones. A morphism that is merely made invertible by P (not necessarily an identity) is called pseudovertical.
 = P\nearrow :D = P Y® X = P Q: given any map F® Q whose image factors into  in the sense of forming a commutative triangle in S as illustrated, there is a unique fillin F® Y such that the upper triangle commutes and the image is the given map G® D.
:D® X = P Q in S there is a prone lifting \nearrow :Y ® Q with P Y = D and P\nearrow = . In this case the source, C, and target, S, of P are called the total category and base category respectively. omitted diagram environment
So P:C® S is an opfibration iff P:C^{op}® S^{op} is a fibration.
PROPOSITION 9.2.7 Let \nearrow [thick]():S^{op}® Cat be any functor, where we write u^{*}:\nearrow [thick](D)® \nearrow [thick](G) instead of \nearrow [thick](u) for the action of maps in S. Then the following define a fibration P:C® S:
omitted diagram environment

PROOF: Associativity of composition in C depends on functoriality of \nearrow [thick](). The mediator for [u;f] in the universal property of the prone map [id] is [g]. Conversely if [g] is prone then g is invertible, since [uid] is also prone. Everything else in the definition of fibration is straightforward. []
EXAMPLES 9.2.8 As the data for Proposition 9.2.7 consist merely of an assignment of a category to each object of the base category (in a functorial way), examples of fibrations are not difficult to find.
PROPOSITION 9.2.9 Let L_{type} Ì L be generalised algebraic theories, one a conservative extension of the other. Then there is a bifibration of their categories of models, which has adjoints on both sides.
omitted diagram environment
Let u:R® S be a homomorphism in the subtheory ( L_{type}).

S = S_{type}+S_{prop} be a divided Horn theory, M,N Ì S two closed subsets and u:R = MÇS_{type} Ì S = NÇS_{ type}. Then the initial algebra in the fibre over R is the closure of R with respect to the larger theory; the final one is R+S_{prop}. The restriction of N is R+NÇS_{ prop}, and the induction of M is the closure of MÈS.
For finitary theories, the restriction functors preserve filtered colimits. Restriction and induction maps between algebraic lattices are called projections and embeddings respectively (Exercises 9.10ff). []
Coherence issues For any (``semantically given'') fibration, a choice of prone liftings \nearrow :Y® Q for each  and Q is called a cleavage, and extends to ``substitution'' functors ^{*} between fibres. A split fibration is one for which these act functorially, as they do for syntactic categories. In general, the natural isomorphisms between (u;)^{*} and u^{*}·^{*} in a cleavage must be specified, and obey a system of coherence laws.
These isomorphisms are defined by universal properties, so are uniquely determined by certain equations. However, as Jean Bénabou rather forcefully pointed out [B \' en85], there is a casual tendency just to call them ``canonical''  as if this were an intrinsic property like continuity. The problem is that if isomorphisms are not kept under strict control, they conspire to form nontrivial groups.
PROPOSITION 9.2.11 A group homomorphism P:C® S is a fibration iff it is surjective, and the fibre over the unique object of S is the kernel,

REMARK 9.2.13 Let [`(u)] Î C be a cleavage, ie a choice of preimages (prone liftings) for each u Î S. This is also known as a transversal for the normal subgroup K\triangleleftC. Then



Example 9.2.12(d) is a topological group. In this case, the base S^{1} can be covered by open subsets (in the sense of Section 3.9) for each of which the two square roots may be distinguished continuously. The indexation is now over the frame W(S^{1}) of open subsets of the circle, but it is also necessary to say how these (and things defined over them) are pasted together with respect to the coverage. A fibration which respects this pasting is called a stack, or champs in French. (The French for a field of numbers is corps, but beware that Bénabou has used the word corpus in yet another sense!) For an account of the Grothendieck school's approach to fibred categories, see [Gir71], in which Jean Giraud studies nonAbelian cohomology of topological groups up to dimension 3. []
Stacks arise in type theory too, for example to say that S^{2} @ S¯ 2, respecting the coproduct 2 = 1+1, cf Exercise 9.20 . They were also used by Hyland, Robinson and Rosolini [ HRR90] to state precisely the completeness of the category of modest sets (Example 7.3.2(l)).
In type theory, Bénabou's criticism has been (misunderstood and) a source
of confusion  for syntactically defined indexed structures,
the substitutions really are functorial on the nose, and the group
theoretic issues do not arise. The more difficult technology of fibrations
has been employed where the simpler indexed one would have been enough. Even
for semantics, we saw in Sections 7.6 and
8.4 that there is an equivalent syntactic category:
Exercise 9.17 provides a similar construction
for fibred versus indexed categories. One should not try to
choose product, substitution functors, etc but work instead
in the syntactically constructed category, taking the results back along
the weak equivalence.