Practical Foundations of Mathematics

Paul Taylor

7.7  Gluing and Completeness

To complete the equivalence between syntax and semantics, it remains to prove confluence, strong normalisation for the l-calculus and the disjunction property for intuitionistic logic. The conceptual content of these results, when proved syntactically, is drowned in a swamp of symbolic detail which cannot be transferred to new situations. The remarkable construction which we use illustrates how much can be discovered simply by playing with adjoints and pullbacks.

The origin of the name gluing is that this is how to recover a topological space from an open set and its complementary closed set (Exercise  3.71). The construction for Grothendieck toposes was first set out in [AGV64, Exposé IV, §9.5]. Considered as inverse images, functors between toposes with the rich properties of (p0,p1):S¯ U® SxA or p1:S¯ U® A are called surjections and open inclusions respectively (geometrically, SxA is the disjoint union of S and A.)

The gluing construction   Recall from Example 7.3.10(i) that, for any functor U:A® S, the gluing construction is the category S¯ U whose objects consist of I Î obS, G Î obA and f:I® UG in S, and whose morphisms are illustrated by the diagram below. We shall say that (I,G,f) is tight if f is an isomorphism.

omitted diagram environment

Since it preserves everything in sight, p1 is also called a logical functor.

PROPOSITION 7.7.1 Let U:A® S be any functor. (We emphasise the case where it preserves finite products and maybe pullbacks, and S is a topos; the dotted lines signify even stronger assumptions which we do not wish to make. See Exercise 3.70 for posets.) Then

omitted diagram environment

(a)
p1:S¯ U® A is an op-fibration, and also a fibration if S has pullbacks (Definition  9.2.6);

(b)
if S has an initial object \initialobjS then p1 also has a full and faithful left adjoint, E, so p1 creates limits and E preserves colimits;

(c)
E identifies A with the full (co-reflective) subcategory of S¯ U in which I = \initialobjS;

(d)
if \initialobjS is strict (Definition  5.5.1) and A has a terminal object \terminalobjA then this subcategory of S¯ U is the slice by (\initialobjS,\terminalobjA, \initialobjS® U\terminalobjA), so E is a discrete fibration and creates non-empty limits;

(e)
in this case, moreover,
E(Gxp1(Jf® UD)) = (0® U(Gx D)) = E(G)x(Jf® UD)
holds and the co-unit E·p1® id is a cartesian transformation (Remark 6.3.4, cf the Frobenius law, Lemma 1.6.3, Corollary  9.3.9);

(f)
p1 has a right adjoint, A, so p1 preserves colimits and A limits;

(g)
A identifies A with the full subcategory of S ¯ U consisting of tight objects, which is therefore reflective; it is also an exponential ideal (Exercise 7.11) if, as we shall show, S¯ U is cartesian closed;

(h)
U = p0·A and p1·A = id;

(i)
A preserves whatever colimits U does (but one of our main goals is to show that this happens); if U has a right adjoint R:S ® A and A has pullbacks then A also has a right adjoint; omitted diagram environment

(j)
p0 is a fibration;

(k)
p0 preserves whatever limits U does; indeed if F\dashv U with unit h then p0 has a left adjoint, identifying S with the full subcategory of S¯ U @ F¯ A which consists of universal maps (Definition  7.1.1);

(l)
if A and S have and U preserves 1 then p0 has a right adjoint T, so p0 preserves colimits and T limits;

(m)
T identifies S with the full subcategory of S ¯ U in which G = \terminalobjA; omitted diagram environment

(n)
(p0,p1) creates colimits, and has a right adjoint V if S has binary products;

(o)
(Gavin Wraith) S¯ U is the category of coalgebras for the comonad ( cf Definition  7.5.4) on SxA induced by (p0,p1)\dashv V;

(p)
(p0,p1) creates any limits which U preserves, and has a left adjoint if U does and A has binary coproducts. []

COROLLARY 7.7.2 Assuming only that U preserves finite limits, if A and S have the following structure, so does S¯ U, and p1 preserves it:

(a)
finite limits;

(b)
stable disjoint sums (Section 5.5);

(c)
regularity (Section 5.8);

(d)
effective regularity (Barr-exactness);

(e)
the structure of a prelogos;

(f)
that of a (countably) complete prelogos;

(g)
being a pretopos;

(h)
N (Example 6.4.13) and List(X) (Exercise 6.30).

If U preserves this structure then so does p0. []

Implication and the function-type are considered in Exercise 3.72 and Proposition 7.7.12; Exercises 7.50- 7.51 deal with factorisation systems (and so the existential quantifier, Section 9.3) and W (higher order logic).

Conservativity   Let C be a category and L a subcanonical []-language for it (Definition 7.6.5(a)), ie L names all of the objects and maps of C, stating all of the laws which hold between them, possibly with encoding operations for some []-structure. Recall from Definition  7.6.8 that [] is called conservative if the functor \qqdash :C® Cn[]L is full and faithful.

NOTATION 7.7.3

(a)
Define a functor U:Cn[]L® S º SetCop by
G® Cn[]L(\qqdash ,G),
which preserves any limits that Cn[]L has;

(b)
and another functor Q:C® S¯ U by
X ® (\HX,\qq X,\qX),
where \qX:\HX® F\qq X is a morphism of S º SetCop, ie a natural transformation between presheaves. It has components
\qX,Z:\HX(Z) º C(Z,X)® U\qq X(Z) º Cn[]L(\qq Z,\qq X)
given by quoting \qqdash of C-maps Z® X (which are the operation-symbols of L). In Proposition  7.3.9, Q is the mediator to the comma category from the lax square consisting of the Yoneda embedding \H(-):C \hookrightarrow SetCop,    quoting \qqdash :C® Cn[]L andq:\H(-)® U\qqdash .

EXAMPLE 7.7.4 Let C = {1} and suppose that L says that \qq 1 is indeed the terminal object (so there is a nullary encoding operation \vdash *:\qq 1 with one h-rule x:\qq 1\vdash x = *). Then

U º Cn[]L(1,-): Cn[]L® S º Set
gives the set of global elements of a context, ie its closed terms, or proofs under no hypotheses (Remark 4.5.3). In sheaf theory this functor is traditionally called G, which of course conflicts with the notation of this book. When A is a topos (instead of Cn[]L), [^(A)] º Set¯ U is called the Freyd cover or scone (Sierpi\'nski cone) of A, the (closed) vertex being Set qua the one-point topos ( cf lifting a domain, Definition  3.3.7 and Exercise 3.71) . Also, Q(1) = (id:1® U1). []

LEMMA 7.7.5 Q is full and faithful.

PROOF: An (S¯ U)-map QX® QY is a pair (x,a) making the square below commute, but by the Yoneda Lemma (Theorem 4.8.12(a)) any S-map (natural transformation) x:C(-,X)® C(-,Y) is of the form post(a) for some unique (semantic) map a = xX(\idX):X® Y in C.

omitted diagram environment

The other map, a, belongs to Cn[]L, ie it is syntactic, a substitution. We must show that a = \qqa without assuming the theorem we're trying to prove, that \qqdash is full and faithful. In fact this follows from the fact that the square commutes at \idX Î C(X,X). Hence (x,a) = Qa. []

THEOREM 7.7.6 Suppose that

(a)
S¯ U has and p1 preserves []-structure ,

(b)
S satisfies the axiom-scheme of replacement, and

(c)
Q is a model of L, ie Q preserves any []- structure which L specifies.

Then \qqdash is full and faithful, ie [] is conservative.

In practice, p1 preserves []-structure on the nose, and [[-]] is defined by structural recursion so that [[G]] = ([[G]]0,G,\qG ), where [[-]]0 = p0[[-]].

The functor [[-]] reflects the existence of isomorphisms: if [[G]] º [[D]] somehow then G º D. (This is the categorical analogue of an injective function between posets.) For higher order logic, [[-]] need not be full.

PROOF: Since Cn[]L is the classifying category, and using the axiom-scheme of replacement to justify the recursion, the model Q extends to a []-preserving functor [[-]]:Cn[]L® S¯ U making the upper triangle commute, uniquely up to unique isomorphism:

omitted diagram environment

The lower Cn[]L is also a model, for which both id and p1[[-]] serve as the mediator from the classifying category (since [[-]] and p1 preserve []- structure), so they are isomorphic, p1[[G]] º G. Hence [[-]] is faithful, whilst Q is full and faithful, so \qqdash is also full and faithful. []

EXAMPLES 7.7.7 The first clause of the theorem is applicable to the structures [] listed in Corollary 7.7.2 (and more). The difficulty lies in condition 7.7.6(c), ie what structure is named by the language L.

(a)
L may be just the canonical elementary language of C, with no extra structure.

(b)
L may also include some tuple maps, or, more generally, encoding operations for some finite limits (Definition  7.6.5). Then C, Cn[]L, S and S¯ U have these limits and \H(-), \qqdash , U and Q preserve them.

(c)
L also includes some stable colimits, encoded by a Grothendieck topology J. The category S = SetCop of presheaves must be replaced by the category Shv(C,J) of sheaves, which freely adjoins colimits, but keeping those in J, cf Theorem 3.9.7 for posets.

(d)
Corollary 7.7.13 shows that Q and A also preserve exponentials.

The construction relies on the fact that S, which is a topos, has all of the extra structure [] (plus the axiom-scheme of replacement) and the Yoneda embedding is full and faithful and preserves it. However, S does not freely adjoin this structure (except in the case of arbitrary stable colimits), and the question is whether the embedding into the free category Cn[]L is full and faithful.

REMARK 7.7.8 In the case C = {1}, an object If® UG º Cn[]L(1,G) of S¯ U is a family of closed terms or proofs of G, indexed by I. More generally, it is a cocone \Fredi:\qq \typeXi®G of such proofs under a certain diagram \typeX(-):Á® C of base types or hypotheses. This diagram is the discrete fibration corresponding to the sheaf I:Cop® Set by Proposition 9.2.7.

Notation 7.7.3(b) provided a specific sheaf of closed terms \qX of each base type X Î obC, so we shall call it the realisation of X. Theorem 7.7.6 showed that this is an isomorphism (the realisation is tight) for base types, and extended the notation to general contexts. We already know that the full subcategory of tight objects in S¯ U is closed under definable limits, so the same is true of the class of tightly realised contexts. We shall see that this extends to colimits and exponentials, so if [] consists only of this (first order) structure then A is already the interpretation [[-]], and this is full as well as faithful.

For higher order logic the realisation is no longer tight. Andre Scedrov and Philip Scott [SS82] trace the method back in the symbolic tradition to Stephen Kleene's realisability methods (1962), and link it to the categorical construction. Peter Freyd found this after hearing the presentation of Scott's work with Joachim Lambek [ LS80] at a conference, and not at first believing the theorem below which their results implied.

Existence and disjunction properties   Recall that [[-]]0 º p0·[[-]].

LEMMA 7.7.9 The realisation q:[[-]]0® U is naturally split epi.

PROOF: First observe that, by the Yoneda lemma (Theorem  4.8.12(c)),

S([[\qqdash ]]0,[[G]]0) = S(\H(-) ,[[G]]0) º [[G]]0.
The section m:U® [[-]]0 (called u in [AHS95]) is the action of [[-]]0,
Cn[]L(\qqdash ,G) ® ([[-]]0 )\qqdash ,G S([[\qqdash ]]0,[[G]] 0) º [[G]]0
naturally in (- and) G. We have to show that \qG (\mG(u)) = u for each u Î UG º Cn[]L(\qqdash ,G), along the bottom row of the next diagram. Evaluating this equation at each X Î obC, we use naturality with respect to \uX:\qq X® G.

omitted diagram environment

Then the diagram in Set commutes and the required law follows from its effect on \idX Î C(X,X). []

THEOREM 7.7.10 [Freyd] U:Cn[]L® S preserves colimits named in [], but not necessarily those named in L . In particular, the global sections functor (Example  7.7.4) preserves

(a)
the initial object, so there is no closed term \vdash 0 in Cn[];

(b)
coproducts, so there are just two closed terms \vdash 2 ;

(c)
regular epis, so 1 is projective (Remark  5.8.4(e));

(d)
coproducts and coequalisers (Example  6.4.13), so the closed terms \vdash N are the numerals. []

PROOF: We have just shown that U is a retract of [[-]]0, which preserves whatever colimits are in [], and hence so does U (Exercise  7.13). []

COROLLARY 7.7.11 In terms of proof theory, the fragment []

(a)
is consistent;

(b)
has the disjunction property: if \vdash fÚy then either \vdash f or \vdash y;

(c)
has the existence property: if \vdash $x.f[x] then \vdash f[a] for some a;

(d)
has standard arithmetic. []

S can prove consistency of [] because it has been strengthened with the axiom-scheme of replacement, to which we return in Section  9.6.

Exponentials   Recall that [I® J](X) = S(\HXxI,J) by Exercise 4.41, whilst UG(X) = Cn[]L(\qq X,G) by Notation 7.7.3(a).

PROPOSITION 7.7.12 Suppose A and S are cartesian closed, S has pullbacks and U preserves finite products. Then S¯ U is cartesian closed and p1 and A (but not p0 or U) preserve exponentials. (See Exercise 3.72 for the version for Heyting semilattices.)

PROOF: Given (If® UG) and (Jg® UD) in S¯ U, we form an internal version of the hom-set (S¯ U)(f,g), namely the pullback

omitted diagram environment

in S, where the lower left map is the exponential transpose of

UGxU[G® D] º U æ
è
Gx[G® D] ö
ø
® Uev UD.
Then (Hh® U[G® D]) is the required exponential, with l-abstraction

omitted diagram environment

Notice that if g is an isomorphism, then so is h. []

COROLLARY 7.7.13 Q preserves any exponentials that are named in L. If D has tight realisation then so does [G® D] for any G whatever.

PROOF: In computing Q(X® Y), the edges of the pullback square above are all invertible, the vertices being isomorphic to \HX® Y. []

THEOREM 7.7.14 [Yves Lafont, [Laf87, Annexe C]] The l- calculus is a conservative extension of algebra. []

This is as much as is needed for the equivalence between semantics and syntax in Theorem 7.6.9. We haven't proved the normalisation theorem as such, but by a variation on this technique every term is provably equal to a normal form [MS93, AHS95,CDS98]. It seems likely that a purely categorical proof will be found for strong normalisation itself, handling reduction paths in the fashion of Exercise  4.34. We return to consistency and the axiom of replacement in Section 9.6.