Practical Foundations of Mathematics

Paul Taylor

9.3 Sums and Existential Quantification

Remark 5.8.5 used relational algebra to illustrate the link between the existential quantifier (with proof-anonymity) and stable factorisation (into regular epis and monos). In this section we shall demonstrate this directly from syntax. Recall that we used the notation \hookrightarrow and \twoheadrightarrow in Section 5.7 for factorisation systems, without assuming that these maps really were mono and epi; we are using the same Convention 9.1.2 in this chapter, calling the body and result of the quantifier ``propositions,'' without assuming proof-anonymity.

In the Lawvere presentation, the existential quantifier is the left adjoint of the substitution functor. So P:Cn^×_type|prop Ž Cn^×_type is a bifibration (Definition 9.2.6(e)), but the Beck-Chevalley condition, for invariance under substitution, must be stated separately (Exercise 9.19). The dependent sum arises in the same way from arbitrarily divided contexts (Example 9.2.5), the Beck-Chevalley condition now being automatic.

We shall use display maps instead of the fibred technology of the previous section, and derive diagrammatic universal properties directly from the syntactic introduction and elimination rules. The quantifiers are only naturally defined when the ``substitution'' is weakening, so $x\dashv[^(x)]^*.

Dependent sums and composition We begin with the case where the range, body and result types are of the same kind. This quantifier, the dependent sum S, exists when the (single) class of display maps is closed under composition ( cf Definition 8.3.2).

REMARK 9.3.1 We defined a display map to be one which arises in the category of contexts from forgetting a single variable, so if the class is to be closed under composition, every context [G,x:X,y:Y] with two (extra) variables must be the same as some [G,z:Z] with just one.

omitted diagram environment

In this case we have an isomorphism over G making Z the dependent sum Sx:X.Y[x]. As the notation suggests, this situation reduces to a binary product in the case where Y[x] does not in fact depend on x:X (indeed, GXY is then the ( P-)pullback of GX and GY, Remark 8.3.1).

But it is asymmetrical in X and Y: like iffandythen in imperative programming languages, the x- component is ``read'' first.

The projection operations have arity

G,z:Z \vdash p₀(z):X G,z:Z \vdash p₁(z):Y[p₀( z)].

Notice that p₀(z) is used twice; in this sense the ($E )-rules which we shall discuss below are computationally simpler.

Similarly, if an identity (or more generally an isomorphism) is a display then it must be possible to omit the corresponding type, and conversely to introduce its value in a unique way. This type is therefore a singleton.

Hence dependent sums are freely added to a type theory by closing its class of displays under composition.

Sum-introduction We cannot recover a:X and b:f[a] from a proof of $x.f[x], so the projections p_i are lost when we quantify one kind over another. But we still have the pairing map. This operation has not previously been given a name in type theory: we do so to stress that it need not be an isomorphism, and that it is to $ as evaluation is to ".

DEFINITION 9.3.2 The term-formation rule introducing sum types is

G,x:X,y:f\vdash ve:$x:X.f. ($Á )

This operation takes a witness a:X and its evidence b:f[a], and yields a proof of $x.f[x], so we shall call it the verdict , ve(a,b). Spelling this out, the right rule in the sequent calculus is

omitted prooftree environment

The verdict operation is a map [G,x:X,y:f]\twoheadrightarrow [G,z:$x.f]. We use the double arrowhead because, if the propositional displays \hookrightarrow are monos, then the verdict maps are stable regular epis, as we shall see.

For the binary sum (Remark 2.3.10) we wrote n_x(y) for ve(x,y). Note that x,y Ď FV($x.f); we ought perhaps to write [^(y)]^*[^(x)]^*$x˘:X.f[x: = x˘], but we shan't. Also, we never meet the quantifier $y:f.X; this is because its verdict operation ve(y,x) would be a type-term depending on a proof y:f, violating Remark 9.1.1(b) and Definition 9.2.1(b).

Unsubstituted weak sums and the adjunction

REMARK 9.3.3 The simplest weak sum elimination rule is

omitted prooftree environment

which reduces to ($E ) as in Definition 1.5.1 if we erase the proofs (terms of propositional type). `` G\vdash q prop '' is the more precise type- theoretic way of saying that q is a well formed proposition with x Ď FV(q). With the variable z, this is actually the ``left rule'' in the sequent calculus, cf Remark 1.4.9: the elimination rule in natural deduction gives a value c to z. This term might involve parameters from another context, but we shall ignore these at first.

The let syntax, though ugly, is needed to match the argument z or c against the pattern ve(x,y), binding the variables x and y ( cf n_i in ( +E), Remark 2.3.10), whereas (lx.p)a assigns its argument to just one variable. The b-rule for sums (cut-elimination) executes the match:

omitted prooftree environment

On the face of it, we associate the value a to the variable x and b to y within the proof f. But the verdict need not be the pairing function, and many different pairs a,b may be associated with the same proof c = ve(a,b) of $x.f[x]. So there is an equivalence relation amongst such pairs, and the let expression corresponds to the familiar idiom of ``choosing'' a member of the equivalence class, cf Remark 1.6.7 - ie to using an ($E )-rule. This indeterminacy is why we say let instead of put.

The box idiom is

= .30omitted vchbox environment \leadsto ^{$^-b} omitted vchbox environment

The h-rule is

omitted prooftree environment

Like l-abstraction, let respects equality:

omitted prooftree environment

PROPOSITION 9.3.4 $ and ve satisfy the unsubstituted weak sum rules iff in the square (commutative since the rules happen in the context G),

omitted diagram environment

there is a unique fill-in which makes the triangles commute.

PROOF: The sum elimination rule ($^-_idE) gives such a map; it is a term of type q, so the lower triangle commutes. The upper one is the ($^-b)-rule in the unsubstituted form ( cf Example 7.2.7)

omitted eqnarray* environment

Finally, the (let = , $^-h)-rules say that p is unique. []

REMARK 9.3.5 Existential quantification is the left adjoint of weakening. Indeed [z: = ve(x,y)] is a universal map (Definition 7.1.1) in the fibre category P([G,x:X]) from the object [G,x:X,y:f], ie the proposition f, to the functor [^(x)]^*:P(G)ŽP([G,x:X]). Then

[G,x:X,y:f] Ž ^{h = [z: = ve(x,y)]} [G,x:X,z:

^
x

$x.f]

and

[G,z:$x.

^
x

q] Ž ^{e = [m: = let(x,y)be zin y]} [G,m:q]

are respectively the unit and co-unit of the adjunction $x\dashv [^(x)]^*. []

Substitution and the Beck-Chevalley condition The adjunction is very neat, but it is not the whole story, because we have overlooked substitution for the parameters which might occur in the proof c of $x.f.

These parameters are provided by the substitution u:GŽ D . We make the convention that the types X, f[x] and $x.f are defined in D ( cf type- symbols being defined over D in the previous chapter), although for reasons of space we often omit these from the rules. Then

G\vdash c:u^*$x.f[x],

corresponds by Lemma 8.2.14 to a morphism

[u,z: = c]:GŽ [D,z:$x.f].

As G, u and c are arbitrary, this is a generalised element of [D,z:$x.f].

DEFINITION 9.3.6 The (substituted) weak sum elimination rule is

omitted prooftree environment

which turns the diagram in Proposition 9.3.4 into

omitted diagram environment

REMARK 9.3.7 The comparison (marked ş in the diagram)

G,z˘: $x:u^*X.u^*f\vdash let_G (x,y) be z˘in u^*\ve_D (x,y) :u^*$x.f

arises from the unsubstituted rules - the introduction rule (unit, ve) of $x_D \dashv [^(x)]_D and the elimination rule (co-unit, let) of $x_G\dashv [^(x)]_G :

$x_G ·\u_x^* Ž ^h_D $x_G ·\u_x^* ·

^
x

*
D

·$x_D = $x_G ·

^
x

*
G

·u^* ·$x_D Ž ^e_G u^* ·$x_D .

In the case u = id, this is the identity, by the triangular laws given in Definition 7.2.1. The fully substituted form of ($^-E) provides the inverse of the comparison for any substitution u, as may be seen by putting $x:u^*X.u^*f for q in the diagram. This is the Beck-Chevalley condition for sums, cf the context diagrams in Remark 9.1.9.

THEOREM 9.3.8 The verdict obeys the weak sum rules iff $x\dashv [^(x)]^* and the Beck-Chevalley condition holds. []

COROLLARY 9.3.9 With u:[D,y]\hookrightarrow D, we have the Frobenius law

$x.(f[x]Ůy) ş ($x.f[x])Ů y.

because the two factorisations of [D,X,fŮy]\hookrightarrow [D,X]Ž D in the diagram overleaf must be isomorphic. []

Our Frobenius Law follows a corollary of Beck-Chevalley because, unlike Lawvere and Bénabou, we include substitution for propositional as well as type variables in the change of base u.

Putting f = T, the co-unit of $x\dashv [^(x)]^* is a cartesian transformation ( cf Remark 6.3.4 and Proposition 7.7.1(e)).

omitted diagram environment

The box proof ( cf Lemma 1.6.3) is

omitted proofbox environment

An idiomatic form of this proof would use `` let(x,y)becin'' to open the box, after which we may say c = ve(x,y). However, when the box is ultimately closed (at the end of the proof or before closing a surrounding box), the term has to be exported in its let form.

Semantics and open maps The existential quantifier adds a case to the structural recursion in Remark 9.1.10. Given displays [[[^(y)]]] and [[[^(x)]]],

omitted diagram environment

we have to find denotations for ve and [^(z)] making the square commute. For soundness of the let syntax, these must have the same universal property in the semantics as that described in Proposition 9.3.4 for the syntax. So the functor [[-]] preserves the factorisation system.

EXAMPLE 9.3.10 Let S be Sp or Loc and M the class of open inclusions; by the definition of continuity, this is closed under pullback.

For any G Î obS, the relative slice P(G) ş SŻ G is the frame of open subsets of the space G, and for any continuous map u:GŽ D, the substitution functor u^*:P(D)Ž P(G) is the inverse image (frame homomorphism) of the same name. By Remark 9.3.5, if u (deserves to be called a display [^(x)] and) admits an existential quantifier $x, then this must be the left adjoint \u_!\dashv u^* with the Frobenius law

\u_!(UÇu^*V) = \u_!(U)ÇV for all U Î P(G) and V Î P(D).

Such a u is called an open map. This usage is consistent with the term open inclusion, because any mono which satisfies the Frobenius law is the inclusion of an open subset. Then the class D of open maps

(a): contains all isomorphisms,
(b): is closed under composition,
(c): is stable under pullback against arbitrary continuous maps,
(d): satisfies the Beck-Chevalley condition for such pullbacks, and
(e): obeys the cancellation law that, if e is a surjection ( ie e^* is full) and e;u is open, then u is also open.

Since the class E of open surjections also has these properties, and in particular the factorisation of open maps into open surjections and open inclusions is stable under pullback, we have a sound interpretation of $ ( geometric logic), where D provides display maps for the types. []

Strong sums So far we have only defined the adjunction $x\dashv [^(x)]^* between the categories whose objects are a single type f over [G,x:X] and q over G. If the kind of propositions admits dependent ``sums'' over itself, ie the class M of displays is closed under composition, then this is enough to deal with contexts ( lists of propositions) F and Q ( cf Exercises 5.47 and 9.27).

Otherwise we must use a more complicated version of ($E ) for the context Q = [q₁,q₂], and in particular for the case where q₁ = $x.f:

omitted prooftree environment

The orthogonality condition for a factorisation system (Definition 5.7.1) provides the stronger rule, in which q may depend on z:$x.f.

THEOREM 9.3.11 [Martin Hyland, Andrew Pitts [HP89]] A verdict

G,x:X,y:f\vdash ve(x,y):$x:X.f

is orthogonal to all propositional displays [^(m)]:[Q,m:q]\hookrightarrow Q iff it satisfies the strong sum elimination rule,

omitted prooftree environment

where q also becomes q[z: = ve(x,y)] in the conclusion of ($b) and q[z: = z˘] in ($h). Hence strong sums with range D and body M exist iff there is another class E (consisting of all maps which are isomorphic to verdicts) such that E^M and M;D Ě E;M, this factorisation ( [^(y)];[^(x)] = ve;[^(z)]) being stable under pullback.

omitted diagram environment

PROOF: According to the original definition, we should show that ve is orthogonal to [Q,q]\hookrightarrow [l = 1.8em]Q with respect to any z:[G,$x.f]Ž [l = 1.5em]Q. However, Lemma 5.7.10 lets us consider ``epi'' and ``mono'' maps with the same target [G,z:$x.f], ignoring z. Recall that the proof of this lemma used pullback along z ( cf Exercise 9.30). As for the weak sum in Proposition 9.3.4, the fill-in p is given by the elimination rule, the b-rule says that it makes the triangle commute, and it is unique by the h- and equality rules. Remark 9.3.7 has already shown that the pullback along u of a verdict map must be another such. []

REMARK 9.3.12 As a special case, a single kind admits strong sums over itself ( M = D) iff it is closed under composition (Exercise 9.26) . In this case the verdict maps are isomorphisms, so the Beck-Chevalley condition and stability under pullback are automatic. The formulation with ``product'' projections (Remark 9.3.1) relies on the kinds being the same, otherwise we would have witnesses for existential quantification.

REMARK 9.3.13 The strong sum generalises the test proposition q to a context extension, but there seems to be no type-theoretic notation for $x.F, where F is a list of propositions involving x. This is because

$x.f[x]Ůy[x]\vdash

ć
č

$y.f[y]

ö
ř

ć
č

$z.y[z]

ö
ř

is irreversible without ``co-operation'' between the witnesses of f and y. By Lemma 5.7.6(e), the comparison map

[G,$x.(f,y)]Ž [G,$x.f] \hookrightarrow G

is in \orthr E, so maybe it should be regarded as a proposition (in M), but this is not clear. If we do adopt this view, then the factorisation problem reduces to two cases, of which the first is called the support of X:

omitted diagram environment

Even then, type theory does not require all maps to be factorisable. In particular the pullback diagonal (contraction, variable qua term)

[G,x:X] Ž ^{[y: = x]} [G,x:X,y:X],

which is of course a split mono, does not have to be (factorisable into a verdict and) a propositional display. For example, this map is open (Example 9.3.10) with G = 1 iff the space X is discrete, cf Remark 8.3.5.

Finally, notice that it is the factorisation e;m rather than the class E which is required to be stable under pullback, since the target of the substitution u:GŽ D is that of m, not e. (Before Definition 9.3.6 we did mention a morphism to [D,$x.f], but its extra component c did not contribute to the pullback.)