Previous Up Next

6  Enforcing sobriety

Now we turn from the analysis to the synthesis of categories that have all objects sober. So our primary interest shifts from locales to the restricted λ-calculus in Remark 2.1.

Since we handle continuous functions f:XY in terms of the corresponding inverse image maps Σf, it is natural to work in a category in which there are both “first class” maps f:XY (given concretely by homomorphisms ΣfY→ΣX) and “second class” maps F:X−× Y that are specified by any FY→ΣX.

These second class maps — ordinary functions rather than homomorphisms between algebras — are just what is needed to talk about U-split (co)equalisers as in Beck’s theorem (cf. Proposition 4.9 and [B]). Even in more traditional subjects such as group and ring theory, we do indeed sometimes need to talk about functions between algebras that are not necessarily homomorphisms.

The practical reason for according these maps a public definition is that the product functor is defined for them (Proposition 6.5), and this will be crucial for constructing the product of formal Σ-split subspaces in [B]. After I had hesitated on this point myself, it was seeing the work of Hayo Thielecke [Thi97b] and Carsten Führmann [Füh99] on continuations that persuaded me that this is the best technical setting, and this section essentially describes their construction.

As to the first class maps, the whole point of sobriety is that they consist not only of f:XY in C, but other maps suitably defined in terms of the topology.

Definition 6.1 The categories HC and SC both have the same objects as C, but

  1. the (second class) morphisms F:X−× Y in HC are (any) C-morphisms
    FY→ΣX, cf. Remark 3.13, and
  2. the (first class) morphisms H:XY in SC are C-morphisms HY→ΣX that are homomorphisms (Definition 3.4):

    Thielecke and Führmann call these thunkable morphisms, since they write thunkX for ηX considered as an HC-map. It follows immediately (given Theorem 3.10) that ηX:X→ΣΣX is natural in SC but not HC.

Identity and composition are inherited in the obvious way from C, though contravariantly, which is why we need the F notation (which [Sel01, Section 2.9] also uses).

Remark 6.2 By Lemma 3.6, for f:XY in C, the map HfY→ΣX is a homomorphism, so H:XY is in SC. We shall just write this as f:XY instead of Σf:XY, but beware that, in general, different C-maps can become equal SC-maps with the same names.

By Remark 4.2, this functor CSC is faithful iff every object of C is T0, and it also reflects invertibility if every object is replete. Theorem 4.10 said that it is also full iff every object of C is sober; as SC and C have the same objects, they are then isomorphic categories.

There are, of course, many more morphisms in HC than in C, but one (family) in particular generates the rest. We shall see that the new second class morphism force2 X−× X objectifies the operation PfocusP that is only defined when P2 X is prime. Thielecke and Führmann apply their β-rule for force without restriction, producing computational effects, whilst our side-condition on focus gives it its denotational or topological meaning.

Definition 6.3 forceX = ηΣX : ΣΣX −× X is a natural transformation in the category HC, and satisfies ηX;forceX=idX or force(thunkx)=x.

Proof    This is Lemma 2.10 again. force(−) in HC is ηΣ(−) in C, which is natural (in C) with respect to all maps FY→ΣX, so force(−) is natural (in HC) with respect to F:X−× Y. The other equation is ηΣXηX=idX.         ▫

Corollary 6.4 The C-map ηX:X→Σ2 X is mono in both HC and SC.

Proof    It is split mono in HC, and remains mono in SC because there are fewer pairs of incoming maps to test the definition of mono.         ▫

Proposition 6.5 For each object X, the product X×− in C extends to an endofunctor on HC. This construction is natural with respect to C-maps f:XY (so Hf).

Proof    For J:V−× U in HC, i.eJU→ΣV in C, we write X× J:X× V−× X× U for the C-map JXX× U→ΣX× V. This construction preserves identities and composition because it is just the endofunctor (−)X defined on a subcategory of C. It extends the product functor because, in the case of a first class map g:VU (so JgU→ΣV), we have X× J=X×Σg=ΣX× g=X× g, which is a first class map X× VX× U.

The construction is natural with respect to f:XY because J(−) is.         ▫

Example 6.6 The existential quantifier ∃Γ in the context Γ is obtained in this way, and its Beck–Chevalley condition with respect to the substitution or cut f:Γ→Δ Proposition C 8.1 is commutativity of the square (cf. Proposition 5.5):

Example 6.7 × is not defined as a functor of two variables on HC, because the squares

do not necessarily commute (+ [FS90]). For example, take F=J:Σ−×0 where F=J0=1→ΣΣ is the element ∼id∈ΣΣ; then these two composites give the elements ∼π0,∼π1∈ΣΣ×Σ.

Remark 6.8 × is a premonoidal structure on HC in the sense of John Power [Pow02], and a map F makes the square commute for all J iff F is central (Definition 2). Thielecke, Führmann and Selinger begin their development from HC as a premonoidal category, whereas we have constructed it as an intermediate stage on the journey from C to SC.

Definition 6.9 F:X−× Y is discardable or copyable respectively if it respects the naturality of the terminal (or product) projection (!) and the diagonal (Δ).

These terms are due to Hayo Thielecke [Thi97a, Definition 4.2.4], who demonstrated their computational meaning (op. cit., Chapter 6). In particular, non-terminating programs are not discardable, but he gave examples of programs involving control operators that are discardable but not copyable, so both of these properties are needed for a program to be free of control effects such as jumps (Remark 1.5). In fact, these conditions are enough to characterise first class maps in the topological interpretation [F], but not for general computational effects [Füh02]. [See the appendix to [F].]

Lemma 6.10 Δ is natural in SC, i.e. all first class maps are copyable.

Proof    As in Lemma 3.7, we show that the above diagram commutes by making it into a cube together with

which commutes by naturality of Δ in C, as do the side faces of the cube, the other edges being ηX, ηX×ηY, etc. The top and bottom faces commute because H is a homomorphism and by naturality of H(−) and (Σ2 H)(−) with respect to ηX and ηY. The original diagram therefore commutes because ηY×ηY is mono by Corollary 6.4.         ▫

Proposition 6.11 SC has finite products and CSC preserves them.

Proof    The terminal object 1 is preserved since Σ is the initial algebra (Lemma 3.12). The product projections and diagonals are inherited from C, so Δ;p0=id=Δ;p1 and Δ;(p0× p1)=id.

Then, for SC-maps a=H:Γ→ X and b=K:Γ→ Y, we obtain <a,b> as Δ;a× b, but we need centrality (Lemma 3.7) to make a× b well defined.

The issue is that the squares commute. In C, the upper one is

using one of the two definitions for H×K=a× b. The left-hand square commutes by Lemma 3.7 because KY→ΣΓ is discardable (as it is a homomorphism), and the right-hand square by naturality of H(−)X×(−)→ΣΓ×(−) with respect to !:Y1.

For uniqueness, suppose that f;p0=a and f;p1=b. Then

  f=fX× Y;(p0× p1
 =ΔΓ;(f× f);(p0× p1)         naturality of Δ
 =ΔΓ;(a× b)         × is a functor on SC
 =<a,b>         ▫

Previous Up Next