# Well-behaved monad quotients

Reading through Modular specification of monads through higher-order presentations, this paper includes the following lemma within set-truncated homotopy type theory:

Given a monad $$R$$ (they work on the type-theoretic universe $$Set$$) preserving epimorphisms and a collection of monad morphisms $$(f_i : R → S_i)_{i\in I}$$ , there exists a quotient monad $$R/(f_i)$$ together with a projection $$p^R : R → R/(f_i)$$, which is a morphism of monads such that each $$f_i$$ factors through $$p$$.

For further context, they form a relation from the monad morphisms $$f_i$$, let's call it $$q$$, which they quotient by.

What is known about the following related statement failing:

For a monad $$R$$ (on a category $$C$$) preserving epimorphisms given a relation $$q$$, taking a quotient of the underlying structure of $$R$$ by $$q$$, the quotient monad exists.

Is there a succint generalization of, $$q$$ being formed by monad morphisms to $$q$$ formed by some other morphisms(?), such that the quotient turns out to be monad? Are there any other sufficient conditions on $$q$$ known? Are there sufficient and necessary conditions if we assume some properties of $$C$$?

## 1 Answer

Steve Lack's paper On the monadicity of finitary monads shows that if $$C$$ is locally finitely presentable, then the category of finitary monads on $$C$$ is monadic over a power of $$C$$. Since monadic functors create certain coequalizers (this is part of the monadicity theorem), it follows that in these circumstances, a certain sort of "quotient" of the "underlying structure" of a finitary monad can be given a monad structure making it a quotient monad.