mathlib

6e3516de - feat(category_theory/monad): monadic adjunctions (#1176)

feat(category_theory/monad): monadic adjunctions (#1176) * feat(category_theory/limits): equivalences create limits * equivalence lemma * feat(category_theory/monad): monadic adjunctions * move file * fix * add @[simp] * use right_adjoint_preserves_limits * fix * fix * undo weird changes in topology files * formatting * do colimits too * missing proofs * convert monad to a typeclass decorating a functor * changing name * cleaning up * oops * minor