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/ ]