The Constructive Lift Monad

Abstract

The lift monad is the construction which to a poset freely adjoins a bottom
element to it, or equivalently (from the classical viewpoint), the construction which freely adjoins suprema for subsets with at most one element. In constructive mathematics (i.e. inside a topos), these two constructions are no longer equivalent, since the equivalence is based on the boolean reasoning that a set with at most one element either is a singleton {x}, or is empty.
Likewise based on boolean reasoning is the proof of two important properties of the lift monad T :
1) If a poset C has filtered suprema, then so does TC.
2) Every poset with a bottom element ? is "free", i.e. comes about by
applying T to some poset (namely the original poset less the bottom).
Both these properties fail to hold constructively, if the lift monad is interpreted
as "adding a bottom"; see Remark below. If, on the other hand,
we interpret the lift monad as the one which freely provides supremum for
each subset with at most one element (which is what we shall do), then the first property holds; and we give a necessary and sufficient condition that the second does. Finally, we shall investigate the lift monad in the context of (constructive) locale theory. I would like to thank Bart Jacobs for guiding me to the literature on Z-systems; to Gonzalo Reyes for calling my attention to Barr's work on totally connected spaces; to Steve Vickers for some pertinent correspondence.
I would like to thank the Netherlands Science Organization (NWO) for supporting my visit to Utrecht, where a part of the present research was carried out, and for various travel support from BRICS.