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
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.
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,
|
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:
|
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:
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.
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.
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
|
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.