Category of adjunctions inducing a fixed monad (source code)

= Category of adjunctions inducing a fixed monad

Fix a <monad> on $\mathcal C$. Objects are <adjunctions> with left-hand <category> $\mathcal C$ whose induced monads are identified with the fixed monad. A <morphism> between two such adjunctions is a <functor> between their right-hand <categories> commuting with both adjoints and respecting the specified units and counits. Strict identifications give a <category>; coherent identifications give the analogous <universal property> up to compatible <natural isomorphism>.