We introduce the notion of an equational lifting monad: a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). We prove 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. Thus, equational lifting monads precisely capture the equational properties of partial maps as induced by partial map classifiers. The representation theorem also provides a tool for transferring non-equational properties of partial map classifiers to equational lifting monads. It is proved using a direct axiomatization of Kleisli categories of equational lifting monads. This axiomatization is of interest in its own right.
An equational notion of lifting monad / A. Bucalo, C. Fuehrmann, A. Simpson. - In: THEORETICAL COMPUTER SCIENCE. - ISSN 0304-3975. - 294:1-2(2003), pp. 31-60.
An equational notion of lifting monad
A. BucaloPrimo
;
2003
Abstract
We introduce the notion of an equational lifting monad: a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). We prove 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. Thus, equational lifting monads precisely capture the equational properties of partial maps as induced by partial map classifiers. The representation theorem also provides a tool for transferring non-equational properties of partial map classifiers to equational lifting monads. It is proved using a direct axiomatization of Kleisli categories of equational lifting monads. This axiomatization is of interest in its own right.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.