To complete the categorytheoretic interpretation of Zermelo type theory (Section 2.2), we need to discuss how to form a subtype from a predicate, and also to investigate the type W which names all of the propositions.
Comprehension The formation and elimination rules of {x: Xf[x]} resemble those of an existential quantifier, yielding a set instead of a proposition, and it behaves like Sx on its range. But the introduction rule for comprehension is different from that for sums. Comprehension turns a proposition into a type, so the effect is to move it across the division of the context in Section 9.2. It is like the singlekind Example 9.2.5, where the division was imposed arbitrarily.
Although {x:Xf[x]} is usually called a sub set, it is a common idiom to put two or more variables on the left of the divider, or none at all (Remark 2.2.7). In fact the formal rules also suggest that we should view comprehension as an operation on contexts. Then {Df} is the context D extended by a new type \propext f, which is what the proposition f becomes after its move across the division.
There is a very simple account of comprehension in terms of fibrations, which was, of course, found by Bill Lawvere [Law70]. It was rediscovered by Thomas Ehrhard [Ehr89] and considered further by Bart Jacobs [Jac90] and Du sko Pavlovi\'c [Pav90].
DEFINITION 9.5.1 In a generalised algebraic theory with divided contexts, the extent of a proposition f is the type \propext f with typeformation and indirect termformation (typeintroduction) rules



REMARK 9.5.2 The comprehension {Df} is the context [D,\propext f ]. The introduction rule (combined with cut) is then

omitted diagram environment
In particular, for D = [x:X] and G = [ ],

THEOREM 9.5.3 Let P:C® S be a fibration and P\dashv T with counit P·T = \id_{S} (Proposition 9.2.3). Then P interprets comprehension iff there is an adjoint T\dashv C, with counit ev and transposition k.
In other words, the way in which comprehension turns propositions into types is by a coreflection ( cf the support of a type, which is its reflection into propositions, Remark 9.3.13). Substitutioninvariance is automatic.
PROOF: From the above diagram, there is an adjoint correspondence:

Not all subobjects in the base category need arise by comprehension. Those that do form a class of support maps (Definition 5.2.10); indeed the notion of a class of supports corresponds to that of a fragment of logic in the propositional kind.
This account of comprehension, pretty though it is, does not explain its role in Zermelo type theory as a way of creating sets beside those definable with 1, x, N and P. Exercises 9.45ff describe three approaches.
The type of propositions In higher order logic, proposition and typeexpressions are handled as if they were terms. In a purely syntactic investigation such as [ Bar92], the colon notation a:U between terms and types can be extended to types and kinds U:type or f:prop, and even used to say things like prop:type or type:type.
With categorical interpretations in mind, we prefer to keep the term:type relationship a twolevel one, and distinguish the substance of a type (to which its terms belong) from its name considered as a term belonging to the type of types; the new types Prop and Type classify the kinds or classes of display maps prop and type respectively. (Per MartinLöf attributes these two approaches to higher order logic to Bertrand Russell and Alfred Tarski respectively.)
DEFINITION 9.5.5 A generic proposition w[z] involves translation of


for each well formed G\vdash f prop , there is some G\vdash a:Prop with G\vdash f º w[a], (Prop Á)
where the isomorphism is as usual expressed by operationsymbols


Recall from Theorem 8.2.16 that the substituted type w[a] is given by a canonical pullback, as in the diagram on the left:
omitted diagram environment
More concisely, for any propositional display f\hookrightarrow G there is some characteristic map a:G® Prop which makes the square on the right a (not necessarily canonical) pullback.
How does a depend on f? Since f is a proposition (or type) and not a term, there can be no operationsymbol f® a, so the rule (b) must be a scheme: the existence of a is asserted individually for each proposition f.
REMARK 9.5.6 Is the characteristic map a:G® Prop at least uniquely determined by the display f\hookrightarrow G? If it is then any isomorphic display y\hookrightarrow G must correspond to the same map a ( up to equality), since we have discarded the isomorphism (i,j) in the translation. This is an extensionality rule ( cf Definition 2.2.5 and Remark 2.8.4),


THEOREM 9.5.7 Prop is a support classifier (Definition 5.2.10) iff it satisfies comprehension, proof anonymity and extensionality.
PROOF: We must replace the proposition f by its extent, the type \propext f (Definition 9.5.1), as it remains to show that {z:Propw[z]} º 1. Consider any map G® {z:Propw[z]}, which corresponds to


Observe that any single display map generates a class of displays which satisfies Definition 9.5.5(a), by Example 8.3.6(j). Conversely, if a kind has a generic display w\hookrightarrow Prop then we may state the typetheoretic properties of the kind in terms of this instead of the whole class.
REMARK 9.5.8 Using the uniquely determined characteristic map, the connectives may be transferred from the propositions to their names, ie they define algebraic operations on Prop as in Remark 2.8.5. We write W for Prop, as in an elementary topos, when it classifies all monos (Definition 5.2.6); this happens exactly when the internal connectives and quantifiers for all types X exist ([ Tay98], Exercise 9.52).
omitted diagram environment
The displays on the left of each square are derived from the universal properties or proof rules of the typetheoretic connectives Ù, Ú and Þ : they are the product, coproduct and exponential in the context [x,y:W]. Then and, or and implies are defined by these diagrams, ie

REMARK 9.5.9 We may do the same for other support classifiers such as the Sierpi\'nski space (Definition 3.4.10, Example 5.2.11(d)). In this case the kind of propositions consists of open inclusions in Sp, for which we discussed existential quantification along open maps in Example 9.3.10. Although (w[x]Þw[y]) Ì SxS exists as a subspace, it is not open, or even locally closed (Example 9.4.12(c)). However, Barendregt's calculus allows us to juggle the kinds so that when " is applied to a geometric proposition it is called something else (not G_{d} , but something similar) and so is no longer a candidate for classification by S.
REMARK 9.5.10 There is a certain awkwardness in the typetheoretic rules for the powerset. In symbolic logic (where proofs and formulae alike are expressions) it is natural to repeat the term:type relationship as type:kind. This is also the practice in that tradition of category theory which is founded in algebraic topology (though not the one from logic), and it is unnatural to force isomorphisms into equalities. These considerations do not arise in first order logic, as equality is a matter between two terms relative to some type. But the extensionality law brings us back to the questions of equality versus interchangeability of mathematical objects in Section 1.2, so let's review its uses.
Extensionality was needed in older mathematical constructions because Zermelo type theory has very few connectives. Nowadays function and listtypes are used in functional programming to do many jobs previously done by the powerset (Exercise 9.55). However, Exercises 2.54 and 9.57 do depend on extensionality.
Set theory treats higher order logic metaphysically, model theory pretends that it doesn't exist, type theory bureaucratises it and category theory has no view which is identifiably its own. I feel that it does play an important part in mathematics, at least in the weak case of the Sierpi\'nski space, and that this needs to be explained [Tay98].