This section, which is an extended introduction to the chapter, sets up certain conventions for the way in which we shall use the familiar notation of the predicate calculus to explain a much more general and abstract theory. This overview is closer than is the rest of the chapter to Bill Lawvere's treatment of the semantics and Per MartinLöf's of the syntax of type theory. We shall also show how the quantifiers fit into the general recursive scheme for constructing and interpreting type theory.
Throughout the book we have stressed the formal analogy between types and propositions. The only distinction between them in Chapter VIII, which set up the algebraic formalism for dependent types and its relationship with category theory, was the rather superficial one that proofs of propositions are not distinguished, so their displays are mono.
REMARK 9.1.1 The theme of this chapter is not the extensional difference between all maps and monos, but the separate roles which sets and propositions play in the quantifiers, comprehension and powerset.
We say that sets and propositions are types of two kinds (some authors say sort or order). These differences and the generality of which they are examples are sometimes presented in an extremely abstract way. Henk Barendregt uses *, [] and like symbols for kinds in describing his pure type systems [Bar92]. We end up proposing the use of such a formalism for semantic reasons, but we will keep the familiar terminology of the predicate calculus for the sake of motivation.
CONVENTION 9.1.2 However, we employ the words ``proposition'' and ``type'' as variables. In each section, these kinds are only required to obey the conditions of that particular section. They may in fact stand for the same kind  f may be a type like X  but we use this predicate convention to show where they are potentially different. What we say in propositional notation applies mutatis mutandis to types  in fact simply by transliteration of X for f etc .
Like characters in a Greek tragedy, prop, type, * and [] act out dramas about the essential interactions of things, in which their own identity is not relevant. In particular, the principle (a) of proofanonymity is only used at one point in this chapter, namely in the discussion of the hrule for the powerset (Remark 9.5.6). Assuming proofanonymity would in fact make the second half of Section 9.4 pointless.
Classes of display maps Chapter VIII set up the interpretation of types in context ( G\vdash X type) as pullbackstable ``display maps'' X® G. The partition of the class of all types into various kinds is handled by equipping the category with two or more classes of displays.
NOTATION 9.1.3 Following the predicate convention, we shall write
([G,x:X]® ^{[^(x)]}G) Î D and ([G,f]\hookrightarrow G) Î M
for sets and propositions respectively. But this is only a convention:
\hookrightarrow does not necessarily signify an injective function,
because this would mean that proofs were anonymous, which, as we have said, we shall usually not assume. There are, for example, realisability models of the predicate calculus in which proofs are distinguished and displays for propositions are not monos.
Note that nothing that we did in Chapter VIII mixes up the two classes, since there we considered displays one at a time. This unary closure condition gave rise to the []modality ``stably'' in Example 8.3.6(k). It is the union of the kinds to which Theorem 8.4.10 refers.
The same semantic display map may belong to several classes, and be used as the interpretation of types of different kinds. In particular, we shall set out the theory of the existential quantifier and the type of propositions in detail, and deduce that of the dependent sum and type of types from it by substituting M = D and prop = type. Proofanonymity is itself the parameter which distinguishes $ from S as we understand them semantically, so of course we are careful not to assume it.
Fibrations We shall continue to work in the category of contexts and substitutions developed in the previous chapter, but now these contexts consist of types and propositions.
REMARK 9.1.4 Do not confuse [x:X,y:f[x]] with {x:Xf[x]} , which is the subset formed by comprehension. Compare the ``virtual objects'' consisting of programvariables and midconditions introduced in Remark 5.3.3: semantically, a context is not just a set but a subset of a particular ``ambient'' set. The semantics of the category of contexts is not Set but the comma category M¯ Set (Definition 7.3.8).
Until Section 9.5, where we consider comprehension as a typeforming operation, this means that the essential logical information is in a sense duplicated in the category. Exercise 9.9 explains how the results in Section 9.3 about factorisation systems in M¯ S relate to S itself.
omitted diagram environment
REMARK 9.1.5 Cn^{×}_{type}, which consists of setonly contexts, is called the base category. For each set (or each context G consisting only of sets), there is a subcategory of this big category that consists of the predicates f[[(x)\vec]] over G; it is called the fibre P(G). For each function u:G®D, there is a substitution or inverse image functor u^{*}:P(D)® P(G); the assignment u® u^{*} provides a functor P():(Cn^{×}_{type})^{op}® Cat, which is known as an indexed category. The big category Cn^{×}_{typeprop} whose contexts consist of both types and propositions collects all of these fibres together. There's a propositionerasing functor P:Cn^{×}_{typeprop}® Cn^{×}_{type}, called a fibration. Beware that P and P are in different typefaces!
Bill Lawvere and Jean Bénabou used fibrations to study the quantifiers and infinitary limits and colimits. We show in Section 9.2 that fibrations capture the independence of types from propositions (Remark 9.1.1(b)), but this is not relevant to the quantifiers (it is to comprehension).
The quantifier formation rules As for the predicate and lcalculi (Sections 1.5 and 2.3), we present the syntactic rules for the quantifiers in both the box and sequent styles.
REMARK 9.1.6 The quantifier formation rule binds a variable, so the box begins with a contextformation (Definition 8.2.2).

The indirect ("Á ) and ($E )rules define terms
lx.p and let(x,y)bec inf
which bind the variables x and y, so they are subject to a equivalence, as are the type formation rules. Corresponding to the formation rules, there are also type and term equality rules, such as

As in Section 1.6, types and terms may be imported into boxes from above, and exported if wrapped in the quantifier or indirect operation.
Adjointness in foundations These are symbolic trivia: what we really want to know is how the indirect, b and hrules correspond to the universal properties of ve and ev.
REMARK 9.1.7 Bill Lawvere finally brought symbolic logic into the heart of mathematics by recognising the bijective correspondences


REMARK 9.1.8 Since universal properties describe objects in category theory only up to isomorphism, we shall understand notation such as $x.f in the same way: it means any object y which satisfies the introduction, elimination, b and hrules for an existential quantifier for the predicate f[x] over the type X. This need not be the string ``$x.f,'' just as X® Y in Section 4.7 did not have to be literally an arrow. In fact the symbolic rules also characterise y only up to isomorphism.
Following the preference stated in Chapter VII, we shall discuss the universal properties of the quantifiers diagrammatically, instead of using Lawvere's adjunctions.
Substitution and the BeckChevalley condition We are used to substituting directly under the quantifiers: Definition 1.1.10(d) said that u^{*}$x:X.f is equal to $x:u^{*}X.u^{*}f. We don't state such a rule here because to assert equalities between types may conflict with their possibly different histories of formation.
REMARK 9.1.9 Instead of asserting a substitution rule directly for the types, we give stronger indirect rules for the terms. Then, as for all universal properties, we prove that u^{*}Qx:X.f º Qx:u^{*}X.u^{*}f, in a unique way which commutes with the structure.
Categorically, the contexts involved form a pullback as shown on the left,
omitted diagram environment
and we want the diagram on the right to commute, in the sense that a certain natural transformation (provided by the universal properties of Qx_{G} and Qx_{D} ) is invertible. This equation between types is known as the BeckChevalley condition, although it was Lawvere and Bénabou who identified it in categorical logic, respectively attributing it to Jon Beck and Claude Chevalley because of analogous properties in their work in the descent theory of algebraic geometry.
This property is often presented as an additional burden: something extra to be checked after the already heavy labour of the construction of the concrete objects to be used in the interpretation. Of course, if you choose to define the quantifiers categorically as the adjoints to substitution, then this condition does need verification. But we give another characterisation of " with the condition built in, so it can do the work for us: we choose the values of quantifiers of the form "x:X.f where X and f are type and proposition symbols, and then the substituted forms "x:u^{*}X.\nearrow ^{*}f are derived from the BeckChevalley condition.
The recursive definition of interpretations Theorem 8.4.4 showed how to use the history of formation of types and terms to interpret generalised algebraic theories in categories with display maps.
REMARK 9.1.10 The quantifiers and their terms contribute new cases to this structural recursion, just as the simply typed lcalculus in Remark 4.7.4 extended the interpretation of algebra in categories with products. By the recursion hypothesis, we already have

REMARK 9.1.11 For the sake of making [[]] into a bona fide functor, let us consider briefly how to choose a particular object from the isomorphism class which the universal property provides. In Zermelo type theory (Remark 2.2.4) this may be done by fiat for $, as comprehension names canonical subsets for the image factorisation.
The formal rules as we give them say that the BeckChevalley condition only holds up to unique isomorphism, even in the syntax. Without some trick, $x:X.f must be regarded as a new proposition symbol, even when X and f are type expressions: f^{*}$x:X.f is a substitutioninstance of it, but $x:f^{*}X.f^{*}f is not.
We would like to find some way of prescribing interpretations to make the BeckChevalley condition hold up to equality. Although we have introduced it semantically, this is really a symbolic problem: does cut or substitution commute with the type formation rules? If it does then once again we need only choose the results of quantification at type symbols. Recall that Theorem 8.4.4 did this for unquantified typeexpressions: given a choice of semantic displays at typesymbols, it used pullbacks anchored there to interpret typeexpressions.
Since f^{*}\propext (\nearrow ^{*}f) = (f;\nearrow )^{*}\propext f, there is no difficulty with comprehension (or the powerset). In the cases of $ and ", substitutions may be embedded in two places: for the range and the body. Corollary 9.4.15 shows that
