Practical Foundations of Mathematics

Paul Taylor

8.3  Display Categories and Equality Types

This section investigates the semantic structure needed to interpret the syntax of the previous two sections. We shall see that there are many naturally occurring examples of it in general topology and elsewhere, so one of the aims in setting out these ideas is to encourage topos theorists and others to adopt the notation of dependent type theory.

The structure requires less than that the semantic category have all finite limits, and we show that this shortfall corresponds exactly to the addition of equality types to the language. In preparation for the interpretation of and equivalence with syntax in the next section, we show how to present any semantic category equipped with a class of display maps as a sketch analogous to that used to construct the category of contexts and substitutions in Section 8.2.

Display maps   In Section 4.6 the interpretation of a (simply typed) algebraic theory L in a category C was a product- preserving functor Cn×L® C. In the dependent type case the functor preserves (certain) pullbacks, but there are a lot more of these, so how can the extension to type dependency be conservative?

REMARK 8.3.1 The P pullback is simply the binary product Xx Y in the slice  Cn×L¯ G, as in simple type theory. This is commutative and associative, but only up to isomorphism.

omitted diagram environment

The second square was not mentioned before, as it was automatically a pullback by Lemma 5.1.2. This is because when x Ï FV(Y), as also for (\check S), the X-indexed union becomes XxY and the map marked na is a section of  [^(x)] = p1:XxY® Y ( cf Lemma 8.2.15(b)).

In the dependent case, na is no longer a (generalised) element but the ath inclusion into a sum indexed by X. Being a pullback expresses stability of this sum, as in Section 5.5, and na is a regular mono, but not necessarily split. We also see the semantic reason why the components of the normal form of a map to [G,x:X,y:Y] come in the order [y: = b];[x: = a]: the element b Î Y[a] must be selected before it is included in the sum.

Putting these together, to abstract Theorem 8.2.16 we need the pullback of any display map [^(y)] against arbitrary maps in the category.

DEFINITION 8.3.2 Let D Ì morC be a class of maps of any category, which we write ® .

Then we call D

(a)
a display structure, if for each d:X® D in D and u:G® D in C there is a given pullback square, in which u*d Î D ;

(b)
a class of displays if every such square exists, with u*d Î D, and the class D is closed under composition with isomorphisms. omitted diagram environment

An interpretation of (C,D) considered as a generalised algebraic theory is a functor from C which preserves displays and these pullbacks.

We shall say that a C-map is a cut if, like na above, it can be expressed as a pullback of a section of a display along a sequence of displays.

The class D need not be a subcategory, ie include all identities and be closed under composition. In fact these properties of D say that there are base types isomorphic to singletons and dependent sums (Remark 9.3.1). But the semantic classes of displays frequently are subcategories, and in practice it is convenient and harmless to make this assumption.

Even when D is a subcategory, it is ``closed under pullbacks'' only in the sense that if the right hand side of a pullback square in C lies in D then so does the left. The category D need not have pullbacks: we have not required pullback mediators to lie within it (Exercise 8.13). In particular it need not be the M-class for a factorisation system. Indeed if the cancellation property (u;d),  d Î DÞ u Î D ( cf Lemma  5.7.6(e)) were required, this would defeat the point of Definition 8.3.8 below.

Next we consider the extreme cases between which display structures interpolate.

Products and equality types  

EXAMPLE 8.3.3 Let C be a category with specified terminal object 1 and specified binary products. Then the class D of maps that are specified left projections, p0:DxX® D, forms a display structure. The resulting interpretation of the context [x1:\typeX1,¼,xn:\typeXn] is the left-associated product ((···(((1x \typeX1)x \typeX2)x \typeX3) x···)x \typeXn) which was defined in Remark 4.5.15.

PROOF: Given any map u:G® D, let the specified product projection p0:GxX® G serve as the choice of pullback. The ``dependent'' types in this example are in fact constant. []

PROPOSITION 8.3.4 Let C be a category with a class of displays. If all product projections and pullback diagonals are displays, then every map is (isomorphic to) a composite of displays, and C has all finite limits.

PROOF: Consider the graph of u:X® Y (Remark  5.1.7):

omitted diagram environment

Then the pullback of u against any |:Z® Y must exist. []

REMARK 8.3.5 The diagonal is the equality type,

^
=
 
:{y0,y1|y0 = y1} ® [y0,y1:Y],
so Proposition 8.3.4 says that the classifying category of a generalised algebraic theory has all finite limits (and all of its maps are isomorphic to displays) iff the theory has all equality types.

The presence or absence of equality types influences the quantifiers. In the syntax, the quantifiers are always associated with a (bound) variable , and we shall find in Sections 9.3 and 9.4 that they are the two adjoints to the weakening functor for that variable. Bill Lawvere, however, who first had this insight, described them as adjoint to pullback d* against arbitrary maps d [Law69], and emphasised this by discussing the diagram above [Law70, p. 8]. Quantification along a general function f in Set gives the guarded quantifiers (Remarks 1.5.2 and  3.8.13(b)),

omitted eqnarray* environment

in which the effect of the graph {x,y|y = f(x)} is clearly visible.

Consider in particular quantification along the diagonal map [^ = ]X:

($[^ = ] T)[x0,x1] Û (x0 = x1)        ("[^ = ] ^)[x0,x1] Û (x0 ¹ x1).
Perhaps the equality type itself may be acceptable in a computational setting, but the inequality type (x0 ¹ x1) begins to raise doubts. To be able to distinguish positively between x0 and x1 suggests a ``Hausdorff'' condition on the type, ie that there is some computation f:X\rightharpoonup 2 that terminates for these arguments (but not necessarily everywhere) with f(x0) = 0 and f(x1) = 1. In fact "[^ = ] exists for X Î obSp (classically) iff it is locally Hausdorff (Example  9.4.11(e)). On the other hand, $[^ = ] exists iff X is a discrete space (Remark 9.3.13) .

Display maps in topology and elsewhere   Since Definition 8.3.2 is a unary closure condition (Section 3.8) there are lots of examples.

EXAMPLES 8.3.6 The following are semantic classes of displays:

(a)
Product projections ( ie all legs of spans which have the universal property of a product) in a category with finite products.

(b)
All maps in a lex category.

(c)
All instances of the order relation in a meet-semilattice.

(d)
Monos in Set. If we think of subobjects as subsets with canonical inclusions then these provide a corresponding display structure. The pullback in this case is called inverse image.

(e)
A map d:X® D in any category is called carrable if the pullback u*d along every map u: G® D exists.

(f)
The carrable maps in IPO (domains with bottom) are exactly the projections (Example  3.6.13(b)).

(g)
Inclusions of normal subgroups form a class of displays in Gp which is not closed under composition.

(h)
Replete functors (Definition 4.4.8(d) ) form a class of displays in the 1-category of categories and functors.

(i)
Subspaces, local homeomorphisms and open surjections (but not general continuous surjections) of topological spaces. Example 9.3.10 shows how to use open maps to interpret the existential quantifier. These and other classes may also be defined for toposes.

(j)
We may form the closure under pullbacks of any class whatever of carrable maps, to give a class of displays.

(k)
More usefully, given a class of ``grue'' maps (for example closed maps between topological spaces), we say that a morphism is stably grue if all pullbacks of it exist ( ie it is carrable) and are grue. (In the modal logic of Section 3.8, stably means [], and part (j) said < > .)

Many of the examples of classes of displays of toposes may be described as an internal set, locale or other structure in the target topos.

EXAMPLES 8.3.7

(a)
D. Lazard ( c. 1950) defined a sheaf as a local homeomorphism d:X® D between two topological spaces. The fibres X[u] º d-1(u) for u Î D are discrete and may be regarded as the values of a ``variable'' set as u ranges over the space D. The relative slice Sp¯ D @ Shv(D) is a topos, so it obeys the same (intuitionistic) logic as Set. The (global) sections D® X of d are the global elements of the set X, but these are inadequate to characterise it: we need to consider arbitrary maps (generalised elements) G® X (Definition 8.2.13).

(b)
The category Loc of locales has all finite limits, so that arbitrary continuous functions d:X® D may be used as displays. They correspond to internal locales in the topos Shv(D).

Intermediate pullback-stable classes of continuous functions or geometric morphisms correspond to notions of space over D lying between the discrete and the general cases.

(c)
Algebraic lattices (Sections 3.4 and  3.9) provide the simplest notion of ``domain.'' Recall that they are of the form Idl(Cop), where C is a meet-semilattice, and the Scott topology is the frame of monotone functions WCop. Martin Hyland and Andrew Pitts showed how to make these domains ``variable'' [HP89], by allowing C to be an internal semilattice in Shv(D). The topology of the domain is then ACop, the topology of D being A; the topos display is d:Shv(D)Cop ® Shv(D), where d* takes F Î obShv(D) to lX:obC.F .

(d)
They also generalised this idea from propositions to types, replacing semilattices by lex categories, ie the classifying categories of finitary essentially algebraic theories internal to Shv(D). A similar construction could be based on our generalised algebraic theories (classified by display categories) instead.

In the next section we show that for each class of display maps there is a certain generalised algebraic theory. The terms of the corresponding type in context are exactly the points of the variable space, and the type theory allows us to reason about it as if it were a set. Unlike classical logic, no assumption is built in that structures are determined by their points: they may have none globally. The ``points'' provided by type theory are terms or generalised elements (Remark 4.5.3). In this way dependent type theory is applicable in general topology, topos theory and domain theory to justify more ``synthetic'' styles of argument.

Relative slices   From the semantics we shall now move gradually back towards syntax, starting with the analogue of Definition 8.2.9.

DEFINITION 8.3.8 For G Î obC, the relative slice category C¯ G has

(a)
as objects D the composable sequences of D-maps
G¬ \typeX1 ¬ \typeX2 ¬ ·· ·¬ \typeXn

(b)
and as morphisms the commuting triangles in C of the form omitted diagram environment where a:D® F is any C-map.

So the forgetful functor src:C¯ G® C is faithful and reflects invertibility. In particular, if C has a terminal object, C¯ 1® C is full and faithful. Don't confuse C¯1 with C¯ 1, which is trivially isomorphic to C.

REMARK 8.3.9 Every context may be reduced to [  ] by successively omitting variables, so every object of Cn×L has a canonical sequence of displays down to the terminal object. Since it preserves displays, the interpretation only makes use of a particular semantic object if it too has such a sequence. Cartmell [Car86] focused on the sequences of displays, defining a contextual category to have a tree-structure on its object-class (and functorial assignment of pullbacks). However, there may be isomorphic objects with entirely different paths in the tree structure. Our relative slice category C¯ 1 has this tree structure, but C need not.

If every terminal projection X® 1 in C is a display, then C¯ 1 is strongly equivalent to C. More generally, we say that (C,D) is rooted if every X® 1 is a composite of isomorphisms and displays ([HP89] calls this the display condition). Then C¯ 1 @ C, either strongly or weakly according as the composite is given or just exists.

No further hypothesis is needed concerning the existence of products in C¯ G, because they are given by pullbacks of displays over G and so are guaranteed by the display axioms.

Using the contextual structure of the semantic category C¯ 1, its maps can be expressed in ``normal form'' and this category is presented by a sketch in the same way as that used to define the syntactic category Cn×L. The proof is much easier than for the corresponding results of the previous section, because this time we know in advance that P and \check S are pullbacks, whereas before we had to work up to this from the special case in Lemma  8.2.10.

LEMMA 8.3.10 Every morphism b:D® F of C¯ G may be expressed as a composite of a sequence of cuts (in the sense of Definition  8.3.2) of the same length as F, followed by displays corresponding to D. This is unique up to unique isomorphism of the intermediate objects.

PROOF: The pullback on the left gives b = g;[^(D)] with g;[^(F)] = \idD :

omitted diagram environment

We decompose g into a sequence of cuts by induction on (the length of) F, the base case [  ] being trivial. The second diagram is the induction step, adding one display Y® F, where

d = g;[^(y)] is already in normal form. The extra cut a is found as shown, and g = a;dy. Finally, as in Lemma  8.2.10, the number of displays involved is fixed by the source and target of the given map, and the intermediate objects are determined (as pullbacks) up to isomorphism. []

PROPOSITION 8.3.11 C¯ G is given by a sketch with laws analogous to those called (P), (T), ([^(S)]), (\check S) and (W) in Remark  8.2.7.

PROOF: These laws are needed to take a composite which is the wrong way round and rearrange it into normal form. []

We have presented the syntactic and semantic categories by sketches of the same form. Now we shall turn this into a categorical equivalence.