Practical Foundations of Mathematics

Paul Taylor

9.5  Comprehension and Powerset

To complete the category-theoretic 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: X|f[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 single-kind Example 9.2.5, where the division was imposed arbitrarily.

Although {x:X|f[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 {D|f} 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 type-formation and indirect term-formation (type-introduction) rules

REMARK 9.5.2 The comprehension {D|f} 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 co-unit P·T = \id_S (Proposition 9.2.3). Then P interprets comprehension iff there is an adjoint T\dashv C, with co-unit ev and transposition k.

In other words, the way in which comprehension turns propositions into types is by a co-reflection ( cf the support of a type, which is its reflection into propositions, Remark  9.3.13). Substitution-invariance is automatic.

PROOF: From the above diagram, there is an adjoint correspondence:

EXAMPLES 9.5.4

(a)

In the predicate calculus, where the class M of propositional displays consists of monos in Set, the total category Cn^×_{type| prop} is M¯ Set. The maps of this category are commutative squares whose verticals are mono. Such squares are prone iff they are pullbacks (hence the alternative name cartesian). The fibres are P(G) = W^G . omitted diagram environment

(b)

In Example 9.2.5 the division of the context is an arbitrary one between an indexing set I and the sets X[i] which it indexes. This can be described in the same way with M = Set, so any four maps may form the commutative square. The comma category Set¯ Set is the same as the functor category S^® , the fibration functor P being tgt, so this is known as the codomain (target) fibration. The fibre over G is Set¯ G and the adjoints in this case (and the previous one) are given by X® \id_X and src. The slice Set¯ G is equivalent to the functor category Set^G , cf extensive categories if G = 2 (Section  5.5).

(c)

Let S = Cat and \nearrow [thick](G) = Set^G ; then the comprehension functor gives discrete op-fibrations [Law70, SW73].

(d)

Not all comprehension fibrations are like this. The fibration P of the category of rings-with-modules over rings (Example  9.2.10(a)) has comprehension, but it is trivial: C = P (since T gives the zero module, we have T\dashv P as well as P\dashv T). []

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 type-expressions 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 two-level 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 Martin-Lö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

(a)

names into propositions, using a special dependent proposition

z:Prop\vdash w[z] prop, (Prop  E)

dependent on a new type

\vdash Prop type

of names of propositions;

(b)

and propositions into names:

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 operation-symbols

G,x:f\vdash i(x):w[a]        G,y:w[a] \vdash j(y):f

and laws (Prop  b)

G,x:f\vdash j(i(x)) = x:f       G,y:w[a] \vdash i(j(y)) = y:w[a].

See Exercise 9.51 for another version of this rule.

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 operation-symbol 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:Prop|w[z]} º 1. Consider any map G® {z:Prop|w[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 type-theoretic 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 type-theoretic 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 type-theoretic 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.

(a)

Suppose we have a type of proof-anonymous propositions that does not necessarily satisfy (Prop  h). Then there is an extensional such type W iff every equivalence relation on any type has an effective quotient ( cf  Example  2.1.5 and Proposition  5.6.8).

(b)

Proposition 3.1.10 used equivalence relations to reduce any preorder such as (Prop,\vdash ) to a poset. We went on from there to discuss the Yoneda embedding, but from Chapter IV onwards we used this quite successfully for non-skeletal categories.

(c)

The extensional lattice of ideals of a ring (Example  3.2.5(f)) must often be replaced by its non- skeletal category of modules, and for algebraic rather than logical reasons. For example, the ring may have an automorphism such as x® x^p that does not act faithfully on the lattice.

(d)

Let x = (L,U) and y = (M,V) be Dedekind cuts (Example  2.1.1) bearing the same relation to all rationals, ie "q:Q.q Î LÛ q Î M and similarly for U and V. If f:\realno_D® Q is continuous then its values on Q force f(x) = f(y), without extensionality (x = y).

Extensionality was needed in older mathematical constructions because Zermelo type theory has very few connectives. Nowadays function- and list-types 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].