Commit 2022-11-03 01:01 51c07ea9
View on Github →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).
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).