11  Sums and quotients

Paré’s theorem, that any elementary topos has the monadic property [Par74], which originally inspired abstract Stone duality, was itself motivated by the simple way that it affords for constructing colimits. So we conclude this paper with applications of the comprehension calculus to coproducts and coequalisers.

Example 11.1 The idea of Stone duality is to consider spaces in terms of the corresponding algebras. For any algebra (A,α), we have

in which η_A·α is a nucleus (Definition 8.7) because of the Eilenberg–Moore equations for α. The homomorphism H:B→ A corresponds to the function

in which H is behaving as a continuation-transformer. (We saw in the previous section that the operators i and admit merely serve as compile-time type-annotation.) In particular, if H≡Σ^f, where f:X→ Y, this is just focus(λψ.ψ(f x)) = f x by Lemma 8.11.         ▫

The continuation-passing style is more clearly visible in a more complicated example.

Example 11.2 The coproduct X+Y of spaces corresponds to the product A≡Σ^X×Σ^Y of algebras, whose structure map α≡<P₀,P₁> was given in Lemma 5.5:

Then X+Y ≡ pts(A,α) ≡ {Σ^ΣX×ΣY ∣ E_X+Y}, where

The inclusion ν₀:X→ X+Y satisfies Σ^ν₀= π₀, so

Then, for f:X→ Z and g:Y→ Z, the mediator X+Y→ Z is

in which the continuation θ from Z is passed either as θ· f to X or as θ· g to Y. When u≡ ν₀(x) or ν₁(y), one of the two branches is selected and that continuation is applied to x or y.         ▫

We already know that products distribute over coproducts (Proposition A 7.11), and coproducts are disjoint and stable under pullback on the assumption that Σ is a distributive lattice and satisfies the Euclidean principle (Section C 9). In fact this extra structure is unnecessary: if (S,Σ) is monadic then S is extensive on a very much weaker assumption.

[The initial object 0 is strict (X×0≅0) by sobriety, because

For disjointness of coproducts, the square is a pullback iff the upper right diagram is an equaliser. By monadicity, this happens iff the lower right diagram is a coequaliser, which it is iff Σ↠1 is regular epi.

The following results are based on the stronger assumption that this map is split epi, which it is in topology. It seems unlikely that any other application would require the weaker hypothesis.]

Lemma 11.3 The map 0→1 is a Σ-split mono iff Σ has a constant.

Proof    I:Σ⁰≡ 1→Σ≡ Σ¹.         ▫

If I≡ ⊤, this makes 0 a closed subspace; if I≡ ⊥ then it’s open (Examples 2.5). However, we shall call the constant ⋆ here to emphasise that we are not using any lattice structure. Then coproduct inclusions are also Σ-split monos:

Lemma 11.4     X≅{X+Y ∣ <π₀,⋆>} and Y≅{X+Y ∣ <⋆,π₁>}.

Proof    These idempotents arise from the diagram

        ▫

We want to show that every map U→2 arises in this way from a unique coproduct. Because of the continuation-passing behaviour, it is convenient to treat 2 as a subspace of Σ^Σ×Σ. Then the definable elements are π₀≡λ x y.x and π₁≡λ x y.y, which simply select the appropriate continuation from the pair.

Lemma 11.5     2 ≅  {Σ^Σ×Σ ∣ λF F.F(Fπ₀,Fπ₁)}.

Proof    This is the primality equation, F P ⇔ P(λ x.F(λφ.φ x)), with λ x replaced by the two values 0,1:2, and φ:Σ² by a pair.         ▫

We shall abuse our language by calling the two-argument functions P:Σ^Σ×Σ that belong to this subspace “prime”. However, we need yet another characterisation of them.

Lemma 11.6     Γ⊢ P:Σ^Σ×Σ is prime iff, for x,y,z:Σ and G:Σ^ΣΣ,

Proof    If P is prime, so Γ, F:Σ²(Σ×Σ) ⊢ F P   ⇔   P(Fπ₀,Fπ₁), then

• put F≡λ Q.x, so F P ⇔ Fπ₀ ⇔ Fπ₁ ⇔ x and primality says that x ⇔ P(x,x);
• put F≡λ Q.Q(Q(x,y),z), so Fπ₀ ⇔ x, Fπ₁ ⇔ z and P(P(x,y),z)≡F P ⇔ P(x,z);
• put F≡λ F.G(λ z.F(z,⋆)), so Fπ₀ ⇔ Gid, Fπ₁ ⇔ G(λ z.⋆) and primality says that G(λ z.P(z,⋆))≡ F P ⇔ P(Gid,  G(λ z.⋆)).

The converse is not needed in the following applications. We first put G≡λθ.F(λ x y.θ P(x,y)), so G(λ z.⋆) ⇔ F(λ x y.⋆), Gid ⇔ F P,

with which the equations involving G give

Next put G≡ λθ.F(λ x y.θ x), so

with which the first G-equation gives

and similarly G≡ λθ.F(λ x y.θ y) yields F(λ x y.P(⋆,y)) ⇔ P(F(λ x y.⋆), Fπ₁).

From these four consequences of the higher-type G-equations, together with the ones of base type, we deduce that P is prime:

Proposition 11.7 Let u:U⊢ P u:Σ^Σ×Σ be prime. Then the following subspaces are well defined, their coproduct is U and the squares are pullbacks.

Proof    To show that E₀ is a nucleus, we must show for u:U and F:Σ³ U that

is equal to

Put G≡λθ.F(λφ.θ(φ u)) in the Lemma. Then

so P u(y,⋆) ⇔ P u(P u(x,t),⋆) ⇔ P u(x,⋆) as required.

To test that the left hand square is a pullback, we are given Γ⊢ v:U such that Γ⊢ P v=π₀. Then

as is required to form the mediator Γ⊢ admitv:{U ∣ E₀}.

To show that U is the coproduct, we must show that Σ^U is the associated product, i.e. that θ:Σ^U corresponds bijectively to <φ,ψ> where φ=E₀φ and ψ=E₁ψ. In fact, P serves for the pairing operation as well as for the projections: θ≡λ u.P u(φ u,ψ u).

        ▫

Theorem 11.8 If (S,Σ) is monadic and Σ has a constant then S is extensive, i.e. it has stable disjoint coproducts [Tay99, Section 5.5].

Proof    We have to show that the commutative diagram is a pair of pullbacks iff its top row is a coproduct. The map U→2 must arise from a prime u:U⊢ P u:Σ^Σ×Σ, from which Proposition 11.7 constructs subspaces forming pullbacks and a coproduct. Since pullbacks are unique up to isomorphism, if the given diagram is a pair of pullbacks then it is isomorphic to that in the Proposition.

Conversely, if we are given a coproduct U≡ X+Y then u:U⊢ P u:Σ^Σ×Σ is defined by x:X⊢ P x≡π₀ and y:Y⊢ P y≡π₁. Then E₀ in the Proposition becomes

which agrees with Lemma 11.4.         ▫

Corollary 11.9 Let x:X⊢ f x,g x:Z and x:X⊢ P x:Σ^Σ×Σ with P prime. Then

Turning from coproducts to coequalisers, of course we can only construct those that are Σ-split. We leave the reader to formulate Beck-style equations as in Section 3, concentrating instead on the analogue for quotients of the comprehension calculus for subspaces in Section 8. Beware also that the class of Σ-epis is stable under products but not necessarily pullbacks. For the topological motivation, recall that the quotient topology on a set Y induced by the function q:X→ Y from a topological space has V⊂ Y open iff q⁻¹V is open in X.

Lemma 11.10 Let

be a Σ-split epi, and put R≡Q· q. Then

Proof    Three of the four squares

commute by naturality, but that from Y to Σ² X need not. So E is the composite from Σ² X anticlockwise back to itself:

so EF F  ⇔  η_Σ^X(Σ^η_X(Σ² R F)) F  ⇔  F(λ x.F(λφ. Rφ x)). Next,

whence q x = admit(λφ. Rφ x). Finally, i yφ  =  Σ^Q(η_Y y)φ  =  (λφ. φ y)(Qφ)  =  Qφ y.         ▫

Proposition 11.11 Y≡ X/R ,   q x ≡ [x] and

satisfy the rules

/E

/β

together with those for the quotient topology (Σ^/ I, Σ^/ E, Σ^/ β and Σ^/ η),

Proof    We verify the /β and /η rules:

Remark 11.12 Notice that the β-rule is not a computational reduction, but a denotational equation that is a consequence of the equation R(θ· f)=(θ· f) in its hypothesis. A compiler equipped with a proof assistant might perhaps be able know this, but otherwise we can only hope that the implementation will somehow find its way from one side of the β-rule to the other.

Let us specialise this to sets and (discrete) topological spaces, now making use of the lattice structure.

Example 11.13 Section C 10 constructs the quotient X/δ of an overt discrete object X by the open equivalence relation classified by δ:X× X→Σ. Overt discrete means that X is equipped with predicates ∃_X:Σ^X→Σ and (=_X):X× X→Σ satisfying the usual properties.

The construction in Lemma C 10.8 obtains Σ^X/δ (which is unfortunately called Σ^Q=E there, for “quotient” and “equaliser”) as a retract of Σ^X, namely as the image of the closure operation

The quotient space is therefore X/δ=X/R={Σ² X ∣ E}, where

If f:X→ Z respects the equivalence relation δ then the β-rule is

In principle this computation involves a search of the equivalence class, which makes sense, given the connection between coequalisers and while programs [Tay99, Section 6.4].

Example 11.14 As explained in Remark C 10.12, there is another representation of X/δ that is more like the familiar one with equivalence classes. It arises from the factorisation

of the transpose of the equivalence relation. This generalises

cf. Section A 10. The quotient is now given by {Σ^X ∣ E}, where

with q x ≡ admit(λ y.δ(x,y)).

If f:X→ Z respects the equivalence relation then the mediator X/δ→ Z is

This selects an element x′ from the equivalence class y∈ X/δ (classified by a predicate i y∈Σ^X) and applies f to it, as we would expect. Substitution of y ≡ q x yields the same formula focus(λθ.∃ x′.δ(x,x′)∧θ(f x′)) as before.         ▫

Remark 11.15 Here is a summary of the comprehension types that we have used.