2
$\begingroup$

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$?

$\endgroup$

1 Answer 1

3
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .