Practical Foundations of Mathematics

Paul Taylor

9.4  Dependent Products

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.

Application and abstraction  

DEFINITION 9.4.1 The application map ("-elimination) is

D,x:X,f:"x:X.f\vdash ev(f,x):f, ("E )
the corresponding left rule in the sequent calculus being
omitted prooftree environment
The term-formation rule introducing the "-type is l -abstraction:
omitted prooftree environment
combining the ("Á )- and (® Á )-rules of Sections 1.5 and 2.3, together with the substitution u which we have discussed in detail for $. There is also an equality rule (l = ) saying that if p = q then lx.p = lx.q. The b-rule incorporates the substitution u into Definition 2.3.7,
omitted prooftree environment
and finally the h-rule is
omitted prooftree environment
We have already devoted Sections 2.3 and  4.7 to simple type theory, where the dependent product reduces to the function-type X® Y. The diagram in Definition 4.7.9 is obtained from that opposite by replacing GY, f and "x.f by G, Y and F respectively, and otherwise deleting G, D and u. In particular, the ground context G was previously the terminal object and was not drawn. See also Example  7.2.7.

THEOREM 9.4.2 The octagon interprets the rules for the dependent product iff for every dotted map as the lower left oblique edge,

G,x:u*X,Y\vdash p:u*f
there is a unique map for each of the upper diagonals
G,Y\vdash f:u*"x:X.f
making the diagram commute. We write f = lx.p and F = "x.f.

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

omitted prooftree environment
for which the unit and co-unit of [^(x)]*\dashv "x are
[G,z:y] ® h = [f: = lx.z] [G,f:"x. ^
x
 
*
 
y]
[G,x:X,f: ^
x
 
*
 
"x.f] ® e = [y: = ev(f,x)] [G,x:X,y:f]
cf Theorem 9.3.8 for the weak sum. Currying (Example 4.7.3(c)) and Lemma 9.4.13 essentially show how to do this for a list F instead of a single proposition f.

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

G,f:u*"x:X.f\vdash lxG .\evD (f,x) :"x:u*X.u*f.
In categorical notation this is
"xG ·\ux* ¬ eD "xG ·\ux* · ^
x
 
*
D 
·"xD = "xG · ^
x
 
*
G 
·u* ·"xD ¬ hG u* · "xD ,
but from the fully substituted ("E )-rule we obtain
omitted prooftree environment
so that u*"xD .f º "xG .\ux*f. This is the Beck-Chevalley condition for products, using the context diagrams in Remark 9.1.9. []

REMARK 9.4.4 There are two complications in this formulation:

(a)
the Beck-Chevalley condition has to be stated separately, and

(b)
the bijection p« f is quantified over a class of displays such as [^(Y)] .

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

omitted prooftree environment
for all u:G® D whatever. Notice too that we have reverted to the ordinary slice C¯ D, since G is not a context extension of D. There is no further Beck-Chevalley condition.

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.

(a)
C has all dependent products;

(b)
every (ordinary) slice C¯ G is cartesian closed;

(c)
C has pullbacks and every pullback functor u* has a right adjoint.

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.

EXAMPLES 9.4.9

(a)
In Set, elements of DFX, ie maps G = {*} ® DFX, are pairs (u,p), where u Î [[D]] and p:X[u]® F, so
DFX =
å
u Î [[D]]  
FX[u ] ®     [^(p)]    D.

(b)
The functor T that codes a free algebraic theory (Definition  6.1.1) is of the form D(-)X, where X® D is k® W and X[r] = ar[r] .

(c)
In the general dependent product in Set for displays,
\coprodu Î [[D]] \coprodx Î X[u]f[u,x] ® [l = 3em][^(y)] \coprodu Î [[D]] X[u] ® [l = 3em][^(x)] D,
the elements of F[u] are the sections of \coprodxf[u,x] ® X[u].

(d)
In Pos, the elements of DFX are again pairs (u,p), where now p is monotone. As in Theorem  4.7.13, to determine the order on the function- space we consider f:G = {0 < 1}® DFX; then

(\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

"\u0 £ \u1 £ \u2."x Î X[\u0]."z Î X[\u2]. $y Î X[\u1].x £ y £ z,
but this condition is also necessary for F = {^ < T}, \polly0:x® T, \polly2:z® ^. General dependent products in Pos are sets of sections as for Set, equipped with this modified pointwise order.

(e)
F. Conduché found the analogous characterisation of exponentiable functors in Cat, which is discussed in [Joh77, p. 57]. In particular, any fibration or op-fibration is exponentiable, but if DX® [l = 1.8em] D belongs to one class then DFX\rightarrowtail [l = 1. 5em]D is in the other. Also, all replete functors between groupoids are exponentiable.

We have stressed that \hookrightarrow for the body of the quantifier is merely a notational convention. For many of the interesting examples of partial products, it is actually the type display DX® D that is mono.

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.

(a)
Lifting is a partial product, since the test is a partial map G\rightharpoonup F. F^ is the final solution to forming a pullback square containing F® 1 ® W; it is called a pullback complement in [ DT87]. omitted diagram environment

(b)
See Exercise 3.71 for the same construction in Loc; Example  7.7.4, the Freyd cover, gives it for toposes and geometric morphisms.

(c)
Since every open inclusion U\hookrightarrow G is the pullback of the open point of the Sierpi\'nski space along the classifying map G® S of U, and the universal property of the (topological) lift LiftF is stable by the Beck-Chevalley condition, U\hookrightarrow G is exponentiable in Sp.

(d)
Similarly for a closed subset A Ì G. By composition, any locally closed inclusion AÇU Ì G is exponentiable in Sp. Niefield showed that this characterises exponentiability for subspace inclusions.

(e)
The diagonal [^ = ]:X\hookrightarrow XxX is (locally) closed iff X is (locally) Hausdorff, cf Remark  8.3.5. If Y is locally compact and X locally Hausdorff, then any map Y® X is exponentiable.

(f)
Pasynkov's original example [Pas65 , p. 181] applied (c) to the interior of the ball Bn Ì Rn. The sphere S2 can be seen as the partial product of either the interval B1 by the circle S1, or the disc B2 by two points S0. Similarly for higher dimensions: omitted diagram environment

(g)
Using the universal property, a path

[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.

(a)
The function-space NN exists in Sp (it is called Baire space ), but it is not locally compact, so SNN does not exist.

(b)
Equality and the order relation on {^ < T} consist respectively of two and three points of the four-point Boolean algebra. The order can also be thought of as implication, and is definable from lifting. However, by Example 9.4.9(d), a full subposet DX® D is exponentiable iff it is convex, which these examples are not.

(c)
In the analogous topological situation for the Sierpi\'nski space S, these subspaces are not locally closed (Example  9.4.11(e)).

Facts such as these about a category could be presented by identifying certain triples of classes of display maps ( l=15pt,abut] ®, \hookrightarrow , \rightarrowtail ) such that we may form quantifiers whose range, body and result belong to the respective classes. In other words, we have a type theory with many kinds (\K1,\K2,\K3), and the usual introduction, elimination, b- and h-rules, but a restriction on the formation-rule for the dependent product:
omitted prooftree environment
Henk Barendregt [Bar92, § 5.4] has developed just such a formalism, but with the quite different motivation of unifying various syntactic calculi, including Girard's System F (Definition  2.8.10) and Thierry Coquand's Calculus of Constructions [CH88].

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

[F,y:f]\hookrightarrow     [^(y)]    F \hookrightarrow     [^(F)]     [  ],
assuming that these belong to a rooted class of displays. Comparing their universal properties, there is a unique mediator
D(Ff)X\rightarrowtail [l = 30pt,dotted] DFX º [D,f:FX]\rightarrowtail [l = 30pt]D
in the third class. We now show that this corresponds to the proposition "x.f[fx]. This method may be adapted to finding dependent products of contexts "x.F, cf Remark 9.3.13 for $x.F.

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:

(a)
[(p)] D(Ff)X is the partial product of Ff along [^(x)] with evaluation \evFf, shown as the big bold rectangle,

(b)
[(d)] D(Ff)X\rightarrowtail [l = 1.5em]D FX is the dependent product D,f:FX\vdash " x.f[fx], whose evaluation map \evf is shown dashed.

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.

(a)
[[pÞ d]] We are given [u,f]:G ® DFX and [u,f,x,q]:GX® DF XXf, so by composition of the equilateral triangle put p = \evF (f,x) to get [p,q]:GX® Ff, and [u,f,g] = \LambFf x.[p,q]: G® D(Ff)X using the partial product. This is the dependent product by Theorem 9.4.5, whose u, D and f correspond to [u,f], DFX and \evF *f º f[fx] here. The slender triangle at the top left commutes by universality of DFX, and the triangle involving \evf commutes using the pullback \evF *f.

(b)
[[dÞ p]] Given u:G® D and [p,q]:GX® Ff, use the dependent product to put [u,f] = \LambF x.p:G® DF X, define [u,f,x,q] using the pullback \evF *f and let [u,f,\Lambf x.q]: G® DFX "x.f[fx]. []

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). []