the obvious monadic adjoint

Stream: Is there code for X?

[Adam Topaz]

Am I missing an import, or is this instance really missing?

import category_theory.monad.adjunction

open category_theory

variables {C : Type*} [category C] (F : monad C)

example : monadic_right_adjoint F.forget := by apply_instance -- fails

[Adam Topaz]

Ping @Bhavik Mehta

[Bhavik Mehta]

You're right! I think I'd noticed this before and found that it was easier to show if monads were bundled, so I made that PR and then forgot to add this too :| I'll make a fresh PR for it now

[Adam Topaz]

No rush! (Isn't it ~3am where you are?)

[Bhavik Mehta]

That hasn't stopped me before!