Commit 2024-07-08 20:11 c2853f31
View on Github →feat(CategoryTheory/Adjunction): left adjoint is faithful iff unit is mono, etc. (#14490) We prove the full Lemma 4.5.13 in Riehl's Category Theory in Context, characterizing when a left/right adjoint is full, resp. faithful, resp fully faithful in terms of the unit/counit being various types of epi/mono/iso. Earlier we only had the statements for fully faithful functors.