Cartesian Closure for Stable Categories (draft)

Paul Taylor

1989

1 Rigid Adjunctions

1.1 Rigid Comparisons

It is not apparent what meaning, if any, is to be attached to the group of automorphisms of a rigid comparison (perhaps this is a kind of “gauge invariance”) but in view of the lemma it seems we can ignore it and make the

Definition 1.1 RC is the category whose (?)

• objects are stable categories, i.e., for our purposes so far, categories with pullbacks, and

• morphisms are isomorphism classes of rigid comparisons (the right adjoints are also considered to exist only “up to isomorphism”).

The symbol RC, like the term stable category, is considered as a variable, parametric upon our specific requirements.

Exercises 1.2

(a) Composition in RC is well-defined by representatives.

(b) A morphism of RC is invertible ⟺ it is a class of strong equivalences ⟺ its counit is an isomorphism.

(c) Objects of RC are isomorphic iff they are equivalent categories.

(d) RC/T ≃ Copt(T ) (?). □

Rigid comparisons embody an important idea from domain theory: approximation. This must have the property that if X′ approximates X then [X′ → Y] approximates [X → Y] and not vice versa as with precomposition with ordinary maps. Considering a stable functor to be given by its trace, we consider the diagram

[figure: X; C; T; F; Y; X′; Ξ; C′; T′; Φ; F′; Y′; Ψ]

in which C and C′ are comparisons, F and F′ isotomies and Ξ, Ψ and Φ are rigid comparisons (which are both comparisons and isotomies). As in the definition of RC, we interpret “rigid comparison” as an isomorphism class, and the diagram is to commute up to isomorphism. The idea is that the functor F′H′ : X′ → Y′ approximates F H : X → Y, and its domain and codomain are also approximations.

This corresponds to a definition of polymorphism suggested by Eugenio Moggi: we may see SCat as an internal category in itself. The category-of-objects is RC, and the categoryof-morphisms has trace factorisations as objects and diagrams like this as morphisms; domain, codomain and identity are obvious forgetful functors and composition is tensor product. Moggi’s definition of polymorphism is simply that SCat is an internal cartesian closed category which has products indexed by its category-of-objects.

1.2 Calculating Slices of Function-Spaces

We shall now calculate the category Copt(T ) = [T → T ]/id explicitly in terms of T , and hence show that the function-space [X → Y] has slices “of the same kind” as those of (X and) Y. First,

Exercise 1.3 If T has a terminal object then Copt(T ) ≃ T , i.e. the only rigid comparisons into a category with finite limits are slice maps. [Hint: consider M1; cf. Lemma 2.2.4.] □

Lemma 1.4 T ↦ T /T induces an isotomy

T /− : T → RC

whose effect on morphisms, t : T′ → T, is given by the pair t_{!} ⊣ t^{∗}. Proof Its restriction to T /T_{0} is the equivalence T /T_{0} ≃ Copt(T /T_{0}) ≃ RC/(T /T_{0}). □

(?) There are forgetful (pseudo)functors RC → Cat and RC^{op} → Cat which take a rigid adjunction to its left and right parts respectively. Of course, we have the

Exercise 1.5 T is the (pseudo)colimit of the diagram T → RC → Cat. □ More interestingly,

Proposition 1.6 Copt(T ) is the (pseudo)limit of the diagram T^{op} → RC^{op} → Cat. Proof What is an object of this limit? It is an assignment of an object κ_{T} : MT → T of T /T to each object T ∈ T , consistently with the diagram, in the sense that t^{∗}(κ_{T}) = κ_{T′} for each t : T′ → T. This is exactly the content of the pullback square

[figure: MT′; Mt; MT; T′; κ_{T′}; t; T; κ_{T}]

which asserts that κ : M → id is a cartesian transformation. This is enough to determine an object of Copt(T ). A similar argument applies to morphisms. □

Lemma 1.7 Any two subfunctions of the identity commute (up to canonical isomorphism), their composite being their product in Copt(T ). Proof Consider the two pullback diagrams which express naturality of κ_{1} and κ_{2} respectively:

[figure: M_{1}; κ_{1}; id; M_{1}M_{2}; M_{1}κ_{2}; κ_{1}M_{2}; M_{2}; κ_{2}; and; M_{1}; κ_{1}; id; M_{2}M_{1}; κ_{2}M_{1}; M_{2}κ_{1}; M_{2}; κ_{2}]

There is a unique mediating isomorphism τ : T_{1}T_{2} ≅ T_{2}T_{1}. These diagrams are also clearly product diagrams in Copt(T ). □

Proposition 1.8 RC has pullbacks and Copt(T ) has finite limits. Moreover these limits are constructed pointwise, and a pullback of rigid comparisons quâ rigid comparisons is also a pullback quâ (stable) functors. Proof By the equivalence RC/T ≃ Copt(T ) we have just constructed a typical pullback in RC. Observe that objects of the pullback category, i.e. M_{1}M_{2}-coalgebras, correspond to pairs of objects at the other corners, i.e. a M_{1}-coalgebra together with a M_{2}-coalgebra whose carrier is isomorphic. This follows immediately from the fact that M_{1}M_{2} is defined by a pullback. To construct a pullback over M in Copt(T ) we find the product in Copt(T )/M ≃ Copt(trace(M)); but Copt(T ) also has a terminal object, so we can obtain all finite limits. □

Exercise 1.9 Prove Propositions 2.6.4 and 2.6.6 directly for [X → Y]/S. □

Corollary 1.10 Pullbacks of stable functors and cartesian transformations exist and are calculated pointwise. □

We need pullbacks to be constructed pointwise in order that they be preserved by evaluation.

Exercise 1.11 More generally if T has wide pullbacks of a given size then Copt(T ) has limits and [X → Y] and RC have wide pullbacks of that size. These are calculated pointwise, and hence preserved by evaluation. □

1.3 Special Adjoint Functor Theorem

We have almost proved that SCat is cartesian closed, except that we have to use the Adjoint Functor Theorem to prove that evaluation is stable, and so we have to consider questions of size. This is really a form of spread, which we shall discuss in the final section.

[This subsection is currently in a very sketchy state!]

Definition 1.12 A set G of objects coseparates a category X if for each pair f, g : X ⇉ Y, if every s : Y → G with G ∈ G has f ; s = g ; s then already f = g.

This is usually phrased in the negative way that if f ≠ g then there is some s : X → G with f;s ≠ g;s.) For example {2} coseparates Set. Obviously the whole object-set always coseparates: we are interested in the case where a set of objects of a large category suffices.

Conjecture 1.13 If ev_{X} : Copt(X) → X is stable for each X ∈ X then X has a set of coseparators. Proof Here is a pointwise-descending class of functors whose big limit is id, but no small subdiagram has this limit unless there is a set of coseparators. Let G be any set of objects of X. Let k_{0}^{G}X, k_{1}^{G}X : K^{G}X ⇉ X be the kernel pair of all arrows s : X → G with G ∈ G, i.e. for each s we form the pullback of s against itself, and then (for each of the projections) we form the wide pullback (in which the arrows are in fact mono). Unfortunately the k_{i}^{G} are not cartesian. Observe that k_{0}^{G} = k_{1}^{G} = id iff G coseparates, whilst if X ∈ G then k_{0}^{G}X = k_{1}^{G}X = id_{X}. There is a mediating map k_{i}^{G} → k_{i}^{G′} for G′ ⊂ G, and the big limit is id, but this is attained by G iff it coseparates. □

Definition 1.14 A category X is well-powered if for every object X there is a set of monos X′ ↪ X up to isomorphism in X /X.

Exercise 1.15 Let S : X → Y be stable with trace T . If T has a set of coseparators then Spec_{S}(Y) is a small groupoid, i.e. there is a set of components and each component group is small. In particular if Y has epi-mono factorisation and S is the inclusion of the monos then Y is co-well-powered. □

Proposition 1.16 (Special Adjoint Functor Theorem) Suppose X is complete, well-powered and locally small and has a set of coseparators. Then every functor H : X → Y has a left adjoint iff it preserves limits. □

[Coseparators in slices?]

Lemma 1.17 Suppose X has a final set G and Y is locally small and well-powered. Then [X → Y] is locally small and well-powered. Proof It suffices to show that for S_{1}, S_{2} : X ⇉ Y, if ϕ, ψ : S_{1} ⇉ S_{1} are cartesian transformations with ϕ_{G} = ψ_{G} for all G ∈ G then ϕ_{X} = ψ_{X} for all X ∈ X. Given X, let s : X → G; then ϕ_{X} = (S_{2}s)^{∗}ϕ_{G} = (S_{2}s)^{∗}ψ_{G} = ψ_{X}. The same method applies to being well-powered. □

1.4 The Pushout-Pullback Coincidence

The limit-colimit coincidence is a very famous result in domain theory which is the basis of the solution of recursive domain equations. An analogous result holds for stable domains, but its proof is of a rather different character from the results of this paper, so we do not discuss it here. However our present theory has its own limit-colimit coincidence, for wide pullbacks of rigid comparisons and the corresponding pushouts of their right adjoints. First we show that a wide pullback of rigid comparisons is also a pullback quâ ordinary functors.

Lemma 1.18 Let M = lim M_{i} be a limit diagram in Copt(X) and C_{i} : T → Coalg(M_{i}, κ_{i}) a cone of comparisons over the diagram Φ_{u} : Coalg(M_{i}, κ_{i}) → Coalg(M_{j}, κ_{j}) of forgetful functors. Then the mediator C : T → Coalg(M, κ) is a comparison. Proof An object of Coalg(M, κ) is of the form \underline{X} = (X, (α_{i})) where α_{i} : X → M_{i}X is a cone over the diagram with arrows κ_{u} : M_{i} → M_{j}, so that X_{i} = Φ_{i}\underline{X} = (X, α_{i}) is an M_{i}-coalgebra. As usual Φ_{i} ⊣ Θ_{i} with unit ι_{i} and counit κ_{i}, etc. An M-homomorphism is an X -map which is simultaneously a homomorphism at each i.

In particular for T ∈ T , we have CT = (C_{0}T, (β_{i})), where C_{i}T = (C_{0}T, β_{i}), i.e. the cone commutes exactly. Suppose C_{i} ⊣ H_{i} with unit η_{i} and counit ϵ_{i}, where for simplicity we assume that the cocone also commutes exactly, i.e. H_{j} = H_{i}Θ_{u} with

η_{j} = η_{i} ; H_{i}ι_{u}C_{i}  and  ϵ_{j} = Φ_{u}ϵ_{i}Θ_{u} ; κ_{u}  (1)

Now consider the diagram in T with arrows of the form

H_{i}X_{i} \overline{\begin{matrix}H_{i}ι_{u}X_{i} \\  \end{matrix}}H_{i}Θ_{u}Φ_{u}X_{i} = H_{j}X_{j}

Since this diagram has a terminal vertex we may take its limit, H\underline{X}, with limiting cone γ_{i}\underline{X} : H\underline{X} → H_{i}X_{i}, i.e.

γ_{j}\underline{X} = γ_{i}\underline{X} ; H_{i}ι_{u}X_{i}  (2)

It is easy to show that γ_{i} : H → H_{i}Φ_{i} is cartesian, so if H_{i} is continuous and T is pullbackcontinuous then we deduce from Lemma 3.3.6 that H is also continuous.

For T ∈ T the units of the adjunctions C_{i} ⊣ H_{i} afford a cone η_{i}T : T → H_{i}C_{i}T over a diagram of the above form (by (1)), so let ηT : T → HCT be its mediator; then

η_{i}T = ηT ; γ_{i}CT  (3)

We define ϵ by

Φ_{i}ϵ\underline{X} = C_{i}γ_{i}\underline{X} ; ϵ_{i}X_{i}  (4)

This is justified because

C_{j}γ_{j}\underline{X} ; ϵ_{j}X_{j}
= C_{j}(γ_{i}\underline{X} ; H_{i}ι_{u}X_{i}) ; (Φ_{u}ϵ_{i}Θ_{u}Φ_{u}X_{i} ; κ_{u}X_{j})  by (1) & (2)

= C_{j}γ_{i}\underline{X} ; Φ_{u}ϵ_{i}X_{i} ; Φ_{u}ι_{u}X_{i} ; κ_{u}X_{j}  naturality of Φ_{u}ϵ_{i}
= C_{j}γ_{i}\underline{X} ; Φ_{u}ϵ_{i}X_{i}  Φ_{u} ⊣ Θ_{u}
= Φ_{u}(C_{i}γ_{i}\underline{X} ; ϵ_{i}X_{i})

Then

Φ_{i}(CηT ; ϵCT)
= C_{i}ηT ; C_{i}γ_{i}CT ; ϵ_{i}C_{i}T  by (4)
= C_{i}η_{i}T ; ϵ_{i}C_{i}T  by (3)
= id  C_{i} ⊣ H_{i}

and

(ηH\underline{X} ; Hϵ\underline{X}) ; γ_{i}\underline{X}
= ηH\underline{X} ; γ_{i}CH\underline{X} ; H_{i}Φ_{i}ϵ\underline{X}  construction of Hϵ
= ηH\underline{X} ; γ_{i}CH\underline{X} ; H_{i}C_{i}γ_{i}\underline{X} ; H_{i}ϵ_{i}X_{i}  by (4)
= η_{i}H\underline{X} ; H_{i}C_{i}γ_{i}\underline{X} ; H_{i}ϵ_{i}X_{i}  by (3)
= γ_{i}\underline{X} ; η_{i}H_{i}X_{i} ; H_{i}ϵ_{i}X_{i}  naturality of η_{i}
= γ_{i}\underline{X}  C_{i} ⊣ H_{i}

so C ⊣ H. □

Theorem 1.19 Given a wide pullback diagram of rigid comparisons, the pullback of the comparisons quâ functors, the pushout of their right adjoints quâ functors and the pullback of the comparisons quâ rigid comparisons all exist and are equivalent. Proof We have to show that a pullback of rigid comparisons is the pushout of their right adjoints; by the equivalence RC/X ≃ Copt(X) we may assume that the diagram is equivalent to the special form in the lemma. Let S_{i} : X_{i} → Y be a cocone of stable functors over the diagram Θ_{u}. Applying the trace factorisation to each of them, we find that they share the same isotomy part (up to equivalence), so they factor through H_{i} : X_{i} → T and F : T → Y with C_{i} ⊣ H_{i}. Then C_{i} : T → X_{i} is a cone of comparisons over the (pointwise) limit diagram, and so there is a mediator C : T → X, which by the lemma has a (continuous) right adjoint H. This mediates for the cocone H_{i} and so S = F H mediates for S_{i}. Given another mediator, we may take its trace factorisation, of which the isotomy part must be F, whilst the comparison part mediates for the limit diagram and so must be C. □

The true significance of this result is domain-theoretic, so we shall postpone discussion to the next section.

Lemma 1.20 Let Y be a stable category and X and X_{i} be as in Lemma 2.8.1. Then the mediator

[colim_{i} X_{i} → Y] → lim_{i} [X_{i} → Y]

is an equivalence. Proof The functor is simply the correspondence between mediators S = F H : X → T → Y and cocones S_{i} = F H_{i} : X_{i} → T → Y. This is essentially surjective by definition of colim and we have to show that it is full and faithful. Cartesian transformations ϕ : S′ → S correspond to diagonals Φ : T′ → T . On the other hand, if ϕ_{i} : S′_{i} → S_{i} is a natural system of cartesian transformations, their diagonals Φ_{i} : T′ → T must coincide. □

The coincidence does not hold for pushouts and coequalisers of rigid comparisons. That leaves equalisers:

Exercise 1.21 Find a parallel pair of rigid comparisons which has no equaliser, although the corresponding pair of right adjoints has a coequaliser. [Hint: a five-point poset will suffice.] □

1.5 Rigid Comparisons — Notes

However this representation would appear to introduce 3-cells, namely cartesian natural transformations between rigid comparisons, into the 2-category SCat, and, by iteration, worse. However we already know from Definition 1.7.1 that these have no effect.

Lemma 1.22 Let Φ_{1}, Φ_{2} : T ⇉ T_{0} be rigid comparisons and τ : Φ_{1} → Φ_{2} a cartesian natural transformation between them. Then τ is invertible (the same is true for isotomies and functors with left adjoints, but, of course, not for arbitrary stable functors). Proof Φ_{1} and Φ_{2} are isotomies, and so are the second parts of their own (non-standard) trace factorisations, the first parts being identities. In order to make the triangles commute, any diagonal between them must be a (strong) equivalence. Hence the corresponding cartesian natural transformation τ is invertible, but (in the case where Φ_{1} = Φ_{2}) not necessarily the identity. The same argument applies to functors with left adjoints and isotomies. □

Lemma 1.23 Equivalent diagonals correspond to isomorphic subfunctions. Proof We interpret “equivalent” in the weakest possible sense. Let S_{0}, S_{1}, S_{2} : X → Y be stable functors with traces T_{0},, T_{1} and T_{2}, and ϕ_{1} : S_{1} → S_{0} and ϕ_{2} : S_{2} → S_{0} be cartesian natural transformations with diagonals Φ_{1} : T_{1} → T_{0} and Φ_{2} : T_{2} → T_{0}. Suppose that there is a strong equivalence I_{2} : T_{2} → T_{1} with pseudoinverse I_{1} such that Φ_{1}I_{2} ≅ Φ_{2}; then I_{1}Θ_{1} ≅ Θ_{2} and M = Φ_{1}Θ_{1} ≅ Φ_{2}I_{1}I_{2}Θ_{2} ≅ Φ_{2}Θ_{2}. Let κ′_{2} : M ≅ Φ_{2}Θ_{2} → id; then by Exercise 3.5.9 κ′_{2} ≅ κ_{1} : M → id and we can recover ϕ_{1} and ϕ_{2} using Lemma 3.4.8, whence ϕ′_{2} ≅ ϕ_{1}. □

In most of the examples of categories of stable domains which have been introduced the domains are posets, so the stronger property holds that any two rigid comparisons which are Berrycomparable are uniquely isomorphic. Unfortunately this simplification is not available in general, essentially because of the

Examples 1.24

(a) Let X be a group considered as a category with one object (•) and ϕ_{•} a nontrivial element of the centre of the group.

(b) Let X = VSp, the the category of (real) vector spaces, and ϕ_{X} be scalar multiplication by some fixed nonzero real number.

Then id : X → X is a rigid comparison with a nontrivial cartesian automorphism ϕ. □

2 Cartesian Closed Categories

2.1 The Limit-Colimit Coincidence

In this final section we shall conclude our investigation of cartesian closure by constructing filtered colimits in function-spaces, and then turn to the interpretation of first-order (dependent-type) polymorphism. In the terminology of [T85] we shall show that SCat is relatively cartesian closed with respect to rigid bifibrations. Second-order (impredicative) polymorphism may be treated in the same way by considering RC as a domain; unfortunately it is too big (in fact, too “wide”) for this to work unless we restrict attention to smaller domains. This is the subject of the final part of the paper: a systematic survey of what restrictions we may put on our domains whilst still being able to perform the constructions of interest. In this way we reproduce the previous work on specific subcategories of SCat and suggest new ones of potential interest.

Firstly, we must say something more about continuity (preservation of filtered colimits), which is the essential technical feature underlying the construction of fixed points and hence the modelling of recursion. We have made only passing reference to this topic, because stability and continuity are orthogonal concepts: each is more clearly understood in the absence of the other and (although this is not obvious) they may be combined with almost no interaction. For the most part, then, we have little to add to the traditional theory; in particular recursive domain equations such as X ≃ [X → X]_{⊥} may be solved in the usual way. The other ingredient needed for fixed points is an initial object (⊥), but this is just a special case of the general topic of spread, i.e. the complexity of polycolimits, which we shall discuss later.

The solution of recursive domain equations (in particular those involving the function-space functor) depends on a property called the limit-colimit coincidence, which was first noticed by Scott for complete lattices and is now well-known for sequences of embedding-projection pairs between domains of various kinds. It can be proved in general for FCCat (the 2-category of categories with small filtered colimits, continuous functors and natural transformations), although I know of no reference to a proof in the literature. Although it contains no surprises, the proof is notationally complicated and has nothing to do with stability, so we shall state the theorem without proof.

Theorem 2.1 Let T_{(−)} : I → FCCat be a filtered diagram whose arrows Φ_{u} : T_{i} → T_{j} are comparisons. Write Φ_{u} ⊣ Θ^{u} and T^{i} = T_{i}, so that the Θ^{u} are the arrows of a cofiltered diagram T^{(−)} : I^{op} → FCCat. Then

(a) the (pseudo)limit of the cofiltered diagram T^{(−)} and the (pseudo)colimit of the filtered diagram T_{(−)} both exist and are equivalent;

(b) corresponding functors Φ_{i} in the colimiting cocone and Θ^{i} in the limiting cone are adjoint;

(c) colim_{i} Φ_{i}Θ_{i} ≅ id in the common limit and colimit;

(d) this is also the (pseudo)colimit in the 2-category FCCat^{cp} whose morphisms are comparisons. □

We write bilim_{i} T_{i} for the common limit and colimit of the diagram. When we write “X = colim X_{i}” we mean that the context determines a diagram with typical vertex X_{i} and a cocone X → X_{i}, and that this cocone is (pseudo)colimiting; similarly “Y = lim Y_{j}”. “X = bilim X_{i}” means that both of these hold, and further that the corresponding arrows in the diagrams are adjoint, as are the cocones and cones.

Apart from the application to the solution of recursive domain equations, this has the important

Corollary 2.2 The covariant continuous function-space functor

(− → −) : FCCat^{cp} × FCCat^{cp} → FCCat^{cp}

is continuous. Proof The reader is invited to supply the diagrams and (co)cones in the following identities:

(bilim_{i} X_{i} → bilim_{j} Y_{j}) = (colim_{i} X_{i} → lim_{j} Y_{j})  the Theorem
= lim_{i} (X_{i} → lim_{j} Y_{j})  definition of colim
= lim_{i} lim_{j} (X_{i} → Y_{j})  definition of lim
= bilim_{i} bilim_{j} (X_{i} → Y_{j})  the Theorem

The identity (colim X_{i} → Y) = lim(X_{i} → Y) at the level Set is simply the correspondence between cocones X_{i} → Y and mediators colim X_{i} → Y. This is enriched over Cat because natural transformations between mediators correspond bijectively to natural families of natural transformations between the cocones; we shall spell this out in Lemma 3.1.5. Finally it is enriched over FCCat because the forgetful functor FCCat → Cat creates (pseudo)limits. The same applies to (X → lim Y_{j}) = lim(X → Y_{j}). The two bilimits may of course be interchanged. □

The same result will hold (for much the same reasons) in the stable case, but first we have to extend the theorem to rigid comparisons. We can do this by proving a separate result for isotomies.

Lemma 2.3 Let T be the colimit of a filtered diagram T_{(−)} : I → FCCat whose arrows Φ_{u} : T_{i} → T_{j} are isotomies. Then the functors Φ_{i} : T_{i} → T in the colimiting cocone are also isotomies. Proof Let 0 be an arbitrary point of I. Since I is filtered, replacing I by the coslice I\0 we may assume without loss of generality that this is the initial vertex, with î: 0 → i. Let X^{0} ∈ T_{0}; we have to show that Φ_{0} : T_{0}/X^{0} → T /Φ_{0}X^{0} is an equivalence.

Now T is generated by the images of the T_{i} together with filtered colimits; by filteredness we do not even need to consider composition. Hence any map f : Y → Φ_{0}X^{0} = X in T is at worst the mediator for a cocone over a filtered diagram, where the maps in the diagram and the cocone are images of T_{i}-maps. Let the diagram have vertices Y_{i} = Φ_{i}Y_{i}^{i} and arrows Φ_{j}y_{u}^{j} where y_{u}^{j} : Φ_{u}Y_{i}^{i} → Y_{j}^{j} for u : i → j in I, and let the cocone be f_{i} = Φ_{i}(f_{i}^{i} : Y_{i}^{i} → ΦîX^{0}).

But Φî is an isotomy, so Y_{i}^{i} ≅ ΦîY_{i}^{0} (without loss of generality equality holds) and f_{i}^{i} = Φîf_{i}^{0}, and then y_{u}^{j} = Φĵy_{u}^{0}. This reduces the diagram (y_{u}^{0} : Y_{i}^{0} → Y_{j}^{0}) and cocone (f_{i}^{0} : Y_{i}^{0} → X^{0}) to the level 0 ∈ I, and we may put Y^{0} = colim Y_{i}^{0} there, with mediator f^{0} : Y^{0} → X^{0}. Then Φ_{0}f^{0} mediates for the cocone in the colimit and hence f^{0} is the required lifting of f. Lifting triangles is similar. □

Lemma 2.4 Let T be the colimit of a filtered diagram T_{(−)} : I → FCCat and F_{i} : T_{i} → Y a cocone of isotomies, where Y is pullback-continuous. Then the mediator F : T → Y is also an isotomy. Proof Let T = colim Φ_{i}T_{i} ∈ T and y : Y → F T in Y. Form the pullback

[figure: F_{i}T′_{i}; F_{i}t_{i}; F_{i}T_{i}; Y; y; F T]

where we may write the upper map as an F_{i}-image because this is an isotomy. Then the right-hand side is a typical map in a colimiting cocone in Y and by pullback-continuity so is the left. Put T′ = colim Φ_{i}T′_{i} ∈ T , so that F T′ ≅ colim F_{i}T′_{i}, and let t : T′ → T mediate the cocone. Then t′ is the required F -lifting of y. Lifting triangles is similar. □

Lemma 2.5 The equivalence

[colim_{i} X_{i} → Y] = lim_{i} [X_{i} → Y]

is enriched over SCat. Proof We have to verify the correspondence between natural transformations between cocones and between mediators restricts to cartesian transformations. Let Θ_{i} : X → X_{i} and Φ_{i} : X_{i} → X be the limiting cone and colimiting cocone respectively, and C, D : colim_{i} X_{i} → Y. Clearly if α : C → D is cartesian then so is α_{i} = αΦ_{i} : CΦ_{i} → DΦ_{i} for each i, so we have to prove the converse. Since any object X ∈ X can be expressed as X = colim Φ_{i}X_{i} with X_{i} ∈ X_{i}, we may obtain α from α_{i} as the mediator between two colimits:

colim CΦ_{i}X_{i} ≅ CX \overline{\begin{matrix}αX \\  \end{matrix}}DX ≅ colim DΦ_{i}X_{i}

[figure: CΦ_{i}X_{i}; Cξ_{i}; α_{i}X_{i}; DΦ_{i}X_{i}; Dξ_{i}]

Morphisms x : X′ → X correspond to cocones x_{j} : Φ_{j}X′_{j} → X; any such map is of the form Φ_{j}x_{ij} ; Φ_{i}ξ_{i} with x_{ij} : X′_{j} → X_{i}, and in fact corresponds to an equivalence class.

We make a cube out of this diagram x : X′ → X in X and x_{ij} : X′_{j} → Φ_{u}X_{i} in X_{j}. The lower square is a pullback since α_{j} is cartesian. To show that the top is also, let y : Y → CX and z : Y → DX′ and form a cube with vertex Y_{ij} by pulling back against both of Cξ_{i} and Dξ′_{j}. Then by pullback-continuity we have Y = colim_{ij} Y_{ij} whilst by cartesianness of α_{j} we have w_{ij} : Y_{ij} → CΦ_{j}X′_{j}. Finally w : Y → CX′ is the mediator. (?) □

Theorem 2.6 The limit-colimit coincidence holds for filtered diagrams of rigid comparisons between pullback-continuous categories. Hence RC has filtered colimits and the covariant stablefunction-space functor [− → −] : RC × RC → RC preserves them. Proof The first part is a special case of the continuous version, except for saying that we have the filtered colimit in RC. But Lammas 3.1.4&5 show that the colimiting cocone and mediator are isotomies as well as comparisons. Continuity of the function-space is analogous to Corollary 3.1.2, except that we need Lemma 3.1.5 to show that the colimit identity is enriched; the limit version requires nothing else to be proved (exercise). □

Exercise 2.7 Let Φ_{i} : X_{i} → X be a cocone of rigid comparisons over a filtered diagram of them, with Φ_{i} ⊣ Θ_{i}. Show that this cocone is colimiting iff colim^{↑} Φ_{i}Θ_{i} ≅ id. [Hint: rigid comparisons are comonadic.] □

2.2 Filtered Colimits of Stable Functors

In this subsection we shall use the limit-colimit coincidence to show that the function-space [X → Y] has filtered colimits, and that they are preserved by evaluation. Let S_{i} : X → Y be stable functors for i ∈ I, with cartesian natural transformations ϕ_{u} : S_{i} → S_{j} for u : i → j in I. Let S_{i} = F_{i}H^{i} with C_{i} ⊣ H^{i} be the standard trace factorisation via T_{i}, and for u : i → j let Φ_{u} : T_{i} → T_{j} be the diagonal, so that

T_{i}

[figure: C_{i}; F_{i}]

X  Y

[figure: C_{j}; F_{j}]

T_{j} \begin{matrix}Φ_{u} \\  \end{matrix}

commutes “on the nose” and Φ_{u} ⊣ Θ^{u} for u : i → j.

We know from the limit-colimit coincidence, or indeed from general considerations of universal algebra, that the (pseudo)colimit, T , of the diagram (T_{i}, Φ_{u}) exists, with colimiting cocone Φ_{i}, and hence that there are continuous mediators C : T → X and F : T → Y so that the triangles

[figure: T; Φ_{i}; Φ_{j}; T_{i}; Φ_{u}; T_{j}; and; T; C; F; X; C_{i}; T_{i}; Φ_{i}; F_{i}; Y]

commute (up to natural isomorphism). In fact it will be possible to dispose of these irritating natural isomorphisms, because it will turn out that T is a trace and hence may be chosen to be standard.

Lemma 2.8 C and Φ_{i} are comparisons, say with C ⊣ H and Φ_{i} ⊣ Θ^{i}, whilst F and Φ_{i} are isotomies. Moreover colim_{i∈I} Φ_{i}Θ^{i} ≅ id_{T}. Proof From the last two parts of Theorem 3.1.1, and Lemma 3.1.3. □

Corollary 2.9 S = F H is a continuous stable functor and SX = colim S_{i}X. Proof F and H are stable. Since F and C mediate and C ⊣ H, etc., we have F_{i} ≅ F Φ_{i} and H^{i} ≅ Θ^{i}H. Then using the lemma,

F HX ≅ colim F Φ_{i}Θ^{i}HX ≅ colim F_{i}H^{i}X = colim S_{i}X

since F and H are continuous. □

It is easy to show that X ↦ colim S_{i}X defines a continuous functor which is the colimit with respect to continuous functors and arbitrary natural transformations, but showing by brute force that this functor is stable — let alone the colimit in the stable functor category — is very difficult. It is done in the poset case in [T88].

Theorem 2.10 The category [X → Y] of stable functors and cartesian natural transformations has filtered colimits, and ev : [X → Y] × X → Y preserves them. Proof Let S and S_{i} be as constructed, so that S is the pointwise colimit. Proposition 1.4.3 gives an equivalence between the category of traces and diagonals which are adjoint pairs, and by the limit-colimit coincidence T is also the colimit in this category. For fixed X ∈ X, ev(−, X) is continuous precisely because filtered colimits are constructed pointwise, whilst ev(S, −) is continuous because S is. But separate continuity of a function in two arguments suffices for joint continuity. □

Lemma 2.11 S is also the colimit in the category of stable functors and arbitrary natural transformations. Proof From Proposition 1.7.3 there is an equivalence between this category and the category of traces and equivalence classes of diagonals. Since natural transformations appear in the definition of diagonals, it would appear at first sight that we are faced with a lax colimit problem. However composition is defined in terms of Φ alone (and in fact we only need it up to isomorphism), so in fact it is an ordinary colimit given (by construction) by T . The F_{i} and (since the ϕ_{u} are cartesian) the C_{i} afford cocones, and so (T , C, F), and hence S, is the colimit. □

However the assumption that the natural transformations in the diagram are cartesian is necessary, because the pointwise colimit of stable functions is not in general stable.

Example 2.12 Let X = ℕ∪{∞} with the usual order and let Y be the Sierpinski space. Consider the (stable) functions S_{i} : X → Y where

S_{i}(x) = \{ \begin{matrix}⊤ & if i ≤ x ≤ ∞ \\ ⊥ & if 0 ≤ x < i \end{matrix}

Then (S_{i} : i ∈ ℕ) is a cofiltered system in the pointwise order, but

lim_{i∈ℕ} S_{i}( colim^{↑}_{x∈ℕ} x) = ⊤ ≠ ⊥ = colim^{↑}_{x∈ℕ} lim_{i∈ℕ} S_{i}(x)

so lim_{i} S_{i} is not continuous. By reversing the order we have a pointwise filtered system of stable functions whose colimit is not stable.

Exercise 2.13 Explain how we managed to prove that a pullback of continuous stable functors is continuous in section 2 whilst barely mentioning continuity. Also, why is our proof (using the Berry order) so radically different from the counterexample (in the pointwise order)?

Exercise 2.14 Show that [X → Y] has and ev preserves cofiltered limits by the same technique. The above proof is based on the obvious forgetful functor SCat → FCCat, but we may instead take a stable category to its opposite, hence interchanging the notions of comparison and homomorphism.

2.3 Dependent Sums

Suppose we have a domain Y[X] which depends on an object X ∈ X ranging over another domain. We may quantify over the variable X to give the dependent sum,

ΣX : X .Y[X] = {(X, Y) : X ∈ X , Y ∈ Y[X]}

or the dependent product,

ΠX : X .Y[X] = {(SX)_{X∈X} : ∀X ∈ X .SX ∈ Y[X]}

This is first order polymorphism, which we shall discuss in the next two sections. Replacing X by a “type of types” such as RC we obtain Girard-Reynolds second-order polymorphism, but there are size problems involved in this.

We have to make the definition of the dependent sum more functorial, so for x : X′ → X there is to be a rigid adjunction

Y[x]_{!} ⊣ Y[x]^{∗}

which is (pseudo)functorial in x, i.e.

Y[−] : X → RC

Y = ΣX : X .Y[X] is then given by the total category of X → SCat → Cat^{op}. This has objects the pairs (X, Y) where X ∈ X and Y ∈ Y[X] and morphisms (x, y) : (X′, Y′) → (X, Y) where x : X′ → X in X and either y : Y[x]_{!}(Y′) → Y in Y[X′] or equivalently y : Y′ → Y[x]^{∗}(Y) in Y[X]. The functor P : Y → X given by (X, Y) ↦ X is called the Grothendieck fibration, and for fixed X_{0} ∈ X we have injections ν_{X_{0}} : Y[X_{0}] → Y.

Definition 2.15 A functor p : Y → X is a bifibration if both it and p : Y^{op} → X^{op} are fibrations; this is equivalent to saying that substitution functors have left adjoints. (This term is due to Lamarche.) It is a rigid bifibration if the adjunctions are rigid.

It is well-known that this set-up interprets dependent sums: our purpose is to examine the specific results for stable categories.

Theorem 2.16 Suppose X and Y have pullbacks and P : Y → X is a rigid bifibration. Then the slices of Y are of the form Y_{0} ↓ T for some functor T : X_{0} → Y_{0}. Proof Let (X_{0}, Y_{0}) ∈ Y, i.e. X_{0} ∈ X and Y_{0} ∈ Y[X_{0}] = P^{−1}(X_{0}). Put X_{0} = X /X_{0} and Y_{0} = Y[X_{0}]/Y_{0}. Now define the functor T : X_{0} → Y_{0} on objects by

T (X →^{x} X_{0}) = (Y[x]_{!}(Y[x]^{∗}(Y_{0})) →^{κ} Y_{0})

and use the horizontal liftings afforded by Y[x]^{∗} to provide those for ξ : (X → X_{0}) → (X′ → X_{0}); in other words the definition on morphisms is essentially the same.

Now let (x, y) : (X, Y) → (X_{0}, Y_{0}) in Y, i.e. y : Y → Y[x]^{∗}(Y_{0}) in Y[X]. But Y[x]_{!} is an isotomy, so

Y[X]/Y[x]^{∗}(Y_{0}) ≃ Y[X_{0}]/Y[x]_{!}(Y[x]^{∗}(Y_{0})) ≃ Y_{0}/T x

In other words, (X, Y) is determined up to isomorphism by x and Y[x]_{!}(y) : Y[x]_{!}(Y) → T x, which is an object of Y_{0} ↓ T. The same applies to morphisms. Hence Y/(X_{0}, Y_{0}) → X /X_{0} is equivalent to the forgetful functor Y_{0} ↓ T → X_{0}. □

The functor T : X /X_{0} → Y[X_{0}]/Y_{0} is actually just the restriction of the indexation Y[−] : X → RC, as we may see by comparison with Proposition 2.6.4.

Corollary 2.17 The fibration and injections are stable. Proof We have to show that P and ν_{X_{0}} have left adjoints on slices.

[⊣ P] On slices P is Y_{0} ↓ T → X_{0} by (Y →^{w} T X) ↦ X. For X ∈ X_{0} let I → T X be the polyinitial candidate below T X, i.e. the initial object of Y[X]/T X; then the left adjoint is X ↦ (0 → T X).

[P ⊣] There is also a right adjoint on slices, given by X ↦ (T X → T X).

[⊣ ν_{X_{0}}] On slices ν_{X_{0}} is Y ↦ (Y → 1), which has left adjoint (Y →^{w} T X) ↦ Y (but no right adjoint). □

Proposition 2.18 In this notation the rigid comparisons and homomorphisms are given by composition and pullback, so for ξ : X′ → X in X_{0},

Y[ξ]_{!}(X′, Y′ →^{y′} T X′) = (X, (T ξ)_{!} y′)
Y[ξ]^{∗}(X, Y →^{y} T X) = (X′, (T ξ)^{∗}y)

where Y, Y′ ∈ Y_{0}, etc. (cf. Lemma 2.2.3 and Exercise 2.2.7; recall that f_{!} y = y ; f). □

Exercise 2.19 When does P has a left adjoint (cf. Exercise 1.7.7)? When is it an isotomy?

The magnitude of what we have just proved is easily overlooked. Imagine the base category as the frame of a weaving loom, with the fibres as the “warp”. The substitution functors form the “weft”, which may in the general case wander erratically, and so there is little redundancy in the description. However if these functors are rigid homomorphisms, once the top border has been woven (which may be arbitrary), the strands of the weft below it are parallel, and so the top row determines the structure of the whole tapestry. Hence lemmas like “a compact object of the total category is a compact object of a compact fibre” become obvious corollaries.

In fact it can be shown (using lemmas of this kind) that the total category of a fibration whose substitution functors are merely stable (so they have poly- rather than rigid adjoints) is, for example, locally finitely presentable iff the base category and fibres are. However one may show that whereas parts of the construction of the dependent product are also possible in this way, its display is not a fibration unless the given fibration is also an op-fibration, i.e. its substitutions have (rigid) left adjoints. Consequently the construction under weaker hypotheses, besides being far more difficult to execute (and this property possessed by finite presentability is not shared by other features) is of no interest in the study of polymorphism.

If we are interested in continuous stable functors we must show that the total category has and the fibration and injections preserve filtered colimits. This result again has nothing to do with stability, and so we shall omit the proof, even though this also is not to be found anywhere in the literature.

Proposition 2.20 Let X ∈ FCCat and Y[−] : X → FCCat^{op} be continuous in the sense that filtered colimits are taken to cofiltered (pseudo)limits. Then ΣX : X .Y[X] has filtered colimits and they are preserved by the fibration and injections. □

It is quite essential that Y[−] be continuous in this result, and so the functor T must also be continuous.

Now let’s consider the complexity of other polycolimits (the spread). The essence of the result already lies in Exercise 1.6.7: if X and each Y[X] are groups then since p : Y → X is a fibration it is (exactly) a surjective group homomorphism, in fact Y ≅ Y[X] : X, a group extension of Y[X] by X (exercise: what is the associated action?).

Definition 2.21 B → A is the groupoid-extension of A by B if this is the fibration corresponding to the indexation B : A → Gpd^{op} where A is a groupoid. (Of course this makes the functor B → A an isotomy, but we intend it to be actually a fibration.) The extension is split if the fibration is split, i.e. B is a functor (not a pseudofunctor).

Exercise 2.22 (⟨x_{i}, y_{i}⟩ : ⟨X_{i}, Y_{i}⟩ → ⟨X, Y ⟩) is a polycolimit candidate in ΣX : X .Y[X] iff (x_{i} : X_{i} → X) is in X and (y_{i} : Y[x_{i}]_{!}(Y_{i}) → Y) is in Y[X]. □

Proposition 2.23 The spread of ΣX : X .Y[X] is the groupoid extension of the spread of X by that of Y. Proof Let Y → X be the display of a dependent sum and ⟨X_{i}, Y_{i}⟩ a diagram in Y of type I. Let A be the groupoid of polycolimit candidates for the diagram X_{i} in X. For a candidate A = (x_{i} : X_{i} → X) ∈ A, let B[A] be the groupoid of polycolimit candidates for the diagram Y[x_{i}]_{!}(Y_{i}) in Y[X], and for an automorphism a : A ≅ A of the candidate, let B[a] = Y[a]^{∗}. Using the exercise we deduce that ΣA : A.B[A] is the groupoid of polycolimits of Y. □

Exercise 2.24 Recall that in a fibration, maps of the form

[figure: ⟨X′, Y[x]^{∗}(Y)⟩; ⟨X, Y ⟩; in; Y; X′; x; X; in; X; P]

are called horizontal; indeed the definition of a fibration is that there is a factorisation system (Definition 1.3.5) of Y-maps into vertical maps (whose images under P are identities) followed by horizontal maps.

(a) Show that horizontal maps are cartesian in the sense that they give rise to a cartesian transformation Y[x]^{∗}ν_{X} → ν_{X}.

(b) The above diagram is called the horizontal lifting of x at ⟨X, Y ⟩. Show that the lifting preserves pullbacks.

(c) A pullback of a horizontal map is horizontal. □

Exercise 2.25 Similarly op-horizontal maps are those of the form ⟨X′, Y′⟩ → ⟨X′, Y[x]_{!}(Y′)⟩. Show that for a rigid bifibration, op-horizontal maps are also cartesian. [Hint: take the verticalhorizontal factorisation of the op-horizontal maps and use the fact that ι : id → Y[x]^{∗}Y[x]_{!} is cartesian.] □

Exercise 2.26 Describe the effect of the functors

Σ_{X} : (X → RC) → RC  and  Σ : (ΣX : RC.(X → RC)) → RC

on morphisms, and show that they are continuous. [Hint: for naturality of Φ[X] ⊣ Θ[X] with respect to x : X′ → X, Y[x]_{!} and Y[x]^{∗} must both commute with each of Φ[X], Θ[X], κ[X] and ι[X], interchanging X ↔ X′ and Y ↔ Y′; cf. Proposition 3.4.1 below.] □

2.4 The Beck Condition

Proposition 2.27 The quantifier Σ commutes with substitution:

(ΣY : Y[X].Z[X, Y])[X := SX′] = ΣY : Y[SX′].Z[SX′, Y]

Proof When we express dependent types with the display Y → X instead of the pseudofunctor Y : X → RC, substitution becomes pullback and sums become composition of displays. This is illustrated in the following diagram:

Σ(X′, Y) : (ΣX′ : X′.Y[SX′]).Z[SX′, Y] ≅

[figure: ΣX′ : X′.ΣY : Y[SX′].Z[SX′, Y]; ΣX′ : X′.Y[SX′]; X′]

[figure: Σ(X, Y) : (ΣX : X .Y[X]).Z[X, Y]; ΣX : X .Y[X]; X; S]

≅ ΣX : X .ΣY : Y[X].Z[X, Y]

where the isomorphisms are “Fubini’s theorem” for calculating iterated dependent sums. The commutation of the quantifier (Σ) with substitution — known as the Beck condition — is the fact that the iterated sum on the top (obtained by substitution and then sum) is indeed the pullback (obtained by sum and then substitution). □

There is a similar condition for dependent products.

There are also interesting examples of indexations in universal algebra where the substitutions have left adjoints, such as the assignment of the category of modules to a ring (induced and restricted modules) and the category of models to a theory (free and underlying algebras), but these do not satisfy the Beck condition. Nor is it satisfied (by the substitution functors and their adjoints) in continuous domain-theoretic models of polymorphism, so one might imagine that there are simply two branches of indexed category theory: one concerned with logic where adjoints to substitution are called quantifiers and satisfy the Beck condition, and the other concerned with model theory where the (left) adjoint is a “free” functor and does not satisfy this condition.

However when we come to stable domain theory, this changes: the base type X has pullbacks, which we now consider algebraically significant (as they are in logic but not model theory), and so they should be preserved in the “domain” of domains RC. Hence it is appropriate to make Y[−] : X → RC stable. This arises quite naturally from Lemma 2.6.2 and when we consider second-order polymorphism, because of the

Proposition 2.28 The stable function space functor [− → −] : RC × RC → RC is stable and continuous. Proof Continuity has already been proved in Theorem 3.1.6, and preservation of wide pullbacks is exactly analogous using Theorem 2.8.2 and Lemma 2.8.3. To deduce stability we have to use the Adjoint Functor Theorem as in section 2.7. □

Lamarche has observed that stability has the result that the Beck condition holds. Since the functor T of Theorem 3.3.2 is essentially the restriction of Y[−] to a slice, and by construction it also preserves the terminal object, T then has a left adjoint.

Proposition 2.29 Let Y[−] : X → RC be stable and suppose the square on the left is a pullback in X:

[figure: X_{1} ×_{X_{0}} X_{2}; π_{1}; X_{1}; X_{2}; π_{2}; x_{2}; X_{0}; x_{1}; Y[X_{1} ×_{X_{0}} X_{2}]; Y[π_{1}]^{∗}; Y[X_{1}]; ⇒^{δ}; Y[X_{2}]; Y[π_{2}]_{!}; Y[x_{2}]^{∗}; Y[X_{0}]; Y[x_{1}]_{!}]

Then the right-hand square commutes up to isomorphism δ. Proof Let Y_{1} ∈ Y[X_{1}] and put Y_{0} = Y[x_{1}]_{!}(Y_{1}); we shall work in the slice of ΣX : X .Y[X] by (X_{0}, Y_{0}), so to simplify notation assume that this is terminal. The object Y_{1} is now given by (X_{1}, 1 →^{y_{1}} T X_{1}), where y_{1} = Y[x_{1}]_{!}(ι_{Y_{1}}). Forming the pullback on the left in Y_{0},

[figure: Y; y_{3}; T (X_{1} × X_{2}); T π_{2}; T X_{2}; 1; y_{1}; T X_{1}; T π_{1}; !_{T X_{1}}; T X_{0}=1; !_{T X_{2}}]

we represent

Y_{1}  by (X_{1}, y_{1})
Y[π_{1}]^{∗}(Y_{1})  by (X_{1} × X_{2}, y_{3})
Y[π_{2}]_{!}(Y[π_{1}]^{∗}(Y_{1})) by (X_{2}, y_{2})  where y_{2} = y_{3} ; T π_{2}
Y_{0} = Y[x_{1}]_{!}(Y_{1})  by (X_{0}, id_{1})

and Y[x_{2}]^{∗}(Y[x_{1}]_{!}(Y_{1})) by (X_{2}, id_{T X_{2}})

so the mediator is δ = y_{2}. However the bottom composite is the identity and the right-hand square is a pullback by the hypothesis that the indexation is stable, so the mediator is an isomorphism. Observe that we used Theorem 3.3.2 to give the representation of Y[f]^{∗} and hence to make the left-hand square a pullback. □

Exercise 2.30 Let Y[−] : X → RC be stable. Show that

(a) Y_{0} ↓ T ≅ G ↓ X_{0} where G ⊣ T;

(b) ν_{X_{0}} : Y[X_{0}]/Y_{0} → Y/⟨X_{0}, Y_{0}⟩ has a second left adjoint given by the unit Y ↦ (Y → T GY);

(c) op-horizontal lifting preserves pullbacks;

(d) the pullback of an op-horizontal map is op-horizontal. □

Exercise 2.31 Show that Σ : (ΣX : RC.[X → RC]) → RC is stable (and continuous). □

2.5 Dependent Products

Dependent products are a generalisation of function-spaces, and we shall use the same technique to calculate their slices. As with dependent sums, this turns out to be much simpler than in the usual case. Dependent products over types (RC) we shall consider separately, since they raise a number of questions of a different kind.

It is not difficult to see that the dependent product ΠX : X .Y[X] must be constructed as the domain Sect(P) of sections of the fibration P : Y = ΣX : X .Y[X] → X. However although this exists irrespective of the properties of P (since

[figure: Sect(P); ⊂; [X → Y]; S ↦ S ; P; S ↦ id; [X → X]]

is an equaliser in SCat) it does not give the dependent product unless P is a fibration whose substitutions are rigid homomorphisms.

Suppose that the base domain is itself dependent upon a variable Z : Z, so that X : Z → RC. The Beck condition requires that the quantifier Π commute with substitution for Z, either of a determinate value Z_{0} ∈ Z or an expression SZ′ with Z′ ∈ Z′. This means that ΠX : X [Z].Y[Z, X] must be functorial in Z, and in fact be a dependent type Z → RC.

Conjecture 2.32 Let S : Y → X be a (stable) functor between (stable) categories. Suppose that S^{∗}, pullback against S in (S)Cat, has a right adjoint. Then S is a (rigid) bifibration.

Theorem 2.33 Let X : Z → RC and Y : (ΣZ : Z.X [Z]) → RC be dependent types. Then ΠX : X [Z].Y[Z, X], given by the domain of sections of P [X] : ΣX : X [Z].Y[Z, X] → X [Z], is also a dependent type. Moreover evaluation is stable and the Beck condition holds. Proof The substitution functors and their adjoints are given by pre- and post-composition with those of X and Y in a standard way. The adjunctions are rigid because the units and counits are obtained by applying stable functors to cartesian transformations. □

Theorem 2.34 The functor Π : (ΣX : RC.[X → RC]) → RC is stable and continuous. Proof From Exercise 3.4.6, the construction of Y = ΣX : X .Y[X] is continuous and stable, and by the same technique so is that of P : Y → X, so we have only to show that P ↦ Sect(P) is stable and continuous. For stability, we use the pushout-pullback coincidence (Theorem 2.8.2) to express the diagram as a wide pullback of rigid comparisons; similarly for continuity we use the limit-colimit coincidence (Theorem 3.1.6) and a cofiltered limit of rigid homomorphisms. Then these limits commute with equalisers. □

These results are standard: what interests us here is how to calculate dependent products, in particular what their slices and polycolimits look like.

Proposition 2.35 Let S : X → Y be a section of the fibration P corresponding to Y : X → RC. Then there is a (stable) functor X → RC such that Sect(P)/S is given by the pseudolimit of a diagram X^{op} → RC^{op} → Cat. Proof Let ϕ : S′ → S in Sect(P) and x : X′ → X in X. Write the vertical-horizontal factorisation of Sx as |Sx|; \underline{\overline{Sx}}. Then in the diagram

[figure: S′X′; |S′x|; Y[x]^{∗}(S′X); \underline{\overline{S′x}}; S′X; SX′; ϕ_{x′}; |Sx|; Y[x]^{∗}(SX); Y[x]^{∗}(ϕ_{X}); \underline{\overline{Sx}}; SX; ϕ_{X}]

the right-hand square is a pullback because the top and bottom are horizontal maps, whilst the rectangle is since ϕ is cartesian, so the left-hand square is also. Hence

[figure: Y[X′]/SX′; \underline{|Sx|^{∗}}; |Sx|_{!}; Y[X′]/Y[x]^{∗}(SX); \underline{Y[x]^{∗}}; Y[x]_{!}; Y[X]/SX; SX′; Y[x]^{∗}(SX); SX]

so X ↦ Y[X]/SX defines a functor X → RC and by the same argument as Proposition 2.6.4 Sect(P)/S is the limit of the diagram of rigid homomorphisms. □

Exercise 2.36 Any stable functor Z : X → RC such that Z[X] has a terminal object may occur in this way. □

There are several ways of finding filtered colimits in the dependent product. There’s brute force. We could also find a “dependent trace” and reproduce the method of section 3.2. The simplest method, however, is to observe that since ⌜id⌝ and postcomposition with P are continuous, the equaliser above creates filtered colimits, which we know to exist and be calculated pointwise in [X → Y].

Proposition 2.37 Sect(P) = ΠX : X .Y[X] has filtered colimits. □

Calculating polycolimits in dependent products (or function-spaces) is an entirely different matter. We shall find later that the existence and uniqueness (connectedness) of polycolimit candidates depends not only on polycolimits in the codomain (as with slices) and those in the domain, but also on the slices of the codomain. Their automorphisms, however, can be bounded by those of the codomain.

Proposition 2.38 Suppose that each Y[X] has filtered colimits which are preserved by Y[x]^{∗} and polycolimits of type I and of type X \X. Then ΠX.X : Y[X] has polycolimits of type I. Proof Let S_{i} → S be a cocone in ΠX.X : Y[X]. For X ∈ X let S_{i}X → F_{0}X → SX be the polycolimit candidate in Y[X]; note that F_{0} is not necessarily stable (unless pullbacks preserve colimits of type I) and the natural transformations S_{i} → F_{0} → S are not cartesian. However for any X_{0} ∈ X, we may define a stable functor on X /X_{0} by

(x : X → X_{0}) ↦ Y[x]^{∗}(F_{0}X_{0} → SX_{0})

and it is easy to show that this is the initial stable functor between S_{i} and S on this slice. (Imagine this functor like a cable-car coming down a mountain.) This is fine if X_{0} is terminal, but otherwise we have to patch together lots of functors like this. Thus we define

(F_{n+1}X → SX) = colim_{x:X→X′} Y[x]^{∗}(F_{n}X′ → SX′)

which gives an increasing sequence of functors between S_{i} and S. (This is where polycolimits of type X \X come in.) Now we have

S_{i}X → F_{n}X → F_{ω}X = colim^{↑}_{n} X → SX

and I claim that F_{ω} is stable and the natural transformation F_{ω} → S is cartesian. This depends solely on preservation of filtered colimits by pullbacks: indeed so long as pullbacks have “rank” in some sense we may perform the same argument by transfinite iteration.

Let x : X → X′; then there is a commutative square with SX → SX′ on the top and F_{n}X → F_{n}X′ on the bottom, so there is a mediator to the pullback, F_{n}X → Y[x]^{∗}F_{n}X′. On the other hand, the latter is a component of the colimit making F_{n+1}X, and so we have a “sandwich”

[figure: ⋯; F_{n}X; Y[x]^{∗}F_{n}X′; F_{n+1}X; ⋯]

Since Y[x]^{∗} preserves filtered colimits, we deduce that Y[x]^{∗}F_{ω}X′ ≅ F_{ω}X as required, i.e. F_{ω} → S is cartesian and hence F_{ω} is stable. It is easy to check that this is the required polycolimit candidate. □

Corollary 2.39 Polycolimits (where they exist) are computed pointwise iff pullback functors preserve colimits in slices. □

The explicit description of polycolimits enables us to calculate their automorphism groups.

Proposition 2.40 The automorphism group of a polycolimit candidate in ΠX : X .Y[X] is obtained from automorphism groups of polycolimits in Y by a process of forming products, subgroups and extensions.

Proof Let ϕ : F_{ω} → F_{ω} be a natural automorphism which commutes with the cocone S_{i} → F_{ω}, and let X ∈ X. Since S_{i}X → F_{0}X → F_{ω}X is a polycolimit candidate, there is a unique map ϕ_{0}X : F_{0}X → F_{0}X which commutes with the diagram involving ϕX, and ϕ_{0} is a natural automorphism of F_{0}. Now we construct ϕ_{n}X by mimicking the construction of F_{n}X: for x : X → X′ we have a cocone Y[x]^{∗}ϕ_{n}X′ : Y[x]^{∗}F_{n}X′ → Y[x]^{∗}F_{n}X′ and hence a unique mediator ϕ_{n+1}X : F_{n+1}X → F_{n+1}X below ϕX. Then also Φ_{n+1} is a natural automorphism of F_{n+1}.

Now the construction ϕ ↦ ϕ_{0}X is a group homomorphism from the required automorphism group (of S_{i} → F_{ω}) to that of the pointwise colimit S_{i}X → F_{0}X. Automorphisms of the functor F_{0} must be natural, which we may express as a subgroup of the product of the automorphism groups at each component. For the higher stages a similar argument applies: with ϕ_{n} fixed, ϕ_{n+1}X belongs to the automorphism group of the polycolimit of type X \X. Allowing the lower candidates to vary, we obtain an extension group with the component for ϕ_{n+1}X at the bottom and that for ϕ_{0} at the top; again naturality of ϕ_{n+1} may be expressed as a subgroup of a product.

Finally ϕ is determined by the sequence (ϕ_{n}) since we have assumed the existence of filtered colimits (not “poly”), and so ϕ belongs to the cofiltered limit of the groups for ϕ_{n} (if the filtered colimit were poly, there would simply be yet another factor below the limit). □

Corollary 2.41 If each Y[X] has equalisers then so does ΠX : X .Y[X]. □

Lamarche has observed that we cannot make stable functors preserve equalisers if we want cartesian closure, but his semigranular categories and aggregates have them. This result explains why this is possible, although our proof, unlike his (implicitly), does not depend on distributivity.

2.6 Categories of Stable Categories

Hitherto we have set out the theory of stable categories in the most general form possible, whereas other authors have studied more restricted versions. The remainder of this paper will be devoted to showing how their results can be recovered by working “top-down” and to a semi-systematic survey of the possible subcategories of stable categories which admit dependent sums and products (including function-spaces). We find that although the restrictions which previous authors have placed on their stable domains are not necessary for cartesian closure (and in some cases proved a substantial burden to them) they are of interest in themselves, and so we shall study their axioms one by one, and hence recover their results by taking suitable combinations of axioms.

As we have seen, the characteristic feature of stable domain theory is really pullbacks. Write Pbk for the 2-category of categories with pullbacks, functors which preserve them and cartesian transformations.

Theorem 2.42 The abstract adjunctions in Pbk are exactly rigid adjunctions, and the category Pbk^{rc} of categories with pullbacks and rigid comparisons between them has pullbacks. Pbk is cartesian closed and admits dependent sums and products. Proof Left adjoints are isotomies by Lemma 2.5.1. Pbk has binary products from Exercise 1.8.2. We went a long way round to find stable function-spaces, but it is an easy exercise to show that we may calculate pullbacks in function-spaces and RC pointwise. For dependent sums and products, Propositions 3.3.2 and 3.5.3 still apply. □

Everything else is built up from here. Write Pbk_{λ}^{κ} for the 2-category of locally small categories which

(i) have wide pullbacks of size λ

(ii) and filtered colimits of size κ (which must be preserved by pullbacks),

functors preserving them and cartesian transformations. Similarly write SCat^{κ} for the 2-category of locally small categories which

(i′) have wide pullbacks, a set of coseparators and are well-powered

(ii) and have filtered colimits of size κ (which must be preserved by pullbacks), functors preserving them and cartesian transformations.

Theorem 2.43 Pbk_{λ}^{κ} and SCat^{κ} admit dependent sums and products, which are created by the forgetful functors to Pbk. Moreover the categories of domains and rigid comparisons have appropriate wide pullbacks and filtered colimits. □

This is the first aspect of flavour of stable categories, which we call (algebraic) structure. Clearly there’s nothing very exciting to be said about this, and we shall concentrate on the most restrictive case: continuous stability. This classification really applies to stable functors, since we may use spin (see below) to say that equalisers exist, whereas we may not require them to be preserved.

The second aspect of flavour is size: we may seek to restrict our stable categories to be such that there is, for instance, a countable set of objects from which others may be obtained by countable filtered colimits. Restrictions like this are popular in Computer Science for reasons of effectivity, but again nothing very much needs to be said about them, except that they may be inconsistent with the behaviour of spread, essentially because of a result adapted from Smyth’s theorem about maximal cartesian closed categories of countably-based algebraic posets and continuous functions. Thus if we want to restrict size or spread by large cardinals we have to use < ℶ_{ω} rather than < ℵ_{1}.

Exercise 2.44 Let X be an algebraic stable poset with some pair of finitely presentable objects which have κ ≥ 2 multijoins. Then [X → X] has a pair of finitely presentable objects with at least 2^{κ} multijoins.

Besides the ubiquity of pullbacks in the theory we have forever been discussing slices, and we have shown that traces, function-spaces, RC, dependent sums and dependent products have slices of the same kind as the given domains.

Definition 2.45 A class of slices is a class of complete categories closed under equivalence and the following operations:

(i) Singleton, cartesian product and slices.

(ii) Arrow categories Y ↓ T, where T : X → Y is a homomorphism.

(iii) Limits of diagrams whose arrows are pullback functors X^{∗} : X → X /X.

We shall split the problem of the complexity of polycolimits into two parts: the number of components (spread) and their automorphism groups (spin). The second problem is more tractable than the first.

Definition 2.46 A class of spins is a class of groups closed under isomorphism and the following operations:

(i) Singleton (trivial group).

(ii) Extensions.

(iii) Products and subgroups (alternatively arbitrary diagrams of group homomorphisms).

Theorem 2.47 Let S be a class of slices and G be a class of spins. Write SCat[S, G] for the full sub-2-category of stable categories whose slices belong to S and the automorphism groups of whose polycolimit candidates belong to G. Then SCat[S, G] is cartesian closed, and indeed admits dependent sums, and dependent products indexed by arbitrary stable categories. Proof As regards slices, condition (i) provides finite products and (ii) gives dependent sums; we need (iii) for cofiltered diagrams to construct filtered colimits in function-spaces and for general diagrams to construct dependent products. For spins, we used limits and extensions. □

We shall consider separately each of the restrictions which other authors have placed on their stable domains, showing that they may be expressed in terms of slices, spin and spread and why they arise naturally. Cartesian closure of their categories of domains considered will follow from the above results and such others as we can prove about preservation of spread by function-spaces and dependent products.

Exercise 2.48 Let X be a stable category and I a diagram-type (directed graph or category). Write I + 1 for the type obtained by freely adjoining a terminal object, and

Δ : X^{I+1} → X^{I}

for the forgetful functor between the categories of diagrams of these types in X. Then the diagonal universals for Δ are exactly the polycolimit candidates and

Spec_{Δ}(X_{i}) ∈ Gpd

is the groupoid of polycolimits of the diagram (X_{i}). □

Exercise 2.49 Let S : X → Y be stable with trace T and (T_{i}) be a diagram of type I in T . Show that polycolimit candidates T for this diagram are given by pairs (X, Y, u) where X and Y are polycolimit candidates in X and in Y which are compatible in the sense that there is a (unique) morphism u making the diagram commute. By Lemma 1.5.8 this is diagonally universal. Show also that an automorphism of the candidate T is a pair ⟨x, y⟩ of compatible automorphisms, and hence that Aut_{T} (T_{i} → T) is the intersection of Aut_{T} (T) and Aut_{X} (X_{i} → X) × Aut_{Y} (Y_{i} → Y) in Aut_{X} (X) × Aut_{Y} (Y). □

The following two results relate binary products and equalisers to spread (connectedness of polycolimits) and spin (discreteness). It is immediate from the adjoint functor theorem that a stable category has a terminal object iff it has colimits.

Exercise 2.50 A stable category has equalisers iff all polycolimits are discrete (multicolimits in Diers’ terminology). This happens if (but not only if) all polycoequalisers are non-empty, or if the category has (pullbacks and) binary products. □

Exercise 2.51 A stable category X has binary products iff every diagram in X which has a cocone has a colimit (not poly). In this case − × − : X × X → X is a stable functor, continuous iff X is pullback-continuous, and π_{0} : − × X → id is cartesian.

Exercise 2.52 If all multijoins in a stable poset are non-empty then it has a top element. Find an example of a stable category in which all polycoproducts are non-empty but some of them are disconnected. [Hint: fields.]

What about the spread of RC? We mentioned something analogous to disjoint coproducts (disjoint polypushouts) in Exercise 3.7.12. The problem with RC is that its spread tends to far exceed that of its objects:

Example 2.53 Consider X = Y = 2 ∈ RC. A polycoproduct candidate for X and Y is a domain Z consisting of three points in a “V”, bounded by an arbitrary groupoid. Hence the polycoproduct is a large groupoid. □

2.7 Posets and Monomorphisms

In every account of stable domain theory (except [G85], which in any case did not define a cartesian closed category) the domains have satisfied the following:

Exercise 2.54 The following are equivalent for a category X:

(α) Every morphism x : X′ → X of X is mono.

(β) Every slice X /X is a preorder.

(γ) If the parallel pair f, g : X′ ⇉ X has an non-empty polycoequaliser then f = g. □

Proposition 2.55 Complete lattices form a class of slices, and hence stable categories in which all maps are mono form a relatively cartesian closed category. □

This condition is found in the mathematical examples of Diers as well: the categories of fields and linear orders have all maps mono, although they are not preorders. This phenomenon is partly explained by Exercise 1.3.5 but mainly by the

Exercise 2.56 Let T be a first-order theory. Every homomorphism of models of T is mono iff there is a positive formula ϕ(x, y) [i.e. one involving ∧, ∨, ∃ and ∀ but not ¬ or ⇒] such that T ⊢ ∀x, y.ϕ(x, y) ⟺ x ≠ y. □

Examples 2.57

(a) For fields, x ≠ y ⟺ ∃z.z(x − y) = 1.

(b) For linear orders, x ≠ y ⟺ x < y ∨ y < x.

(c) For (tokens of) coherence spaces, x ≠ y ⟺ x ⌣ y ∨ x ⌢ y, where ⌣ and ⌢ denote strict (in)coherence. In this case the model homomorphisms are rigid embeddings. □

We are going to give a number of examples to show that the various axioms restricting stable domains may be expressed in terms of slices and spread. Some of them may appear to be a long-winded way of saying something very simple! Notice that we can deduce the existence of equalisers (and hence that polycolimits are discrete) from (ii) alone, and the existence of binary products (meets) from (iii) alone.

Example 2.58 A stable category X is a preorder iff

(i) every slice is a preorder and

(ii) every parallel pair has at least (exactly) one polycoequaliser candidate.

It is boundedly complete iff additionally

(iii) every pair of objects has at most one polycoproduct candidate. □

Proposition 2.59 Stable posets form a relatively cartesian closed category. □

Conjecture 2.60 Suppose that the polycoequaliser of any parallel pair in [X → X] is nonempty; then X is a preorder. Hence stable posets are the largest cartesian closed category of stable categories with coequalisers.

Example 2.61 A boundedly complete poset is

(i) a qualitative domain iff every slice is a complete atomic Boolean algebra and

(ii) a coherence space iff additionally the polycoproduct of a set of objects is the wide pullback of the polycoproducts of the subsets containing at most two objects. □

The last part shows that spread may or may not be determined by simple diagrams (polyinitial families, polycoequalisers and binary polycoproducts). The study of this phenomenon suggests the use of descent or homology. We do not quite have the tools to assert that qualitative and coherence domains form a cartesian closed category, but

Exercise 2.62 Complete atomic Boolean algebras form a class of slices, and hence Lamarche’s semigranular categories (which are stable categories with Boolean slices) form a relatively cartesian closed category. □

2.8 Algebraic Stable Categories

The theme of Diers’ work is the generalisation of features of the study of algebraic theories expressed in terms of functors with left adjoints to disjunctive theories using stable functors. The most famous result about the use of category theory to describe algebraic theories is the Gabriel-Ulmer duality between LFP, whose objects are categories of algebras, and Lex, whose objects are algebraic theories. More precisely, LFP is the 2-category of locally finitely presentable categories, homomorphisms and natural transformations, and Lex consists of categories with finite limits and functors preserving them. Diers’ result extended the class of objects of these 2-categories by admitting (discretely) stable categories with LFP-slices on the one hand and categories with multipullbacks on the other. However he did not generalise the morphisms, and he also use natural rather than cartesian transformations.

Definition 2.63 A category is locally finitely poly-presentable if it has wide pullbacks, filtered colimits and a set of (isomorphism classes of) finitely presentable objects, and every object may be expressed as a filtered colimit of finitely presentable objects. The category is locally finitely multipresentable if it also has equalisers. Write LFPP (LFMP) for the 2-category of locally finitely poly- (multi-)presentable categories, continuous stable functors and cartesian transformations.

Definition 2.64

(a) A plex-category is a small category with finite poly-limits (its opposite has finite polycolimits); it is called a mlex-category if the poly-limits are discrete.

(b) A homomorphism of plex-categories C : 𝕐 → 𝕏 is a functor which preserves poly-limits.

(c) A trace from a plex-category 𝕐 to another 𝕏 is a pair of functors C : 𝕋 → 𝕏 and F : 𝕋 → 𝕐 such that C preserves poly-limits and F is an equivalence on each coslice. The trace is discrete if F preserves coequalisers.

(d) A diagonal between traces Φ : 𝕋′ → 𝕋 is an isomorphism class of functors which preserve poly-limits and make the C- and F -triangles commute.

Write PLex (MLex) for the 2-category of plex- (mlex-)categories, traces and diagonals.

Theorem 2.65 LFPP and PLex are dual in the sense that there is a 2-equivalence which is contravariant on 1-cells and covariant on 2-cells. LFMP and MLex are also dual, and both dualities restrict to discrete traces and to homomorphisms. Proof If X is a locally finitely poly-presentable category, put 𝕏 = (X_{fp})^{op}; conversely put X = Ind(𝕏^{op}). Lemma 1.5.8 and Exercise 1.9.9 show that this translation also applies to the trace, whilst Propositions 1.7.3 and 2.1.4 relate diagonals and cartesian transformations. The results easily restrict. □

Our interest is in relatively cartesian closed categories:

Proposition 2.66 LFP is a class of slices. Proof

(i) Singleton, cartesian product and slices: easy.

(ii) Arrow categories Y ↓T, where T is continuous, not necessarily a homomorphism. The typical finitely presentable object is y : Y → T X where X ∈ X_{fp} and Y ∈ Y_{fp}. It is easy to show that these approximate.

(iii_{↓}) Cofiltered limits of (not necessarily rigid) homomorphisms, or equivalently filtered colimits of comparisons. Comparisons preserve finite presentability, and so the typical finitely presentable object of bilim X_{i} is Φ_{i}(X_{i}) where X_{i} ∈ X_{i}_{fp}. These approximate images, whilst images approximate all objects.

(iii_{fin}) The limiting cone over a diagram of homomorphisms between complete LFP-categories consists of homomorphisms. Typical finitely presentable objects of the limit are finite colimits of images of finitely presentables. □

Corollary 2.67 The following full sub-2-categories of SCat are relatively cartesian closed:

(a) locally finitely poly-presentable categories,

(b) locally finitely multi-presentable categories,

(c) categories with filtered colimits whose slices are algebraic lattices and

(d) the same, but also having equalisers.

(e) algebraic stable posets. □

Exercise 2.68 A stable category is profinite (i.e. it can be expressed as a limit of a diagram of finite stable categories and stable functors) iff its slices are algebraic lattices. □

Exercise 2.69 Continuous categories in the sense of [Johnstone & Joyal 1982] form a class of slices, and hence the continuous analogue of Corollary 3.8.5 holds (continuous stable posets were studied in [T88]). □

Bifinite stable categories (those which can be expressed as cofiltered limits of finite domains and rigid homomorphisms) are much more special, because rigid comparisons, being isotomies, preserve more than just finite presentability.

Definition 2.70 X ∈ X is called strongly finite if X /X is a finite category. X is strongly presentable if every object can be expressed as a filtered colimit of strongly finite objects.

Exercise 2.71

(a) Show that rigid comparisons create strong finiteness, and strongly finite objects of pullbackcontinuous categories are finitely presentable.

(b) Strongly presentable categories form a class of slices contained in the class of algebraic lattices.

(c) Suppose that the polycoproduct of any pair of strongly finite objects is finite; then any finite set of strongly finite objects is contained in a rigidly embedded finite subcategory.

(d) Hence show that a stable category is bifinite iff it is strongly presentable and the polycoproduct of any pair of strongly finite objects is finite. □

Exercise 2.72 Show that the following are bifinite stable categories:

(a) algebraic number fields (i.e. algebraic field extensions of ℚ) and field homomorphisms;

(b) LOrd (linear orders and strict monotone functions);

(c) dI-domains and rigid embeddings. □

Jung [1988] has shown how to extend the polycoproduct condition to arbitrary objects by imposing the Scott or Lawson topologies on the domain, so that finite becomes compact, but this is outside the scope of this paper. Although we cannot use spread to prove cartesian closure, the following result follows easily from Theorem 3.1.6, Exercise 3.4.6 and Proposition 3.5.3 (Coquand mentions bifinite stable posets).

Proposition 2.73 The 2-category of bifinite stable categories is relatively cartesian closed. □

Conjecture 2.74 The category of bifinite stable posets admits dependent products indexed by its category of rigid embeddings, and hence models System F. The interest of such a model is that Πα.α → α → α would have only the points ⊥, t and f, and not “intersection” as in the coherence space model.

Question 2.75 What about finitely presentable categories as slices?

The most interesting classes of slices are the subclasses of the class of locally cartesian closed categories, which we shall discuss after we have shown why this condition has a serious effect on spread. Let us just conclude this subsection with the trivial case.

Exercise 2.76 Every slice of X /X is trivial (equivalent to the singleton category) iff every morphism of X is invertible. Trivial categories form a class of slices, and hence Gpd is relatively cartesian closed. Trivial groups also form a class of spins, and hence Set is relatively cartesian closed. In Set and Gpd every morphism is a display, and so these categories are locally cartesian closed. □

2.9 Distributivity

By far the most interesting restriction we may place on stable categories is distributivity. All accounts of stable domain theory except [T88] have assumed this because it makes the computation of function-spaces substantially easier. However the importance of this condition lies in the possibility of topological representations, of which there is some hint in [CGW], and in the application to linear logic.

We cannot define a “class of spreads” and prove a simple analogue of Theorem 3.6.5. In particular we cannot make the spread trivial (i.e. all colimits exist) without making the category of domains trivial too. The problem is that whereas slices and spin are essentially independent of each other and of spread, the spread of function-spaces is critically affected by the slices and spin of the domains.

Proposition 2.77 Suppose X and [X → X] are boundedly complete stable posets. Then meets distribute over joins (where they exist) in X. Proof It is well-known that any non-distributive lattice contains one or other of the following as sub-lattices:

[figure: a ∨ b; A; b; a; a ∧ b; ⊥; a ∨ b; a; b; c; a ∧ b; ⊥]

(In this context, a “lattice” has bottom but not top.) Let j : Y ⊂ X be such a sublattice, so that p : X → Y with p and j stable, and j ⊣ p. Define the three endo-functions of Y:

â : y ↦ a ∧ y  b̂: y ↦ b ∧ y  h : y ↦ (a ∧ y) ∨ (b ∧ y)

and verify case-wise that they are stable and h is a multijoin of â and b̂ in [Y → Y]. Then p; h; j is a multijoin of p; â; j and p; b̂; j in [X → X], and p; j also lies above them (in the Berry order). By the hypothesis that [X → X] is boundedly complete, the multijoin should be a join, but if we test cartesianness of p; h; j ≤ p; j at y ≤ a ∨ b with y = A or y = c we obtain the pullback

\begin{matrix}(a ∧ (a ∨ b)) ∨ (b ∧ (a ∨ b)) & = = = = = & a ∨ b \\ (a ∧ y) ∨ (b ∧ y) & & \overline{} & (a ∨ b) ∧ y & \end{matrix}

from which distributivity follows. (This argument appears to be a proof by contradiction, but with slight re-wording it can be made constructive.) □

Conjecture 2.78 If [X → X] has binary products then in X pullbacks preserve colimits.

We have already required pullbacks to preserve filtered colimits as a necessary part of continuity of stable functors, and now we are asking that they also preserve finite colimits. It is because previous authors have defined stable categories in terms of polycolimits that they have needed distributivity to prove cartesian closure.

Definition 2.79 A category X is locally cartesian closed if pullback functors x^{∗} exist and have right adjoints (cf. Lemma 2.2.4). Notice that we have not required there to be a terminal object. We say X is an lccc.

Proposition 2.80 The following are equivalent for X:

(α) pullback functors have right adjoints;

(β) every slice is cartesian closed;

(γ) X is relatively cartesian closed with respect to all maps;

and if X has wide pullbacks and a set of coseparators (...),

(δ) pullbacks preserve colimits;

(ϵ) pullbacks preserve the initial object (it is strict), coproducts (the pullback of X → X+Y ← Y against Z → X + Y is X′ → X′ + Y′ = Z ← Y′), coequalisers (similar) and filtered colimits (pullback-continuous).

Proof Standard exercise. □

Lemma 2.81 In an LCCC, pullbacks preserve exponentials. Proof This is the Beck condition for Π; it states the commutativity of a square whose maps are the right adjoints of those in the Beck condition for Σ (exercise). □

Lemma 2.82 Let S_{1}, S_{2} : X ⇉ Y be stable functors between locally cartesian closed categories. Suppose that the (pointwise) coproduct S_{1}X + S_{2}X exists in Y for each X ∈ X. Then this defines a stable functor S_{1} + S_{2} : X → Y. Proof Let ν_{i}X : S_{i}X → S_{1}X + S_{2}X be the inclusion; this is not a cartesian transformation without additional hypotheses (which we shall investigate in the next subsection). Given w : Y → S_{1}X + S_{2}X in Y, form its pullback (ν_{i}X)^{∗}w : Y_{i} → SX_{i} and factorise this as (ν_{i}X)^{∗}w = u_{i} ; S_{i}f_{i} with u_{i} : Y_{i} → S_{i}X_{i} diagonally universal and f_{i} : X_{i} → X. Now, using preservation of coproducts by pullbacks, it is an exercise to show that X_{1} + X_{2} is the required intermediate object. □

Theorem 2.83 LCCCs with 1 form a class of slices. Hence

(a) LCCCs,

(b) LCCCs with equalisers and

(c) LCCCs with products

form relatively cartesian closed categories. Proof Either exponentials or pullbacks and colimits may be constructed componentwise; hence [a] and [b] follow immediately from Theorem 3.6.5. For [c], having binary products is equivalent to having at most one polycolimit for any diagram. By Corollary 3.5.8, any polycolimit candidate for a diagram in the function-space is computed pointwise and so is unique. □

The relatively cartesian closed categories of stable domains which we have as a result of this are too numerous to mention individually, so we shall just list the ones which others have considered.

Corollary 2.84 The following classes of stable domains form relatively cartesian closed categories:

(a) boundedly complete, strongly presentable and distributive: dI-domains, Berry [1978] and Coquand, Gunter & Winskel [1986];

(b) boundedly complete and Boolean: qualitative domains, Girard [1984];

(c) boundedly complete and Boolean, where any pairwise bounded set has a join; coherence spaces, Girard [1986] and Girard, Lafont & Taylor [1988];

(d) mono, algebraic and distributive: stable categories of embeddings, Coquand [1988];

(e) mono, equalisers, strongly presentable and distributive: aggregates, Lamarche [1988];

(f) Boolean and equalisers: semigranular categories, Lamarche [1988].

In cases (a–c) we may understand non-empty if we please. Proof Obviously Boolean algebras are strongly presentable distributive posets. That the binary condition (c) is reproduced in function-spaces follows from the form of condition 3.7.6(ii). □

[Any distributive domain has a reflection into any class of slices.]

Our reason for considering distributivity was that it was necessary for bounded completeness, whilst the fact that the domain may be taken to be a subset of a frame suggests topological representations of which [CGW] gives some hint. It also appears (although I do not know why) that distributivity is needed to interpret linear logic. Domains of this kind appear to be worthy of specify study, and Girard’s qualitative/quantitative terminology seems too good to waste:

Definition 2.85 A qualitative domain is a boundedly complete poset with directed joins and bottom whose slices are frames.

Theorem 2.86 Qualitative domains form a relatively cartesian closed category. Proof Special case of Theorem 3.9.7 where all maps are mono. □

Theorem 2.87 Qualitative domains admit second-order dependent types, i.e. they model Girard-Reynolds polymorphism. Proof The category of qualitative domains and rigid comparisons has small spread, so we are permitted to form dependent products over it. The slices of such a dependent product are frames, so it only remains to verify that it is boundedly complete; but the argument of Theorem 3.9.7 still applies. □

These dependent products satisfy Moggi’s uniformity property, but the values of polymorphic types are likely to be much the same as in coherence spaces and dI-domains.

2.10 Quantitative Domains

Qualitative domains exploit the best we can do in demanding existence of coequaliers and uniqueness of coproducts; as we shall see, we cannot have both, so we shall now look for the reverse. The following is a special case of Conjecture 3.9.2:

Lemma 2.88 If [X → X] is connected then X (is empty or) has a strict initial object. Proof Clearly X is connected, so let I be the unique polyinitial candidate. By hypothesis id, ⌜I⌝ : X → X are connected by some zig-zag, which using pullbacks we may reduce to

[figure: id; κ; M; ϕ; ⌜I⌝]

Put Z = MI ∈ X and p = κ_{I} : Z → I. Since I is a polyinitial candidate, there is a (unique) j : I → Z with j ; p = id, so p is split epi. For any X ∈ X we have some ξ : I → X and then the left-hand square is a pullback, making Mξ an isomorphism:

[figure: Z; ϕ_{I}; I; MX; Mξ; ϕ_{X}; I; id; MZ; κ_{Z}; Z; Z; ≅ Mp; p = κ_{I}; I; p]

It follows that M takes every morphism to an isomorphism, and in particular Mp is one. Then the right-hand square shows that p is mono and hence iso, so ϕ : M ≅ ⌜I⌝. The argument also shows that any given p′ : Z′ → I is iso; in particular so are g, (ϕ^{−1} ; κ)_{I} : I → I. But suppose we have g : I ≅ I; then naturality of ϕ^{−1} ; κ with respect to g shows that g = id, so I is strict initial. □

The following property of slices is essentially the difference between Girard’s qualitative and quantitative domains: in a poset, binary coproducts (joins) are idempotent, i.e. X ∨ X ≅ X, whereas in Set or any topos they are disjoint, i.e. the pullback of the inclusions is the (strict) initial object. This is the reason why [2 → 2] is not 3 but a V-shaped domain.

Lemma 2.89 Suppose that the polycoproduct of any pair of objects of [X → X] is nonempty. Then X has disjoint polycoproducts. Proof Clearly [X → X] is connected, and so by Proposition 3.9.1 X has a strict initial object 0. Let X, Y ∈ X and consider id, ⌜X⌝ : X → X. By hypothesis these have a polycoproduct candidate S, with ϕ : ⌜X⌝ → S and ψ : id → S, where (ϕ and) ψ are cartesian. Then the square is a pullback:

0  \overline{ψ_{0} = ?_{S0}} S0

[figure: ?_{X}; ϕ_{0}]

X

[figure: ϕ_{Y}]

[figure: Y; ?_{Y}; ψ_{Y}; SY; S?_{Y}]

[figure: ν_{2}; m]

X + Y \begin{aligned}ν_{1} \\ &  \end{aligned}

where m : X + Y → SY is the coproduct in X /SY with inclusions ν_{1} and ν_{2}. It is easy to see that the parallelogram from 0 to X + Y is also a pullback. □

A categorical logician might imagine that the analogous result for polycoequalisers is that equivalence relations are effective. Unfortunately by conjecture 3.7.6 the result is more drastic.

Proposition 2.90 Suppose that [X → X] has a terminal object. Then X is degenerate, i.e. equivalent to either 0 or 1. Proof Suppose that X is connected. The polycoproduct of any pair of objects of [X → X] is nonempty, and so X has disjoint polycoproducts and a strict initial object 0. X also has colimits (since diagrams of constant functors have colimits) and hence a terminal object 1, binary products and equalisers.

Consider the stable functor SX = X^{2} and the object 2 = 1 + 1; as well as the identity, these carry “switch” automorphisms s : 2 → 2 and t : S → S, giving a parallel pair

⟨S, 2⟩ [figure: ⟨t, s⟩; ⟨id, id⟩] ⟨S, 2⟩

in [X → X] × X. The latter has a terminal object, whence any stable functor out of it preserves equalisers. Clearly applying ev to this pair makes them equal, and so the equaliser of the images is 2^{2}.

Since ev preserves equalisers jointly, it must do so separately (although the converse is not true), and in particular equalisers of stable functors are calculated pointwise. The coproduct 2 = 1 + 1 is disjoint, so the equaliser of the above pair is ⟨⌜0⌝, 0⟩, which becomes 0 on application of ev. Hence 2^{2} ≅ 0 and X is degenerate. □

Corollary 2.91 In any non-trivial cartesian closed category of stable categories, there are objects for which some polycoproduct or some polycoequaliser is empty. □

Question 2.92 What feature, if any, of [X → X] would force X to have effective equivalence relations in slices? Is there a connection between this and when rigid adjunctions are monadic?

The following terminology arises from Giraud’s theorem that a category is a Grothendieck topos iff it is of this form.

Definition 2.93 A Giraud topos is a locally small category which has set-indexed colimits and a set of generators and satisfies

(i) it is locally cartesian closed;

(ii) coproducts are disjoint;

(iii) equivalence relations are effective, i.e. if a subobject R ⊂ X × X is reflexive, symmetric and transitive then it is the kernel of its coequaliser;

(iv) epimorphisms are regular, i.e. the coequaliser of their kernels.

Lemma 2.94 In a topos, pullback functors preserve the subobject classifier Ω. □

Theorem 2.95 Giraud toposes form a class of slices, and hence stable domains whose slices are toposes form a relatively cartesian closed category. Proof Either we may compute Ω componentwise, or else we compute pullbacks and colimits componentwise and verify (ii–iv) in the same way as (i). □

As with distributivity, our aim was to optimise spread, and again it seems appropriate to modify Girard’s terminology. Here also we should look for topological representations, since any quantitative domain is a full subcategory of a topos.

Definition 2.96 A quantitative domain is a category with filtered colimits, a strict initial object, binary products and binary coproducts, whose slices are toposes.

Lemma 2.97 Let S_{1} and S_{2} be stable functors between quanitative domains. Then ν_{1}X : S_{1}X → S_{1}X + S_{2}X is cartesian. Proof Suppose f : Y → S_{1}X′ + S_{2}X′ and g : Y → S_{1}X make the square commute. Let Y = Y_{1} + Y_{2}, where Y_{i} = f ∗ (ν_{i}X′). Then Y_{2} → 0 since the coproduct S_{1}X + S_{2}X is disjoint, and so Y_{2} ≅ 0 and Y ≅ Y_{1} → S_{1}X′. □

Theorem 2.98 Quantitative domains form a relatively cartesian closed category. Proof (Sketch) The strict initial object of [X → X] is ⌜0⌝, and we have shown that coproducts are constructed pointwise. Coequalisers, where they exist, are also computed pointwise and hence are unique; it follows that any colimit diagram with a cocone has a colimit, which is equivalent to possessing binary products. The results are easily extended to dependent (sums and) products. □

Theorem 2.99 The category of quantitative domains and rigid comparisons is a quantitative domain, i.e. a type of types. Proof The strict initial object is the singleton, and coproducts are given by products quantitative domains quâ categories. Binary product is a “tensor product” construction which for toposes is topological product. □

Conjecture 2.100 This is the largest category of stable domains with a type of types. □ [The following result belongs in section 2.1; necessity was remarked by Lamarche.]

Lemma 2.101 Φ is full (as well as faithful) iff ϕ is mono. Proof

[⇒] Suppose w_{1} ; ϕ_{X} = w_{2} ; ϕ_{X}, in which we may put w_{1} = u′_{1} ; S′x_{1} and w_{2} = u′_{2} ; S′x_{2}. Then

u_{1} ; Sx_{1} = u′_{1} ; ϕ_{X′_{1}} ; Sx_{1} = u′_{1} ; S′x_{1} ; ϕ_{X} = u′_{2} ; S′x_{2} ; ϕ_{X} = u′_{2} ; ϕ_{X′_{2}} ; Sx_{2} = u_{2} ; Sx_{2}

by naturality of ϕ, and so by diagonal universality of u_{1} and u_{2} there is a unique h : X′_{1} ≅ X′_{2} such that

u_{2} = u_{1} ; Sh  and  x_{2} = h^{−1} ; x_{1}

The first equation makes ⟨h, id⟩ : Φ⟨X_{1}, Y, u′_{1}⟩ → Φ⟨X_{2}, Y, u′_{2}⟩ a morphism, and so by hypothesis ⟨h, id⟩ : ⟨X_{1}, Y, u′_{1}⟩ → ⟨X_{2}, Y, u′_{2}⟩ is also, i.e. u′_{2} = u′_{1} ; S′h. But then

w_{2} = u′_{2} ; S′x_{2} = u′_{1} ; S′h; S′(h^{−1} ; x_{1}) = u′_{1} ; S′x_{1} = w_{1}

as required.

[⇐] Let ⟨x, y⟩ : Φ⟨X_{1}, Y, u′_{1}⟩ → Φ⟨X_{2}, Y, u′_{2}⟩ be a morphism. Then the square on the left commutes and that on the right is a pullback:

[figure: Y_{1}; u_{1}; SX_{1}; Y_{2}; y ; u′_{2}; ϕ_{X_{2}}; SX_{2}; Sx; S′X_{1}; ϕ_{X_{1}}; SX_{1}; S′X_{2}; S′x; ϕ_{X_{2}}; SX_{2}; Sx]

Let v : Y_{1} → S′X_{1} be the mediator. But then v ; ϕ_{X_{1}} = u_{1} = u′_{1} ; ϕ_{X_{1}} and ϕ_{X_{1}} is mono, so v = u′_{1}. Hence also u′_{1} ; S′x = y ; u′_{2}, i.e. ⟨x, y⟩ : ⟨X_{1}, Y, u′_{1}⟩ → ⟨X_{2}, Y, u′_{2}⟩ is a morphism. □