Commit 2024-07-01 22:27 cf6699f8

feat(CategoryTheory): if LR is abstractly isomorphic to the identity functor, then the unit is an isomorphism. (#14017) This PR proves that to show that the unit of an adjunction L ⊣ R is an isomorphism (i.e. that L is fully faithful), it is enough to give an arbitrary isomorphism L ⋙ R ≅ 𝟭 C, and the dual result. To do this, we give a general way to transport (co)monad structures on functors along isomorphisms of functors.