mathlib

51c07ea9 - feat(category_theory): nat_trans.equiv_of_comp_fully_faithful (#17304)

feat(category_theory): nat_trans.equiv_of_comp_fully_faithful (#17304) If `H` is a fully faithful functor, there are bijections `(F ⟶ G) ≃ (F ⋙ H ⟶ G ⋙ H)` and `(F ≅ G) ≃ (F ⋙ H ≅ G ⋙ H)`.