Commit 2024-04-23 09:54 fe756d68
View on Github →feat(CategoryTheory/Adjunction): given an abstract isomorphism, the counit is an isomorphism (#12344) ... in case the left adjoint is fully faithful. We also give the dual result about the unit in case the right adjoint is fully faithful.