Let us deepen our understanding of the Hoare powerspace construction. We shall see that it defines a so-called *monad*. I’ll define everything needed to understand the latter as we go along.

**Monads**

I have briefly mentioned monads in Filters IV. There is an equivalent way of presenting monads (on a category **C**), as the following data (I don’t expect you to understand those equations for now, we shall illustrate them shortly):

- for each object
*X*of**C**, an object**T***X*in**C** - for each object
*X*of**C**, a morphism η:_{X}*X*→**T***X*called the*unit*of the monad - an
*extension operation*†, transforming every morphism f:*X*→**T***Y*into a morphism f^{†}:**T**X →**T**Y, so that the following equations are satisfied (we explain them shortly):

- η
_{X}^{†}= id_{TX} - for every morphism
*f*:*X*→**T***Y*,*f*^{†}o η=_{X}*f* - for all morphisms
*f*:*X*→**T***Y*and*g*:*Y*→**T**Z, (*g*^{†}o*f*)^{†}=*g*^{†}o*f*^{†}.

We then say that (**T**, η, †) is a monad, or, by abuse of language, that **T** itself is a monad. Let’s illustrate that on a concrete example.

Consider the category **Set** of sets for the category **C**. The morphisms from *X* to *Y* are just the functions from *X* to *Y*. Let **T***X* be the powerset **P**(*X*) of *X*, that is, the set of all subsets of *X*. Define η* _{X}* as mapping

*x*in

*X*to {

*x*}, and for every set

*E*, let

*f*

^{†}(

*E*) be defined as the union of all the sets

*f*(

*x*),

*x*in

*E*. We check the monad equations as follows:

- η
_{X}^{†}maps*E*to the union of the sets {*x*},*x*in*E*, namely*E*, so η_{X}^{†}= id_{TX}; *f*^{†}o ηmaps every element x to_{X}*f*^{†}({*x*}) =*f*(*x*), hence is equal to*f*;- for every subset
*E*, (*g*^{†}o*f*)^{†}(*E*) is the union over all*x*in*E*of*g*^{†}(*f*(*x*)), namely the union over all*x*in*E*of the union over all*y*in*f*(*x*) of*g*(*y*). On the other hand, (*g*^{†}o*f*^{†}) (*E*) is the union over all*y*in*f*^{†}(*E*) of*g*(*y*), and that is just the same thing.

**The Kleisli category of a monad**

There is a very rich theory of monads. I would like to explain why the equations 1—3 above are what they are. The reason is the construction of the so-called *Kleisli category* **C _{T}** of the monad

**T**on

**C**.

This is built as follows. The objects of the **C _{T}** are the same as those of

**C**; the only thing that changes are the morphisms: the morphisms from

*X*to

*Y*in

**C**are exactly those from

_{T}*X*to

**T**

*Y*in the old category

**C**. The map η

*:*

_{X}*X*→

**T**

*X*serves as the identity morphism at

*X*in

**C**, and composition of

_{T}*f*:

*X*→

**T**

*Y*with

*g*:

*Y*→

**T**Z is given by

*g*

^{†}o

*f*:

*X*→

**T**

*Z*. The equations 1—3 are exactly what you need to show that this indeed forms a category: composition is associative, and the identity is neutral for composition both on the left and on the right. In fact, you can check that the Kleisli “category” is really a category if

*and only if*the equations 1—3 are satisfied.

In the case of the powerset monad on **Set**, the Kleisli category can be thought as a category of sets and *binary relations* as morphisms. Any binary relation *R* on *X* x* Y* defines a Kleisli morphism *f*: *X* → **P**(*Y*), which maps every *x* in *X* to the set {*y* in *Y* | (*x*, *y*) in *R*}. Conversely, every Kleisli morphism *f*: *X* → **P**(*Y*) defines a binary relation *R* by (*x*, *y*) in *R *if and only if *y* is in *f*(*x*). You can check that the Kleisli identity (the unit of the monad) is the equality relation {(*x*, *x*) | *x* in *X*}, and that Kleisli composition is the ordinary composition of relations: *S* o *R* = {(*x*, *z*) | (*x*, *y*) in *R* and (*y*, *z*) in *S* for some *y*}.

One can also think of the set *X* as a set of states for some computer system. A Kleisli morphism *f* from *X* to **T***Y* tells you, given that you are in some state *x* in *X*, what the set *f* (*x*) of successor states is. In other words, *f* is a so-called *transition relation*. The fact that *f*(*x*) may contain more than one element means that you can choose *y* non-deterministically.

Oh, before we examine the more complicated Hoare monad, recall that I had given another definition of monads in Filters IV. We obtain that presentation from a monad as defined above, as follows:

- a functor
**T**from**C**to**C**; we already have its object parts, and on morphisms*f*:*X*→*Y*, we define**T***f*:**T***X*→**T**Y as (ηo_{Y}*f*)^{†}(check, using 1—3, that this is indeed a functor!) - a natural transformation η from the identity functor to
**T**; this is given as ηon each object_{X}*X*(check, using 1—3, that this is indeed natural in*X*); - a natural transformation μ from
**T**^{2}to**T**, defined on each object*X*by μ= id_{X}_{TX}^{†}:**T**^{2}*X*→**T***X*(check, again, that this is natural); - all of these are also required to satisfied the three laws: (left unit) μ
o η_{X}_{TX}= id_{TX}, (right unit) μo_{X}**T**η_{X}= id_{TX}, and (associativity) μo_{X}**T**μ= μ_{X}o μ_{X}_{TX}. Again, I’ll let you check that those follow from 1—3.

Conversely, any monad as given by a functor, a unit natural transformation, and a multiplication natural transformation satisfying the left unit, right unit, and associativity laws yields back a monad (**T**, η, †) by defining *f*^{†} as μ* _{X}* o

**T**

*f*. The fancy names “left unit”, “right unit”, and “associativity” really come from the fact that monads on

**C**are exactly the monoid objects in the monoidal category of endofunctors of

**C**, with composition as tensor product. (Ignore that if this is your first time with monads, and think of it as some Zen koan: it is impenetrable, but it holds the truth.)

**The H monad**

We can now proceed with the more complicated case of the **H** powerspace construction. That this defines a monad is again due to Andrea Schalk [1]. We take **C**=**Top**, and let **T***X=***H**(*X*) with the upper (=lower Vietoris) topology.

We already have a continuous map η* _{X}*:

*X*→

**H**(

*X*), which sends

*x*in

*X*to the closure ↓

*x*of

*x*. This will be our unit.

Given any continuous map *f*: *X → ***H**(*Y*), we define *f*^{†}: **H**(* X*) →

**H**(

*Y*) by letting

*f*

^{†}(

*F*) be the

*closure*of the union of all the closed subsets

*f*(

*x*),

*x*in

*F*. We need to take the closure because a union of closed subsets may fail to be closed. What we have done here is taking a supremum in

**H**(

*Y*), ordered by inclusion: suprema are closures of unions. In summary,

*f*

^{†}(

*F*) = sup {

*f*(

*x*) |

*x*in

*F*}.

Let us check that this indeed defines a monad. This is somehow more complicated than for the powerset monad.

- To show that
*f*^{†}is continuous, we only have to show that the inverse image of ◊*V*, for*V*open in*Y*, is open in**H**(). Since the closure of a set intersects an open*X**V*if and only if the set itself intersects*V*(Corollary 4.1.28), that inverse image is ◊*f*^{-1}(◊*V*), and we are done.

We now turn to the monad equations.

- First, η
_{X}^{†}= id_{H(X)}. Indeed, the left hand side maps each closed set*F*to the closure of the union of all the sets ↓*x*,*x*in*F*. That union is just*F*, and since*F*is closed, its closure is itself. - Second, for every continuous map
*f*:*X →***H**(*Y*),*f*^{†}o*η*=_{X}*f*. The left hand side maps every*x*in*X*to the closure of the union of all the sets*f*(*x’*), where*x’*ranges over ↓*x*. Since*f*is continuous hence monotonic, every such set*f*(*x’*) is included in*f*(*x*), so (*f*^{†}o*η*) (_{X}*x*) is included in*f*(*x*); the converse inclusion is because*x*itself is in ↓*x*. - Third, for all continuous maps
*f*:*X →***H**(*Y*) and*g*:*Y →***H**(*Z*), we have two maps from**H**(*X*) to**H**(*Z*), namely (*g*^{†}o*f*)^{†}and*g*^{†}o*f*^{†}. We claim that they are equal: (*g*^{†}o*f*)^{†}=*g*^{†}o*f*^{†}… but if you try to prove this directly, you’ll suffer as hell. Instead, recall that for continuous*h*for which*h*^{†}makes sense, for every open subset*W*, (*h*^{†})^{-1}(◊*W*) = ◊*f*^{-1}(◊*W*): this is how we proved that*h*^{†}was continuous. Using that, we check that, for every open subset*W*of*Z*, the inverse image of ◊*W*by (*g*^{†}o*f*)^{†}and by*g*^{†}o*f*^{†}is the same, namely ◊*f*^{-1}(◊*g*^{-1}(◊*W*)). This is enough to conclude that (*g*^{†}o*f*)^{†}=*g*^{†}o*f*^{†}are identical, by Stone duality, and because**H**(*X*) is sober. We can also see that directly: for every closed subset*F*of*X*, for every open subset*W*of*Z*,*F*is in the inverse image of ◊*W*by (*g*^{†}o*f*)^{†}if and only if it is in in the inverse image of ◊*W*by*g*^{†}o*f*^{†}, that is, for every open subset*W*of*Z*, (*g*^{†}o*f*)^{†}(*F*) intersects*W*if and only if (*g*^{†}o*f*^{†}) (*F*) intersects*W*; hence they are equal closed sets.

Just like the powerset monad on **Set**, the Hoare monad **H** on **Top** can be thought as some kind of powerset, with extra topological information. As for the powerset monad, the Kleisli morphisms encode some form of non-deterministic choice, called *angelic* non-determinism. Let me postpone the explanation of that denomination, as I would prefer to explain a few things about *theories* of monads, and monad *algebras*… next time. We shall see that, in a precise sense, the theory of the **H** monad is given by the following axioms:

- (unit)
*a*∨ 0 =*a* - (associativity) (
*a*∨*b*) ∨*c*=*a*∨ (*b*∨*c*) - (commutativity)
*a*∨*b*=*b*∨*a* - (idempotence)
*a*∨*a*=*a* - (inflationary)
*a*≤*a*∨*b*

Note that, if you interpret ∨ as binary union of closed sets, 0 as the empty set, and ≤ as inclusion, then those (in)equalities are trivially satisfied. A topological space with a continuous map ∨ satisfying the above (in)equalities is called an inflationary semi-lattice. What we shall see is that, for each space *X*, **H**(*X*) is the free sober inflationary semi-lattice above *X*, as proved by Schalk [1]… and I’ll try to explain what this means.

— Jean Goubault-Larrecq (May 17th, 2015)

[1] Andrea Schalk. *Algebras for Generalized Power Constructions*. PhD Thesis, TU Darmstadt, 1993.