Kleisli category of the lift monad

[jonsterling]

Developing this properties of this category, including its algebraic compactness (which remains conjectural in a constructive setting as far as I am concerned, but seems plausible) will be important for connecting this work to Axiomatic Domain Theory and thence to Synthetic Domain Theory.

Just to remember, unlike in classical domain theory, here we will not expect the Kleisli category of the lift monad to be equivalent to the Eilenberg-Mac Lane category.