BOUNDEDNESS AND COMPLETE DISTRIBUTIVITY

R. ROSEBRUGH AND R.J. WOOD

ABSTRACT. We extend the concept of constructive complete distributivity so as to make it applicable to ordered sets admitting merely bounded suprema. The KZ-doctrine for bounded suprema is of some independent interest and a few results about it are given. The 2-category of ordered sets admitting bounded suprema over which inhabited (classically non-empty) infima distribute is shown to be bi-equivalent to a 2-category defined in terms of idempotent relations. As a corollary we obtain a simple construction of the non-negative reals.

1. Introduction

1.1. The main theorem of [RW1] exhibited a bi-equivalence between the 2-category of (constructively) completely distributive lattices and sup-preserving arrows, and the idempotent splitting completion of the 2-category of relations — relative to any base topos. Somewhat in passing in [RW1], it was pointed out that this bi-equivalence provides a simple construction of the closed unit interval ([0, 1], ≤), namely as the ordered set of down-sets for the idempotent relation given by strict inequality on the rational closed unit interval. Recall that a relation ≺: X \overline{}X is an idempotent if and only if it is transitive and interpolative, where the latter means that x ≺ y implies (∃z)(x ≺ z ≺ y). Then a down-set for (X, ≺) is a subset S of X for which x ∈ S if and only if (∃y)(x ≺ y ∈ S). This construction for [0, 1], manifestly a variation on Dedekind’s using cuts, takes on, in the context of [RW1], a functorial character and can be carried out in any topos with a natural numbers object. It is natural to wonder whether the theory can be modified so as to obtain a construction for [0, 1), equivalently the non-negative reals, without presuming the relationship between [0, 1] and [0, 1) that exists in classical Boolean set theory. In this paper we answer that question affirmatively but in the process investigate a monad on ordered sets that seems to be of considerable interest in its own right.

1.2. We consider ordered sets that admit just bounded suprema, rather than all suprema as in [RW1], and amongst these we isolate those that are as completely distributive as possible. The 2-category of these ordered sets, functions that preserve bounded suprema, and inequalities is shown to be bi-equivalent to a variant of the idempotent splitting completion of the 2-category of relations. For the latter we take all idempotent relations (X, ≺) as objects and essentially consider the locally-full sub-2-category determined by those arrows of idempotents R : (X, ≺) \overline{}(A, ≺) which are bounded in the sense that there exists a function ρ : X \overline{}A such that, for all a ∈ A and all x ∈ X, aRx implies a ≺ ρ(x). However, for technical reasons related to our interest in working constructively, we take an arrow (X, ≺) \overline{}(A, ≺) to be a pair (R, ρ) as above. (The advantage of this approach will become most evident in the proof of Proposition 5.2.)

The authors gratefully acknowledge financial support from the Canadian NSERC. Diagrams typeset using M. Barr’s diagram macros.

1991 Mathematics Subject Classification: 18B35, 06D10.

Key words and phrases: adjunction, bounded suprema, completely distributive.

1.3. The bi-equivalence alluded to in 1.2 is the major goal of the paper and the question of 1.1 becomes a simple application. It transpires that the methodology used to establish the main bi-equivalence of [RW1] can be adapted to the present paper but to state matters clearly it is far better to take a more monad-theoretic approach than that of [RW1]. Section 2 extends the familiar ‘down-set’ 2-functor, D, on ordered sets in several directions. Ultimately we are able to see variants of D as both a representable 2-functor on the idempotent splitting completion of relations and a monad on the 2-category of idempotents and ‘below-preserving’ functions — which we call idm and introduce in 2.2. The monad D on idm is of the Kock-Zöberlein (KZ) kind [KOK]. In order to fully understand this crucial nature of D we are led to a notion of ‘broken adjoint string’ which we anticipate will be of independent interest.

1.4. In Section 3 we are able to construct what is essentially a sub-monad of D on idm, that we here call B. Restricted to ordered sets, B is the ‘bounded down-sets’ monad (although for the reason mentioned in 1.2 we use explicit bounds). The 2-functor B extends to a representable 2-functor on the 2-category of ‘idempotents and bounded idempotent arrows’ mentioned in 1.2 and at this level becomes the basic ingredient of the main bi-equivalence of the paper.

1.5. Section 4 addresses ordered sets with bounded suprema in a fairly general way, noting how some well-known ideas fit into a monad-theoretic context. It is here that we introduce the concept of complete distributivity for ordered sets that admit bounded suprema. We say that an ordered set with this property is a BCD order because of the parallels with CCD lattices as in [RW1]. Once again, we are able to express a distributive law by an adjunction. This is a little surprising in the present context since the 2-functor B does not naturally lead to the many adjunctions that D does. In this section we also construct the putative inverse of our equivalence in terms of an auxiliary relation that is of the same nature as the ‘totally-below’ relation of [RW1] and the even more familiar ‘way-below’ relation. Finally, in Section 5 we establish the desired bi-equivalence and conclude with the application of 1.1.

We are grateful for the comments that we received from the referee on an earlier version of this paper.

2. Preliminaries

2.1. The present paper makes extensive use of both the ideas and the notations of [RW1]. However, some simplifications of the latter are now in order. We write krl as an abbreviation for kar(rel), the Karoubian envelope (also called idempotent-splitting completion) of the 2-category of relations for some elementary topos known simply as set, whose objects are called ‘sets’. We understand krl to be a 2-category, with transformations (that is 2-cells) given by inclusion. An idempotent in rel, here simply called an idempotent and denoted by X = (|X|, ≺) = (X, ≺) and so on as in 1.1, will be seen as a generalized ordered set. We require of an ordered set X = (X, ≤) only that ≤ be reflexive and transitive; reflexivity provides trivial interpolation for ≤. The full sub-2-category of krl determined by the orders is easily seen to be what is usually called the 2-category of (order) ideals and we denote it by idl. (Our terminology is that of [C&S]. Explicitly, if X and A are orders then an ideal R : X \overline{}A is a relation R : |X| \overline{}|A| satisfying (b ≤ a and aRx implies bRx) and (aRx and x ≤ y implies aRy); there is no directedness requirement.) We see a set as a discrete ordered set so that we have full inclusions

[figure: rel; idl; krl]

If X and A are idempotents and R : |X| \overline{}|A| is any relation then R_{#} = ≺ · R · ≺ is an arrow of krl. It is well known that rel and idl admit all right liftings and all right extensions. It was shown in [RW1] that krl also admits all right liftings and all right extensions. They can be constructed by applying (−)_{#} to the corresponding entities in rel. More precisely; if we write | − | : krl \overline{}rel for the forgetful ‘semi-functor’ then for R : X \overline{}A \overline{}Y : S in krl the right lifting of S through R is given by (|R| ⟹ |S|)_{#}, where |R| ⟹ |S| is the right lifting of |S| through |R| in rel; and similarly for right extensions.

2.2. We write ord for the 2-category of ordered sets and order-preserving functions. Then set may be seen as the full sub-2-category of ord determined by the discrete orders. For f : X \overline{}A in ord, the graph f_{∗} of the function f is a relation for which (f_{∗})_{#} : X \overline{}A is an ideal that we abbreviate by f_{#}. In fact the definition of f_{#} as prescribed by 2.1 simplifies and we have af_{#}x if and only if a ≤ fx. Each such f_{#} is a map in idl, that is to say an arrow which has a right adjoint, and we will write f_{#} ⊣ f^{#}. We recall from [C&S] that up to Cauchy completeness in the sense of [LAW] these are the only maps of idl. The locally-full (−)_{#} : ord \overline{}idl (given on objects by the identity) is an example of proarrow equipment in the sense of [WD]. It is clear that the restriction of (−)_{#} : ord \overline{}idl to the discrete objects is just (−)_{∗} : set \overline{}rel and well known that set is map(rel), where map(−) denotes the locally-full sub-2-category determined by the maps. In the context of 2.1 it is natural to extend (−)_{#} : ord \overline{}idl to idempotents. For idempotents X and A a function f : |X| \overline{}|A| is said to be below-preserving if x ≺ y in X implies fx ≺ fy in A. In this case we write f : X \overline{}A. We write f_{#} : X \overline{}A as an abbreviation for the krl arrow (f_{∗})_{#}. For f, g : X \overline{}A below preserving we define f ≤ g to mean f_{#} ⊆ g_{#}. Idempotents and below-preserving arrows, ordered in this way, form a 2-category that here we call idm (but which in [RW1] was called inf). We recall from [RW1] that (−)_{#} : idm \overline{}krl is proarrow equipment. In fact, from the last paragraph of [RW1, Section 4] it is clear that the notion of Cauchy completeness generalizes easily from enriched category theory to proarrow equipment and, further, that up to Cauchy completeness, the arrows of the form f_{#}, for f below-preserving are the only maps in krl. We extend the notation used for orders and also write f_{#} ⊣ f^{#} for the adjunction in krl that arises from an arrow f in idm. Of course, ord can now be seen as the full sub-2-category of idm determined by the orders. However, for f : X \overline{}A a general arrow in idm we have af_{#}x if and only if (∃y)(a ≺ fy and y ≺ x). In an evident (but naive) sense, we have inclusions of proarrow equipments:

[figure: rel; idl; set; ord; (−)_{∗}; krl; idm; (−)_{#}; (−)_{#}]

2.3. The 2-category of all (constructively) completely distributive lattices, sup-preserving functions, and pointwise inequalities was denoted by ccd_{sup} in [RW1] and the central result there was the establishment of a bi-equivalence

ccd_{sup} ≃ krl.

Each of the 2-categories in the diagram above has been identified with a 2-category of completely distributive lattices by ‘pulling back’ this bi-equivalence. (For the cases of set and rel see [P&W]; for the others see [RW1].) Our present approach to imposing ‘boundedness’ on [RW1] is given in the context of this diagram.

2.4. For X in ord, it was convenient in [RW1] and its prequels to write DX for the ordered set ord(X^{op}, Ω), where Ω is the subobject classifier of set together with its natural order. It follows that DX ≅ idl(1, X), where 1 is the terminal object of set regarded as a discrete order. Furthermore, for X an idempotent, 𝔻X was defined in [RW1] to be the ordered set krl(1, X). Since idl is a full sub-2-category of krl it seems reasonable to simplify and rationalize the terminology. We will write D for the representable 2-functor krl(1, −) : krl \overline{}ord. Since, as noted in 2.1, krl is biclosed; for each Y ∈ krl, for each R : X \overline{}A in krl, krl(Y, R) has a right adjoint given by R ⟹ −. In particular DR = krl(1, R) has a right adjoint and we will write DR ⊣ DR : DA \overline{}DX. Since the orders DX are antisymmetric, the DR are uniquely defined and since the right adjoint of D1_{X} = 1_{DX} is 1_{DX}, it follows that we have a 2-functor D : krl^{coop} \overline{}ord, given on objects by D. If R ⊣ S then, since D is a 2-functor, we have DR ⊣ DS. In this case DR = DS. In particular, for f : X \overline{}A in idm, we have Df_{#} ⊣ Df_{#} = Df^{#} ⊣ Df^{#} and it is convenient to abbreviate the entries in this adjoint string in ord by Df ⊣ Df ⊣ 𝔻f, implicitly defining D, 𝔻 : idm \overline{}ord and D : idm^{coop} \overline{}ord, all of which are given on objects by the ‘down-set’ construction of 1.1, since krl(1, X) can be identified with the set of down-sets of X ordered by inclusion. In 2.7 we will describe this adjoint string more explicitly. We will not make a notational distinction when we compose any of these with the inclusion ord \overline{}idm or restrict to idl or to ord so, for example, we speak of the 2-functor D : ord \overline{}ord and of the 2-functor D : idm \overline{}idm. On the other hand it seems worthwhile to point out that for f : X \overline{}A in set, the string Df ⊣ Df ⊣ 𝔻f is often denoted ∃f ⊣ Pf ⊣ ∀f : PX \overline{}PA.

2.5. For an idempotent X = (X, ≺) we recall that an element of DX, a down-set, is a subset S of X with the property that x ∈ S if and only if (∃y)(x ≺ y ∈ S) and the order on DX is containment. In the following display we have written |X| for the underlying set of X, P− for power set and i : DX \overline{}P|X| for the inclusion function. Also, we have written j : DX \overline{}P|X|, where jS = \{x| ↓ x ⊆ S\} with ↓ x = \{y|y ≺ x\}. It is easy to see that S ⊆ T in DX if and only if jS ⊆ jT in P|X| so that j, like i, is full(y faithful) — a regular monomorphism since P|X| and DX are antisymmetric. We always have i ⊆ j but i = j if and only if (X, ≺) is an order. Here ‘if’ is well known and for ‘only if’ observe that if i = j then, for all x in X, x ∈ j(↓x) = i(↓x) =↓x shows ≺ to be reflexive. Down-sets are closed with respect to union and hence i has a right adjoint ∘, where A∘ is the union of all down-sets contained in A. We noted in [RW1] the slightly simpler formula A∘ = ⋃{↓x| ↓x ⊆ A}. If X is an order then this down-interior operator is joined by a ‘down-closure’ operator given by A ^{}= {x|(∃a)(x ≺ a ∈ A)}. If X is merely an idempotent, observe first that this formula nevertheless defines an order-preserving function (−) ^{}: P|X| \overline{}DX. Next, observe that ^{}preserves unions, which provide sups for both lattices, so that ^{}necessarily has a right adjoint. Direct calculation shows that ⊣ j, for j as described above. We always have ∘ ⊆ ^{}and

· i = 1_{DX} and ∘· j = 1_{DX}

The first of these displayed equations follows from ^{}· i ⊆ ^{}· j ⊆ 1_{DX}, the second containment being the counit for ^{}⊣ j, and 1_{DX} ⊆ ∘ · i ⊆ ^{}· i, the first containment being the unit for i ⊣ ∘. The second of the two equations is proved similarly. Note that DX provides a splitting for the idempotent i· ^{}on P|X| in the 2-category sup of complete lattices, sup-preserving functions and point-wise inequalities. For that matter, DX also provides a splitting in the 2-category inf of complete lattices, inf-preserving functions and point-wise inequalities, for the idempotent j · ∘ which is the right adjoint (in ord) of i · ^{}. The following diagram helps to summarize the situation. (The horizontal arrow is is just part of the display of ∘ ⊆ ^{}. We will use a similar notation in the diagram in Lemma 2.9)

[figure: ⊣; P|X|; DX; j ⊇ i; ⊣; ∘; ⊃]

2.6. Remark. A full systematic study of such ‘broken adjoint strings’ as ^{}⊣ j ⊇ i ⊣ ∘ might be interesting but would take us too far afield here. Another simple example is provided by a relation between mere sets, say R : X \overline{}A. From the general theory of 2.4 we have DR ⊣ DR : PA \overline{}PX but for mere sets we have rel(1, X) ≅ PX ≅ rel(X, 1). We can safely identify these and now using extension rather than lifting we also have rel(R, 1) ⊣ − ⟸ R : PX \overline{}PA. It is interesting to show that DR ⊇ rel(R, 1) if and only if R is a partial function and that DR ⊆ rel(R, 1) if and only if R is everywhere defined.

2.7. If X is an order then the adjoint string ^{}⊣ i ⊣ ∘ : P|X| \overline{}DX is itself an instance of Df ⊣ Df ⊣ 𝔻f, namely that where f : |X| \overline{}X is the X-component of the counit for the adjunction disc ⊣ | − | : ord \overline{}set, where disc provides the discrete order. Of course P|X| = D · disc|X|. The forgetful functor | − | : idm \overline{}set does have a left adjoint but it sends a set A to the idempotent (A, ∅). The only down-set for the empty idempotent is the empty set, so if X is an idempotent and we write f for the Xcomponent of the counit for the adjunction (−, ∅) ⊣ | − | then the resulting adjoint string is just Df ⊣ Df ⊣ 𝔻f : 1 \overline{}DX, which merely ensures us that, for X any idempotent, DX has both a bottom element and a top element. However, even though the ‘broken adjoint string’ of 2.5 is the situation for a general idempotent it still serves to describe the entries in the adjoint string

Df ⊣ Df ⊣ 𝔻f : DX \overline{}DA

for f : X \overline{}A in idm. First, Df(S) = krl(1, f_{#})(S) is the krl composite

1 ^{\overline{}^{S}} X ^{\overline{}^{f_{#}}} A

so that we have

a ∈ Df(S)
iff (∃x)(af_{#}x ∈ S)
iff (∃x)(∃y)(a ≺ fy and y ≺ x ∈ S)
iff (∃y)(a ≺ fy and y ∈ S)

from which the first and last lines show that Df is the composite

DX ^{\overline{}^{i}} P|X| ^{\overline{}^{∃|f|}} P|A| [figure] DA

It is now a simple matter to take right adjoints of the factors of Df to see that Df is given by

DX [figure: ∘] P|X| ^{\overline{}^{P|f|}} P|A| ^{\overline{}^{j}} DA,

generalizing ∘ · j = 1_{DX} of 2.5, which is the case f = 1_{X} : X \overline{}X. We will show below that Df is given equally by

DX [figure] P|X| ^{\overline{}^{P|f|}} P|A| ^{\overline{}^{i}} DA,

(generalizing ^{}· i = 1_{DX} of 2.5, the case f = 1_{X}) so that, again taking right adjoints of factors, 𝔻f is given by the composite

DX ^{\overline{}^{j}} P|X| ^{\overline{}^{∀|f|}} P|A| [figure: ∘] DA

2.8. Lemma. For f : X \overline{}A in idm, we have the following inequality:

P|X|  P|A| \overline{}∃|f| P|X|  P|A| \overline{}∃|f| i · ^{}i · ^{}⊆

Proof. Consider the square

[figure: |X|; |A|; |f|_{∗}; |X|; |A|; |f|_{∗}; ≺; ≺; ⊆]

in rel. It precisely expresses the fact that f is below-preserving. The power-set monad on set has rel for its Kleisli category and sup for its Eilenberg-Moore category. The comparison functor rel \overline{}sup translates the square above to the square of the statement.

The inequality of Lemma 2.8 provides the key to show that Df admits the two quite different descriptions in 2.7. We isolate the argument in terms of the ‘broken adjoint strings’ of 2.5. If A is an object in any ord-category then an idempotent A : A \overline{}A, if split by E : A \overline{}S and M : S \overline{}A, with right adjoints E^{∗} and M^{∗} respectively, generates a broken adjoint string as in the statement of Lemma 2.9. To see this, observe that applying E to MM^{∗} ≤ 1_{A} gives M^{∗} ≤ E from which we get M^{∗}M ≤ EM = 1_{S} and we already have 1_{S} ≤ M^{∗}M. Similarly we add M ≤ E^{∗} and 1_{S} ≤ EE^{∗} to the adjunction inequalities for E ⊣ E^{∗}. For X : X \overline{}X also an idempotent it is natural to say that an arrow F : X \overline{}A carries X to A if F X ≤ AF.

2.9. Lemma. For idempotents (X , X) and (A, A) in an ord-category, with splittings as displayed, assume that F carries X to A and has a right adjoint U. In this case the two arrows shown between the splittings are ‘isomorphic’ in the sense that each is less than or equal to the other.

[figure: P; ⊣; X; T; P^{∗}≥I; ⊣; I^{∗}; >; E; ⊣; A; S; E^{∗}≥M; ⊣; M^{∗}; >; F; U; ⊥; P UM; I^{∗}UE^{∗}]

Proof. Observe first that XU ≤ UA, being the mate inequality of F X ≤ AF, together with the splitting equations X = IP and A = ME provides IP U ≤ UME. Now to give an inequality P UM ≤ I^{∗}UE^{∗} is, by adjointness, to give an inequality EF IP UM ≤ 1_{S} which can be realized via EF IP UM ≤ EF UMEM ≤ EMEM = 1_{S}, using IP U ≤ UME, the counit for F ⊣ U and the splitting equation EM = 1_{S}. On the other hand, 1_{T} = P IP I ≤ P IP UF I ≤ P UMEF I; from the splitting equation P I = 1_{T}, the unit for F ⊣ U and again IP U ≤ UME; provides an inequality that gives I^{∗}UE^{∗} ≤ P UM by adjointness.

2.10. Corollary. The arrow

DX [figure: ∘] P|X| ^{\overline{}^{P|f|}} P|A| ^{\overline{}^{j}} DA

is equal to

DX [figure] P|X| ^{\overline{}^{P|f|}} P|A| ^{\overline{}^{i}} DA.

Proof. Use Lemma 2.8 to apply Lemma 2.9 with X = P|X|, T = DX, F = ∃|f| and so on.

2.11. For each idempotent X, there is a below-preserving function d_{X} : X \overline{}DX given by d_{X}(x) =↓ x = \{y|y ≺ x\}. For any f : X \overline{}A in idm, consider the noncommutative square

[figure: A; DA; d_{A}; X; DX; d_{X}; f; Df]

where, for all x ∈ X, we do have

Df · d_{X}(x) = {a ∈ A|(∃y)(a ≺ fy and y ≺ x)} ⊆ {a ∈ A|a ≺ fx} = d_{A} · f(x).

Note that Df · d_{X}(x) = {a ∈ A|af_{#}x} for a general arrow in idm while d_{A} · f(x) is that to which Df · d_{X}(x) simplifies if X is an order. A lemma is helpful.

2.12. Lemma. If f, g : X \overline{}A in idm are such that (∀x ∈ X)(fx ≺ gx) then f ≤ g.

Proof. Referring to 2.2, we must show that f_{#} ⊆ g_{#}. So assume that af_{#}x. From (∃y)(a ≺ fy and y ≺ x) and fy ≺ gy we have (∃y)(a ≺ gy and y ≺ x) so that ag_{#}x.

The 2-category idm is an ord-category so while the square in 2.11 does not commute it makes sense to consider its commutativity to ‘within isomorphism’.

2.13. Proposition. The arrows d_{X} : X \overline{}DX provide the components of a pseudonatural transformation d : 1_{idm} \overline{}D : idm \overline{}idm.

Proof. Let f : X \overline{}A be an arrow in idm. Since DA is ordered by inclusion, it follows from 2.11 and Lemma 2.12 that Df · d_{X} ≤ d_{A} · f, so we have only to verify the inequality d_{A} · f ≤ Df · d_{X}. Assume that S(d_{A} · f)_{#}x, for S a down-set of A and x ∈ X. Thus (∃y)(S ⊆↓fy and y ≺ x). We can interpolate y ≺ x to get y ≺ z ≺ x and now it follows that S ⊆ {a ∈ A|af_{#}z}, which just as in 2.11 gives S ⊆ Df · d_{X}(z). This last together with z ≺ x gives S(Df · d_{X})_{#}x.

We recall that 2-monads, or even pseudo-monads, are known as KZ-doctrines when they have the property that algebraic structures are necessarily left adjoint to a component of the unit. A standard reference is [KOK] but we will follow the approach of [MAR]. In the case of a KZ-doctrine on an ord-category the pseudo-monad data reduces to a homomorphism (pseudo-functor) D of the given ord-category and a pseudonatural unit d : 1 \overline{}D. The sole requirement for this data is that there exists a fully faithful adjoint string Dd ⊣ m ⊣ dD.

2.14. Theorem. The pair D = (D, d) provides a KZ-doctrine on idm.

Proof. For any X in idm, the arrow dX : X \overline{}DX gives rise to the adjoint string

DdX ⊣ DdX ⊣ 𝔻dX : DX \overline{}DDX.

For S ∈ DDX we see from the second description of D in 2.7 that DdX(S) = {a| ↓ a ∈ S} ^{}. We claim that DdX(S) = ⋃ S, for we have

x ∈ ⋃ S
iff (∃S)(x ∈ S ∈ S)
iff (∃S)(∃a)(x ∈↓a ⊆ S ∈ S)
iff (∃a)(x ≺ a and ↓a ∈ S)
iff x ∈ DdX(S).

Since DX is a complete lattice for which supremum is given by union, it follows that 𝔻dX = dDX and thus we have a fully faithful adjoint string

DdX ⊣ DdX ⊣ dDX : DX \overline{}DDX,

so that, (D, d) is a KZ-doctrine.

2.15. Corollary. The 2-functor D = krl(1, −) : krl \overline{}ord factors through the (nonfull) inclusion ccd_{sup} \overline{}ord.

Proof. For every idempotent X, the fully faithful adjoint string DdX ⊣ DdX ⊣ dDX exhibits DX as a CCD lattice while, for every arrow R : X \overline{}A in krl, the adjunction DR ⊣ DR of 2.4 shows that DR is sup-preserving.

3. Bounded down-sets

3.1. For idempotents X = (|X|, ≺) and A = (|A|, ≺), consider a pair (R, ρ), where R : X \overline{}A is an arrow of krl, ρ : |X| \overline{}|A| is a function and

aRx implies a ≺ ρ(x)

(equivalently, R ⊆≺_{A} ·ρ_{∗}). Given another such pair (S, σ), we define (R, ρ) ≤ (S, σ) to mean precisely that R ⊆ S. Write krl_{bd}(X, A) for the resulting ordered set — evidently not antisymmetric — of all such pairs and (R, ρ) : X \overline{}A for a typical element.

3.2. Lemma. For (R, ρ) : X \overline{}A in krl_{bd}(X, A) and (S, σ) : A \overline{}Y in krl_{bd}(A, Y), (SR, σρ) : X \overline{}Y is in krl_{bd}(X, Y).

Proof. SR ⊆ S· ≺_{A} ·ρ_{∗} = S · ρ_{∗} ⊆≺_{Y} ·σ_{∗} · ρ_{∗} =≺_{Y} ·(σρ)_{∗}.

3.3. Since the identity for (X, ≺) in krl is ≺, the pair (≺, 1_{X}) : X \overline{}X is in krl_{bd}(X, X) and it is clear that the definitions provide an ord-category, henceforth denoted krl_{bd}. The subscript is intended to convey the idea that we speak of bounded arrows of krl. Given (R, ρ) as above we may speak of ρ as a bound for R and if ρ′ is some other bound then (R, ρ) and (R, ρ′) are isomorphic arrows of krl_{bd}. To make some calculations more readable we will often write R for (R, ρ) when there is no danger of confusion; for krl_{bd} is essentially a locally-full sub-2-category of krl, having the same objects. It is interesting to note the full sub-2-category of krl_{bd} determined by the discrete orders regarded as idempotents, which further to the diagram in 2.2 could be called rel_{bd}. The objects are mere sets and any arrow from X to A in rel_{bd} gives rise to a partial function from X to A which can be extended to a function from X to A. Classically, the only partial functions which do not arise in this way are the partial functions from non-empty sets to the empty set.

3.4. If f : X \overline{}A is in idm then, as for any function |X| \overline{}|A|, we have af_{#}x, if and only if (∃y)(a ≺ fy and y ≺ x). Invoking preservation of ≺ we see that the pair (f_{#}, |f|) : X \overline{}A is in krl_{bd}. It is clear that the proarrow equipment (−)_{#} : idm \overline{}krl essentially factors over krl_{bd} \overline{}krl but it should not be supposed that idm \overline{}krl_{bd}, given by f \overline{}(f_{#}, |f|), is again proarrow equipment. For (f_{#}, |f|) : X \overline{}A is seen to have a right adjoint in krl_{bd} if and only if f^{#} is bounded, say by φ : |A| \overline{}|X|, and taking f to be ∅ \overline{}1 shows that such a φ may fail to exist. If f : X \overline{}A has a right adjoint u : A \overline{}X in idm, which is easily seen to mean that

(∃y)(x ≺ y and fy ≺ a) iff (∃b)(x ≺ ub and b ≺ a),

then necessarily (u_{#}, |u|) = (f^{#}, |u|) is right adjoint to (f_{#}, |f|) in krl_{bd} but this is stronger than requiring that f^{#} be bounded.

3.5. Specializing the definitions of 3.1, we find it convenient to write BX = krl_{bd}(1, X). Thus BX is the ordered set consisting of pairs (S, β), where S is a down-set of X, β is an element of X and, for all s ∈ S, s ≺ β. Since (S′, β′) ≤ (S, β) if and only if S′ ⊆ S, it is convenient to think of BX as the ordered set of bounded down-sets of X; for as in 3.3, if both β and β′ provide bounds for S then (S, β) ≅ (S, β′) in BX. In this context especially we will feel free to write S for (S, β) when an explicit β has already been exhibited. The definition of B extends to arrows and inequalities of krl_{bd} by defining it to be the representable 2-functor krl_{bd}(1, −) : krl_{bd} \overline{}ord. With the help of idm \overline{}krl_{bd} as in 3.4 and ord[figure] idm we have B : idm \overline{}idm. To be clear: if f : X \overline{}A in idm and (S, β) ∈ BX then Bf(S, β) = ({a ∈ A|(∃x)(a ≺ fx and x ∈ S)}, fβ).

3.6. For each idempotent X, there is a below-preserving function bX = b_{X} : X \overline{}BX given by b_{X}(x) = (↓x, x). Since d_{X} : X \overline{}DX factors through BX \overline{}DX and each Bf can be seen as a restriction of Df, the considerations of 2.11, 2.12 and 2.13 apply and we have immediately:

3.7. Proposition. The arrows b_{X} : X \overline{}BX provide the components of a pseudonatural transformation b : 1_{idm} \overline{}B : idm \overline{}idm.

3.8. Theorem. The pair B = (B, b) provides a KZ-doctrine on idm.

Proof. Observe first that, in any bicategory, if we have squares

[figure: Y; B; X; A; i; j; g; v; f; u]

which commute to within isomorphism, with both i and j fully faithful, then g ⊣ v implies f ⊣ u. Write i for the fully faithful 2-natural transformation B[figure] D and note that both squares in

[figure: D; DD; B; BB; i; ii; Dd; dD; Bb; bB]

commute, by using i · b = d and ‘naturality’. By 2.14 we have a fully faithful adjoint string Dd ⊣ ⋃ ⊣ dD : D \overline{}DD, so applying our first observation, twice, we see that an arrow ⋁ : BB \overline{}B, satisfying i · ⋁ = ⋃ ·ii will provide an adjoint string Bb ⊣ ⋁ ⊣ bB : B \overline{}BB, necessarily fully faithful. It is clear that ⋁(S, (S, β)) = (⋃ S, β) is well-defined and satisfies the equation above. (The situation might be verbalised by saying that a bounded union of bounded sets is bounded.)

We might note that B[figure] D is a morphism of monads and from the second square in the proof above we see that this rests solely on the ‘morphism of units’ condition i · b = d. We could say that B is a sub-KZ-doctrine of D.

3.9. Corollary. The restriction of (B, b) to ordered sets is a KZ-doctrine on ord.

4. Bounded suprema

4.1. An ordered set X supports a B-algebra structure if and only if bX : X \overline{}BX has a left adjoint which is the case if and only if X admits suprema of bounded subsets — the adjoint being given by (S, β) \overline{}⋁ S. It is basic that such an ordered set admits inhabited (classically, non-empty infima) but the underlying structural reasons for this are worthy of examination and help to provide a context for our approach to distributivity. First, let us write U = (U, u) = ((D(−)^{op})^{op}, (d_{(−)^{op}})^{op}) for the ‘up-set’ monad on ord. Thus UX is the set of ‘up-sets’ of X with superset order while, for f : X \overline{}A in ord, ‘up-closure’ of direct image of f describes Uf. We caution that it follows from the presence of the outer ‘(−)^{op}’ that Uf is right adjoint to inverse image along f. The monad U is often described as being of the coKZ kind in that we have a fully faithful adjoint string uU ⊣ Uu ⊣ Uu, where U = (D(−)^{op})^{op}. Necessarily, an object X is a U-algebra if and only if uX has a right adjoint. (Note that the formulas given allow one to interpret U as a coKZ doctrine on idm too, since the involution (−)^{op} : ord^{coop} \overline{}ord extends in an obvious way to idm.) Consider next the commutative triangles

[figure: DX; UX; X; d_{X}; u_{X}; (−)_{X}^{+}; (−)_{X}^{−}; ⊥]

where (−)^{+}, respectively (−)^{−}, provides the set of upper bounds, respectively lower bounds, and which, with the present emphasis, should be called the Isbell conjugation operators. As indicated in the diagram, (−)^{+} is left adjoint to (−)^{−}. Now suppose that X has all suprema so that we have ⋁ ⊣ d_{X}. The familiar argument that X necessarily has all infima rests on the observation that u_{X} ⊣ ⋁ ·(−)_{X}^{−}, which we dissect as follows: the counit ⋁ ·d_{X} ≤ 1_{X} is an isomorphism since d_{X} is fully faithful from which using the equality d = (−)^{−} · u we get 1_{X} ≤ (⋁ ·(−)_{X}^{−}) · u_{X}. The counit ⋁ ·d_{X} ≤ 1_{X} also provides u_{X} · ⋁ ·d_{X} ≤ u_{X}, which since (−)^{+} is the right (Kan) extension of u along d provides u_{X} · ⋁ ≤ (−)_{X}^{+} which by the adjointness (−)^{+} ⊣ (−)^{−} provides u_{X} · (⋁ ·(−)_{X}^{−}) ≤ 1_{UX}.

Now write NX for the set of pairs (T, α) with α ∈ T ∈ UX, ordered by (T, α) ≤ (T′, α′) if and only if T ⊇ T′; so that NX is essentially the set of inhabited up-sets of X (ordered by reverse inclusion). Evidently u factors through the fully faithful N[figure] U and we write n : 1_{ord} \overline{}N. Observe that defining (S, β)^{+} = (S^{+}, β) and (T, α)^{−} = (T^{−}, α) gives an adjunction (−)^{+} ⊣ (−)^{−} : N \overline{}B which commutes with b and n as shown below.

[figure: BX; NX; X; b_{X}; n_{X}; (−)_{X}^{+}; (−)_{X}^{−}; ⊥]

Furthermore, each of the statements that we emphasized above in the discussion about the ‘D and U’ triangle has a counterpart in the ‘B and N’ triangle, showing that existence of all bounded suprema implies existence of all inhabited infima. Finally, it is a straightforward matter to define N on arrows so that N = (N, n) is a sub-coKZ-doctrine of U = (U, u). The coKZ property can be shown by adapting the argument in Theorem 3.8 and noticing that an inhabited union of inhabited sets is inhabited. Just as existence of all infima in X provides all suprema as well, so it is that if X is an N-algebra then X is a B-algebra. The structural argument is similar to that which we outlined above for suprema providing infima.

4.2. In [MRW] it is shown that there is an adjoint pair of distributive laws l ⊣ r : UD \overline{}DU (which classically, and only classically, are inverse isomorphisms) and that the distributivity of U over D provided by r gives a monad structure on DU, the algebras for which are the (constructively) completely distributive lattices. It is shown that, for an ordered set X and T ∈ UDX,

rX(T ) = {T ∈ UX|(∀S ∈ T )(∃x ∈ T)(x ∈ S)}.

Let (T , (S_{0}, β_{0})) be a typical element of NBX and define

rX(T , (S_{0}, β_{0})) = ({(T, α) ∈ NX|(∀(S, β) ∈ T )(∃x ∈ T)(x ∈ S)}, (↑β_{0}, β_{0})).

To show that this putative definition of an arrow r : NB \overline{}BN makes sense we must show that (↑β_{0}, β_{0}) does bound the set of (T, α) described above. In other words, we must show that if (T, α) satisfies (∀(S, β) ∈ T )(∃x ∈ T)(x ∈ S) then T ⊇↑ β_{0}. Consider then a witness, call it x_{0}, for the condition as it pertains to (S_{0}, β_{0}). Now certainly x_{0} ≤ β_{0} because x_{0} ∈ S_{0}. Then, since T is an up-set, x_{0} ≤ β_{0} and x_{0} ∈ T implies that β_{0} ∈ T. Of course this shows that T ⊇↑ β_{0}. It follows then that r : NB \overline{}BN, given as above for rX(T , (S_{0}, β_{0})), is essentially a restriction of r : UD \overline{}DU and that it is ord-natural.

4.3. Lemma. The ord-natural r : NB \overline{}BN provides a distributive law of N over B.

Proof. Since B is KZ and N is coKZ, it follows from [MRW] that we have only to show the following two triangles commute, the commutativity of the usual pentagons following automatically in this case.

[figure: NB; BN; r; N; Nb; bN; B; nB; Bn]

However, this is immediate from the corresponding triangles for r : UD \overline{}DU, since d factors through b and u through n.

4.4. We recall from [BEK] that an algebra for the composite monad on BN obtained via a distributive law r : NB \overline{}BN is an object in the base category together with a B-algebra structure and an N-algebra structure, subject to the requirement that the B-algebra structure arrow be a homomorphism of N-algebras. Recall too that the last requirement makes sense because a distributive law is equivalent to the existence of a lift of the monad B to the category of N-algebras. It should be clear from 4.1 that in discussing algebras for the monad BN on ord, arising from r : NB \overline{}BN, we can start with an ordered set (X, ≤), which admits suprema of bounded down-sets, ⋁ : BX \overline{}X, and be automatically ensured of infima of inhabited up-sets, ⋀ : NX \overline{}X.

4.5. Lemma. For an ordered set (X, ≤) admitting suprema of bounded down-sets, the following are equivalent:

i) Non-empty infima distribute over suprema of bounded down-sets;

ii) For every T ∈ NBX,

⋀{⋁ S|S ∈ T } ≅ ⋁{⋀{T (S)|S ∈ T }|T ∈ ∏ T };

iii) X is a BN-algebra;

iv) For every T ∈ NBX,

⋀{⋁ S|S ∈ T } ≅ ⋁{⋀ T |T ∈ r(T )};

v) ⋁ : BX \overline{}X preserves inhabited infima;

vi) ⋁ : BX \overline{}X has a left adjoint.

Proof. First observe that i) is but the colloquial way of saying what is precisely formulated in ii). Next, we note that the argument given in Lemma 1 of [F&W] shows that, for all T ∈ NBX, {⋀{T (S)|S ∈ T }|T ∈ ∏ T } = ⋂ T so that ii) is equivalent to saying that the lower quadrilateral commutes, to within isomorphism, in the following diagram:

[figure: NX; BX; X; ⋀; ⋁; NBX; BNX; rX; N ⋁; B ⋀; ⋂]

Since ⋂ : NBX \overline{}BX provides inhabited infima for BX it is clear that this statement is at once equivalent to saying that ⋁ : BX \overline{}X is a homomorphism of N-algebras, which in the present context is equivalent to iii), and that v) is but another expression for the same state of affairs. For any N-algebra X, the top triangle of the diagram commutes, it being a generality about distributive laws that if ⋀ : NX \overline{}X is an N-structure arrow then so is B ⋀ .rX : NBX \overline{}BX. Clearly then, commutativity of the pentagon, which is iv), is equivalent to the commutativity of the quadrilateral. Trivially, vi) implies v). Finally, for v) implies vi) note that a left adjoint to ⋁ : BX \overline{}X, say s : X \overline{}BX, is formally given for x ∈ X, by s(x) = ⋀{S|x ≤ ⋁ S}. In any event this infimum exists since the set of such S with x ≤ ⋁ S certainly has its non-emptiness witnessed by the bounded down-set ↓x. The arrow defined by this s then is left adjoint to ⋁ : BX \overline{}X precisely if the defining infima are preserved by ⋁ : BX \overline{}X.

If we did not work in the ambience of down-sets, we would arrive at a less tractable notion than that found in Lemma 4.5. More precisely, if we were to drop the ‘down-’ in i) above then we would arrive at an apparently stronger notion, which is equivalent to our concerns precisely in the presence of the axiom of choice. We have concluded that, for an ordered set L admitting bounded suprema, ⋁ : BL \overline{}L having a left adjoint is the constructive way to assert that inhabited infima distribute over the relevant bounded suprema. Our formal definition below provides a convenient acronym and generalizes the notion of constructively completely distributive lattice (CCD) given in [F&W].

4.6. Definition. An ordered set L having bounded suprema is BCD if and only if ⋁ : BL \overline{}L has a left adjoint.

4.7. Proposition. For any idempotent (X, ≺), the ordered set BX is BCD.

Proof. This follows immediately from Theorem 3.8.

4.8. We write bcd_{bsp} for the 2-category of BCD orders, (order-preserving) functions that preserve bounded suprema, and pointwise inequalities. For order-preserving f : L \overline{}M we have Bf : BL \overline{}BM given by Bf(S, β) = (∃f(S) ^{}, fβ). (Compare with 3.5.) It is helpful to note that the condition on arrows in bcd_{bsp} is simply that the canonical inequality ⋁ ·Bf ≤ f · ⋁ be an isomorphism. Rather formally then, we could say that bcd_{bsp} is the full sub-2-category of the 2-category of B-algebras, ord^{B}, determined by the BCD objects. We have also in 3.5 written B for the representable 2-functor krl_{bd}(1, −) : krl_{bd} \overline{}ord and we turn again to this point of view. Unlike the situation for D = krl(1, −) in 2.4, we do not have all right liftings in krl_{bd}, so it is not the case that B(R, ρ) has a right adjoint for every arrow (R, ρ) in krl_{bd}. However, since composition in krl_{bd} is essentially relational composition, which preserves unions, we see that the B(R, ρ) preserve the suprema that exist. Formally, for (R, ρ) : X \overline{}A in krl_{bd} and (S, (U, γ)) in BBX we have

B(R, ρ) · ⋁(S, (U, γ)) = (R, ρ)(⋃ S, γ)
= (R ⋃ S, ρ(γ))
= (⋃{RS|S ∈ S}, ρ(γ))
= ⋁ ·(∃B(R, ρ)(S) ^{}, (RU, ρ(γ))

= ⋁ ·(∃B(R, ρ)(S) ^{}, B(R, ρ)(U, γ))
= ⋁ ·B(B(R, ρ))(S, (U, γ))

which shows, together with 4.7:

4.9. Proposition. The 2-functor B = krl_{bd}(1, −) factors through the (non-full) inclusion bcd_{bsp} [figure] ord.

We will write B : krl_{bd} \overline{}bcd_{bsp}.

4.10. For l and m elements of an ordered set L having bounded suprema, define

l ◁ m iff (∀(S, β) ∈ BL)(m ≤ ⋁ S implies l ∈ S).

Equivalently ◁ : L \overline{}L is the right extension of b_{L}^{#} : BL \overline{}L along ⋁_{#} : BL \overline{}L in the 2-category of ordered sets and order ideals. The items i) and ii) below express the ideal property, while iii) and iv) follow easily from the definition.

4.11. Proposition. The relation ◁ satisfies

i) l ≤ m ◁ n implies l ◁ n

ii) l ◁ m ≤ n implies l ◁ n

iii) l ◁ m implies l ≤ n

iv) l ◁ m ◁ n implies l ◁ n

The order ideal ◁ : L \overline{}L can be seen as the order preserving L \overline{}DL given by m \overline{}\{l|l ◁ m\} and by iii) of Proposition 4.11 we can see this as s : L \overline{}BL, with s(m) = ({l|l ◁ m}, m).

4.12. Proposition. If ⋁ : BL \overline{}L has a left adjoint, it is given by s : L \overline{}BL.

Proof. As noted in the proof in 4.5, if ⋁ : BL \overline{}L has a left adjoint then its value at m ∈ L is the intersection of all bounded S such that m ≤ ⋁ S — which intersection is bounded by m. It is clear from the definition in 4.10 that the required intersection is {l|l ◁ m}.

4.13. For X in idm (in particular in ord) it remains convenient to write bX(x) = b_{X}(x) = (↓x, x). For the BCD order BX we have from Theorem 3.8 that BbX ⊣ ⋁ : BBX \overline{}BX. So taking L = BX in Proposition 4.12, and ignoring one layer of bounds for readability, we have

sb_{X}(x) = s(↓x, x) = {(↓y, y)|y ≺ x} ^{}= {(S, β)|S ◁ ↓x}

from which it is apparent that if y ≺ x then ↓y ◁ ↓x.

Next, we have the “interpolation lemma” (which also shows that s ⊣ ⋁ ⊣ b_{L} is yet another example of the distributive adjoint strings studied in [RW2]).

4.14. Lemma. If L is a BCD order then (L, ◁) is an idempotent.

Proof. From iv) of Proposition 4.11 ◁ is transitive, so we have only to show that ◁ is interpolative. Assume that l ◁ m in L. Define S = {x|(∃n)(x ◁ n ◁ m)}. For any x in S, x ≤ m so that (S, m) ∈ BL. Now (S, m) = ⋁{s(n)|n ◁ m} from which it follows that ⋁(S, m) = m. Now l ◁ m ≤ ⋁ S provides l ∈ S and hence (∃n)(l ◁ n ◁ m).

4.15. Our task now is to extend Lemma 4.14 so as to give a 2-functor bcd_{bsp} \overline{}krl_{bd}. Given an arrow f : L \overline{}A in bcd_{bsp}, we have f_{#} : (L, ◁) \overline{}(A, ◁) in krl and the assignment is evidently order preserving in f. The argument in Lemma 15 of [RW1] (using the mate, s · f ≤ Bf · s, of f ⋁ ≅ ⋁ Bf) survives to show that f \overline{}f_{#} is functorial, for f preserving bounded suprema. Such f need not preserve the ◁ relation (and for that matter supremum preserving functions between CCD lattices need not preserve the totally below relation). The extra requirement needed in the present context is a bound for f_{#}. To assume af_{#}l is to assume (∃p)(a ◁ f(p) and p ◁ l), from which (∃p)(a ◁ f(p) and p ≤ l) follows using iii) of Proposition 4.11 and hence (∃p)(a ◁ f(p) and f(p) ≤ f(l)). Finally, a ◁ f(l) follows from ii) of Proposition 4.11 so that |f| is a bound for f_{#}. It follows that f \overline{}(f_{#}, |f|) defines an assignment on arrows and inequalities between them that, together with L \overline{}(L, ◁) on objects, provides a 2-functor bcd_{bsp} \overline{}krl_{bd}.

5. The bi-equivalence and an application

5.1. For L a BCD order, iii) of 4.11 shows that the identity function is below-preserving from (L, ◁) to (L, ≤). In particular, for an idempotent X, the identity is below-preserving from (BX, ◁) to BX = (BX, ⊆). Let us write AX = (BX, ◁). The below-preserving b_{X} : X \overline{}BX factor through the AX \overline{}BX, for we observed in 4.13 that if x ≺ y in X then ↓y ◁ ↓x. We will write a_{X} : X \overline{}AX for the resulting below-preserving functions.

5.2. Proposition. For X in krl_{bd}, the (a_{X})_{#} : X \overline{}AX provide the components of a 2-natural equivalence 1_{krl_{bd}} ^{\overline{}^{≃}} (−, ◁)B.

Proof. Adapting the calculations in [RW1, Proposition 11 and Theorem 17] we see that the krl arrows (a_{X})^{#} : AX \overline{}X, if bounded, provide inverses for the 2-natural (a_{X})_{#}. Define ♭ : |AX| \overline{}|X| by ♭(S, β) = β. Now x(a_{X})^{#}(S, β) iff (∃y)(x ≺ y and a_{X}(y)◁(S, β) iff (∃y)(x ≺ y and ↓y ◁ S). In the latter case we have x ∈↓y ⊆ S, hence x ∈ S and thus x ≺ β. Thus x(a_{X})^{#}(S, β) implies x ≺ ♭(S, β) showing that ((a_{X})^{#}, ♭) is an arrow AX \overline{}X in krl_{bd}.

5.3. For L a BCD order, B(L, ◁) ⊆ B(L, ≤). For if l ≤ m ∈ S, where (S, β) is a bounded down-set with respect to ◁, then (∃n)(l ≤ m ◁ n ∈ S) from which (∃n)(l ◁ n ∈ S) shows that l ∈ S so that S is a down-set with respect to ≤, while β being a ◁ bound is certainly a ≤ bound. We have ⋁_{L} : B(L, ◁) \overline{}L, the restriction of ⋁ : B(L, ≤) \overline{}L. The latter we already know to be an arrow of bcd_{bsp} but so is the former because (bounded) suprema for B(L, ◁) are, like those of B(L, ≤), given by union.

5.4. Proposition. For L in bcd_{bsp}, the ⋁_{L} : B(L, ◁) \overline{}L provide the components of a 2-natural equivalence B(−, ◁) ^{\overline{}^{≃}} 1_{bcd_{bsp}}.

Proof. The s : L \overline{}B(L, ≤) which provide the left adjoints to the ⋁ : B(L, ≤) \overline{}L certainly factor through the B(L, ◁), for each {l|l◁m} is manifestly a down-set with respect to ◁. The calculations to show that the resulting s_{L} : L \overline{}B(L, ◁) provide inverses for the 2-natural ⋁_{L} : B(L, ◁) \overline{}L are the same as those given in [RW1, Proposition 13 and Theorem 17] for the CCD case.

5.5. Theorem. The data introduced constitute a 2-adjoint 2-equivalence

a, ⋁ : B ⊣ (−, ◁) : bcd_{bsp} \overline{}krl_{bd}.

5.6. In the classical base topos of Mathematics, the ordered set of non-negative reals (ℝ_{0}^{+}, ≤) is a BCD order, with ◁ given by <, strict inequality. Thus, B(ℝ_{0}^{+}, <) ≅ ℝ_{0}^{+}. The inclusion i : (ℚ_{0}^{+}, <) \overline{}(ℝ_{0}^{+}, <) of the non-negative rationals is below-preserving so that we have (i_{#}, i) : (ℚ_{0}^{+}, <) \overline{}(ℝ_{0}^{+}, <) in krl_{bd}. Following the argument in [RW1] we see that (i_{#}, i) is an equivalence provided only that i^{#} is bounded. Defining ι : ℝ_{0}^{+} \overline{}ℚ_{0}^{+} to be the composite of the ceiling function ℝ_{0}^{+} \overline{}ℕ and the inclusion ℕ \overline{}ℚ_{0}^{+} provides such a bound. Applying B to the equivalence (i_{#}, i) and composing with B(ℝ_{0}^{+}, <) ≅ ℝ_{0}^{+} provides

B(ℚ_{0}^{+}, <) ≅ ℝ_{0}^{+}.

Since the construction of (ℚ_{0}^{+}, <) in any topos with natural numbers object requires only positive statements, the isomorphism above affords a definition of a version of ℝ in that generality.

References

[BEK] J. Beck, Distributive laws, Springer Lecture Notes in Math 80:119–140, 1969.

[C&S] A. Carboni and R. Street, Order ideals in categories, Pacific Journal of Mathematics, 124:275–278, 1986.

[C&W] A. Carboni and R.F.C. Walters, Cartesian bicategories I, Journal of Pure and Applied Algebra, 49:11–32, 1987.

[F&W] B. Fawcett and R. J. Wood, Constructive complete distributivity I, Math. Proc. Cam. Phil. Soc., 107:81-89, 1990.

[KOK] A. Kock, Monads for which structures are adjoint to units, Journal of Pure and Applied Algebra, 104:41-59, 1995.

[LAW] F.W. Lawvere, Metric spaces, generalized logic and closed categories, Rendiconti del seminario matematico e fisico di Milano, 43:135-166, 1973.

[MAR] F. Marmolejo, Doctrines whose structure forms a fully faithful adjoint string, Theory and Applications of Categories, 3:23-44, 1997.

[MRW] F. Marmolejo, R. Rosebrugh and R. J. Wood, A basic distributive law, to appear.

[P&W] M.C. Pedicchio and R.J. Wood, Groupoidal completely distributive lattices, Journal of Pure and Applied Algebra, ‘Barr volume’ to appear.

[RW1] R. Rosebrugh and R. J. Wood, Constructive complete distributivity IV. Applied Categorical Structures, 2:119-144, 1994.

[RW2] R. Rosebrugh and R. J. Wood, Distributive adjoint strings, Theory and Applications of Categories, 1:119-145, 1995.

[WD] R. J. Wood, Proarrows I, Cahiers de topologie et géometrie différentielle catégoriques, XXIII:279–290, 1982.

Robert Rosebrugh Department of Mathematics and Computer Science Mount Allison University Sackville, NB, E0A 3C0 Canada and RJ Wood Department of Mathematics, Statistics and Computing Science Dalhousie University Halifax, NS, B3H 3J5 Canada

Email: rrosebrugh@mta.ca and rjwood@mscs.dal.ca