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

2
$\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$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.