Boundedness and complete distributivity (Q5956928)

In a previous paper [\textit{R. Rosebrugh} and \textit{R. J. Wood}, Appl. Categ. Struct. 2, No. 2, 119-144 (1994; Zbl 0804.06013)], the authors showed that there was a bi-equivalence between the 2-categories of constructively completely distributive lattices with sup-preserving arrows and that of the idempotent splitting completion of the 2-category of relations; this is all relative to the base topos. Furthermore, as an outcome of this bi-equivalence they were able to obtain a simple construction of the closed unit interval as an ordered set. The motivation for the paper under review is to try to modify these ideas in such a way as to obtain a similar construction for the non-negative reals. The necessary adjustment is to consider ordered sets with bounded suprema over which inhabited infina distribute. This leads to a 2-category which is bi-equivalent to a variation of the idempotent splitting completion of the 2-category of relations. The article takes a more monad theoretic approach than its predecessor by considering variants of the down-set monad. In the process of obtaining the new bi-equivalence and the desired simple construction of the non-negative reals, several interesting results are obtained along the way.