Remark 5.8.5 used relational algebra to illustrate the link between the existential quantifier (with proofanonymity) 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 proofanonymity.
In the Lawvere presentation, the existential quantifier is the left adjoint of the substitution functor. So P:Cn^{×}_{typeprop} ® Cn^{×}_{type} is a bifibration (Definition 9.2.6(e)), but the BeckChevalley 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 BeckChevalley 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

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.
Sumintroduction 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 termformation rule introducing sum types is


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 typeterm 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

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 brule for sums (cutelimination) executes the match:

The box idiom is

The hrule is

Like labstraction, let respects equality:

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 fillin which makes the triangles commute.
PROOF: The sum elimination rule ($^{}_{id}E) 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


Substitution and the BeckChevalley 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


DEFINITION 9.3.6 The (substituted) weak sum elimination rule is

omitted diagram environment
REMARK 9.3.7 The comparison (marked º in the diagram)


THEOREM 9.3.8 The verdict obeys the weak sum rules iff $x\dashv [^(x)]^{*} and the BeckChevalley condition holds. []
COROLLARY 9.3.9 With u:[D,y]\hookrightarrow D, we have the Frobenius law

Our Frobenius Law follows a corollary of BeckChevalley 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 counit 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

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_{1},q_{2}], and in particular for the case where q_{1} = $x.f:

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


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 fillin p is given by the elimination rule, the brule 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 BeckChevalley 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 typetheoretic notation for $x.F, where F is a list of propositions involving x. This is because


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

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