The rules for the dependent product are those for the quantifier " in Section 1.5, with the addition of terms which come from the l-calculus. The dependent product Px and universal quantifier "x are right adjoint to weakening, with a Beck-Chevalley condition, but this is where the similarity with Sx and $x ends. As usual, we relate the syntactic rules to various diagrammatic forms.
Whereas the previous section was very much about the quantifier (albeit directly applicable to categories in which the ``propositional'' displays need not be mono), this one quickly leaves the predicate calculus behind, and has much more of the flavour of function-types. However, following Convention 9.1.2, we retain the predicate notation, although its only purpose is to distinguish the positive role of the body f[x] from the negative range x:X of the quantifier (Remark 1.5.9). Far from assuming the display of f to be mono, in Lemma 9.4.10ff we consider the special case in which f is a fixed object and the type display is mono. You may prefer to start with Definition 9.4.8, skipping the type theory, as there are applications in geometric topology, as well as to free algebraic theories.
DEFINITION 9.4.1 The application map ("-elimination) is
|
|
|
|
|
THEOREM 9.4.2 The octagon interprets the rules for the dependent product iff for every dotted map as the lower left oblique edge,
|
|
PROOF: As before, ("Á ) provides the map, ("b) makes the diagram opposite commute and (l = ,"h) say that the fill-in is unique. The obtuse dotted triangles define bijections \expx p« [u,f] and p« [u,p] by Lemma 8.2.14, and the parallelograms (but not the kites) are pullbacks - there is no room for the right-angle symbol any more! []
quote omitted diagram environment
The composite [^(Y)] ;u:[G,Y]® D above in fact corresponds to the u in the syntactic rules; Y has only been included to state the next result.
The adjunction, Beck-Chevalley condition and other forms
REMARK 9.4.3 Universal quantification is the right adjoint of weakening. With u = id, consider Y not as a context extension but as an object of the relative slice S¯ G. Then there is a natural bijection
|
|
|
Now consider the general substitution u:G® D, which imports proofs into the box in the language of Lemma 1.6.3ff. In that section we only saw the consequences of importation for $, not for ", because the range of quantification (X) was a simple type.
The separate adjunctions [^(x)]*G \dashv "xG and [^(x)]*D \dashv "xD give a comparison
|
|
|
REMARK 9.4.4 There are two complications in this formulation:
In Section 9.3 the analogous object to Y, testing the adjunction, was called q. There the choice between types and propositions for q (rather than for the other participating objects X, f[x] and $x.f) was the crucial difference between the dependent sum and existential quantifier.
The next result, due to Thomas Streicher [Str91], shows that, for the product, these two complications actually cancel each other out. Hence dependent products are absolute: they are defined independently of the choice of the classes M and D of displays.
THEOREM 9.4.5 Let DX® [^(x)]D, DX f\hookrightarrow [^(y)]DX and DF \rightarrowtail [^(f)]D be displays, and ev:DXF® DXf. Then F and ev satisfy the rules for the dependent product "x:X.f over D iff there is a natural bijection
|
PROOF: Again, this follows from the octagonal diagram. []
Local cartesian closure Dependent products may also be described by restricting to slices or fibres, as the octagonal diagram resides there. Together with Chapter V, this is the usual categorical treatment of full first order type theory as it was done in the 1970s.
PROPOSITION 9.4.6 The following are equivalent for any category C which has a terminal object.
In particular the Beck-Chevalley condition is automatic and all colimits are pullback-stable. Then C is said to be locally cartesian closed. []
In a locally cartesian closed category all maps are treated as displays, so it has equality types and dependent sums (Remarks 8.3.5 and 9.3.1). Taking the class of monos for the propositional displays, Exercise 9.34 shows that this is closed under dependent products along all maps, so we may interpret universal quantification. Existential quantification may be interpreted as in Section 5.8 on the additional assumption that equivalence relations have quotients (which are automatically stable).
However, the syntax may lack equality types, for the reasons discussed in Section 8.3. In semantic categories, such as those consisting of domains or (locally compact) topological spaces, not all finite limits need exist. Hence we need to consider products whose ranges belong to a restricted class, which we have called type displays (® ).
DEFINITION 9.4.7 A relatively cartesian closed category C has a single rooted class D of displays, for which all dependent products exist (with the range, body and result in D). Equivalently, every relative slice C¯ G is cartesian closed and pullback preserves exponentials, ie u*\evD has the universal property of \evG . Such categories were introduced by me, together with an essentially syntactic example based on retracts of a model of the untyped l-calculus [Tay86a]. Dependent products of domains were constructed in my thesis [ Tay86b], and this notion was studied further in [HP89].
Partial products Examples of a particular case of dependent product were identified in geometric topology by Boris Pasynkov [Pas65], before Lawvere had studied the quantifiers categorically, and long before the modern type-theoretic account of them had been formulated and applied in informatics. Partial products are more complicated than ordinary function- spaces, but not much, so it is quite feasible to investigate them in semantic categories such as in topology.
Susan Niefield [Nie82] characterised those continuous functions which admit partial products for the Sierpi\'nski space F = S, and hence for all F Î obSp. She also studied the categories of uniform spaces and affine varieties. Building on this, the relationship between partial products and a notion of exponentiability was formulated by Roy Dyckhoff and Walter Tholen [ DT87], although none of these authors discussed the Beck-Chevalley condition. In fact we shall see that all dependent products ( with this condition) can be derived from partial products.
DEFINITION 9.4.8 Let [^(x)]:DX® D a carrable map in a category C, ie one for which all pullbacks exist (Example 8.3.6(e)), so it is legitimate to call it a display. Also, let F be any object of C. Then the sub-diagram in bold below (where the parallelogram is a pullback) is called a partial product if it is the universal such figure, ie given u:G®D and p:[G,u*X]® F there is a unique map [u,f]:G® DFX making the diagram commute.
omitted diagram environment
Treating F as a constant type (defined in the empty context), and using the binary product (DX)xF, shown dashed, this is another special case of the octagonal diagram in Theorem 9.4.2. Hence the partial product DFX is the dependent product "x.[^(x)]*F in the context D.
When D = 1, this is the ordinary function-type FX (Definition 4.7.9).
The map DX® D is exponentiable if partial products DFX exist for all F Î obC.
|
|
(\u0,\polly0) £ (\u1,\polly1) Û \u0 £ D \u1 Ù "x Î X[\u0]. "y Î X[\u1]. x £ XyÞ \polly0(x) £ F \polly1(y).
For this relation to be transitive on DFX, it would suffice that
|
LEMMA 9.4.10 If DX® D is mono and the partial product DFX exists, then DXFX º (DX)xF, ie the dashed vertical morphism in the diagram opposite is invertible.
PROOF: Given Fp¢¬ G¢u¢® DX, put
u:G = G¢® DX® D, so GX = G¢ is the inverse image, and let p = p¢. Then [u,f]:G® DFX factors through DX by construction, so the pullback mediator is the required product mediator G® DXFX. []
EXAMPLES 9.4.11 In the following examples, S denotes the Sierpi\'nski space whilst Sn Ì Rn+1 is a circle or sphere.
[u,f]:G = [0,1]® DFX is determined by the path u in D, together with open segments p in F defined on the inverse image of the interior DX Ì D. This suggests a way of computing the fundamental groupoid p1(DFX).
EXAMPLES 9.4.12 In practice, the result of a quantifier need not lie in the same class of maps as its (range or) body.
|
Partial products suffice Partial products are easier to calculate semantically than general dependent products, but we shall now show that, together with pullbacks, they are enough. The trick, categorically, is to consider naturality with respect to F.
The reason for writing capital F and \hookrightarrow with a double head above is that we shall later use F as the defining context of the proposition-symbol f, a substitution-instance of which occurs as the body of some dependent product to be calculated. We shall now write
|
|
LEMMA 9.4.14 Suppose that DFX (at the top of the diagram below) is the partial product of F along [^(x)] with evaluation map \evF , as in the parallelogram on the right, and let [^(y)]:[F,y:f]\hookrightarrow F be a propositional display. Then the following are equivalent:
The subscripts F and Ff on ev and l refer to the partial products DFX and D(Ff)X, whilst f indicates the dependent product "x.f.
omitted diagram environment
PROOF: For both universal properties, consider a test object G.
THEOREM 9.4.15 Let C be a category with a carrable map [^(x)], a rooted (`` propositional'') display structure, and (choices of) partial products of all objects along [^(x)]. Then all dependent products along [^(x)] exist.
omitted diagram environment
PROOF: We want the dependent product "x:u*X.p*f in G (shown in bold), where u:G® D and p:GX® F. The Beck-Chevalley condition says that the universal property of "x.\evF *f is stable, so the required product is given by pullback along [u,lx.p]:G® DFX as shown, since [u,lx.p]x;\evF = p using the partial product DFX. []
COROLLARY 9.4.16 The interpretation of dependent products can be defined to make the Beck- Chevalley condition hold up to equality.
PROOF: The binary dependency of "x:u*X.\nearrow *f on u and \nearrow is replaced by a unary one on [u,lx.\nearrow ] and the pullback is anchored at DFX, where X and f are type-symbols ( cf Remark 9.1.11). []