An equational notion of lifting monad (Q1398461)

The underlying idea of the categorical approach to denotational semantics is to make a denotational distinction between the operational notions of value and computation by modeling them in two separate categories, namely, the category of values and the category of computations, which is obtained as the Kleisli category of a strong monad on the category of values. This paper identifies the properties a strong monad must possess in order for its Kleisli category to behave like an induced category of partial maps. The authors introduce the notion of an equational lifting monad, which is a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). The main result of the paper is that any equational lifting monad has a representation by a partial map classifier such that the Kleisli category of the former fully embeds in the partial category of the latter.