Decidability of the theory of a monad

[Andrej Bauer <andrej.bauer@andrej.com>]

Consider the theory of a monad, i.e., the axioms are those of a
category and a monad given as a triple: an operation T on objects, for
each object A a morphism eta_A : A -> T A, and an operation lift_{A,B}
which maps morphisms f : A -> T B to lift f : T A -> T B. Concretely,
the axioms are (where lift f is written f* and composition is
juxtaposition):

id f = f
f id = f
(f g) h = f (g h)
eta* = id
f* eta = f
(f* g)* = f* g*

Presumably, the equational theory (with partial operations) of such a
triple is decidable. Is this known? If we ignore the types and
partiality, we can attempt to turn the above equations into a
confluent terminating rewrite system using the Knuth-Bendix algorithm,
but it gets stuck (on various orderings I tried).

A more categorical way of asking the same question is: what is a
concrete description of the free "monad on a category" (is this the
same as  "free monad" on "free category"?).

With kind regards,

Andrej


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]