chore(category_theory/monad): comonadic adjunction (#5770)
Defines comonadic adjunctions dual to what's already there
Co-authored-by: Oliver Nash <oliver.nash@gmail.com>
Co-authored-by: leanprover-community-bot <leanprover.community@gmail.com>
Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: tb65536 <tb65536@uw.edu>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Mohamed Al-Fahim <malfahim8@gmail.com>
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
