An algebraic approach to stable domains

Day [75] showed that the category of continuous lattices and maps which preserve directed joins and arbitrary meets is the category of algebras for a monad over Set, Sp or Pos, the free functor being the set of filters of open sets. Separately, Berry [78] constructed a cartesian closed category whose morphisms preserve directed joins and connected meets, whilst Diers [79] considered similar functors independently in a study of categories of models of disjunctive theories. Girard [85] built on Berry’s work to build a new and very lean model of polymorphism. In this paper we bring these strands together, defining a monad based on filters of con-nected open sets and showing that its category of algebras has Berry’s (stable) morphisms and is cartesian closed. The objects have multijoins as in Diers ’ work, and the slices are continuous lattices. The monad can only be defined for locally connected spaces, so via [Barr-Pare ́ 80] there is a further (unexplained) connection with cartesian closure. Jung [87] has shown that the same objects (L-domains) also form a cartesian closed category with maps preserving only directed joins. Berry’s proof of cartesian closure (using the trace factorisation, which also occurs in Diers ’ work and is discussed in [Taylor 88]) and more direct proofs by Coquand [88] and Lamarche [88] use two additional hypotheses, strong finiteness and distributivity (of finite meets over finite joins). Our proof is the first to use neither of these, but it does use distributivity of codirected meets over directed joins, which [Taylor 88] shows not to be needed either. Lamarche has shown that evaluation does not preserve equalisers, so in the categorical context connected limits must be replaced by wide pullbacks. He has also found a generalised notion of neighbourhood system which unifies stable and continuous functions and generalises our ad hoc notion of Berry order between continuous functions