A forget₂ C D forgetful functor between concrete categories C and D
whose forgetful functors both reflect isomorphisms, itself reflects isomorphisms.
@[protected, instance]
theorem
category_theory.reflects_isomorphisms_forget₂
(C : Type (u+1))
[category_theory.category C]
[category_theory.concrete_category C]
(D : Type (u+1))
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.has_forget₂ C D]
[category_theory.reflects_isomorphisms (category_theory.forget C)] :
A forget₂ C D forgetful functor between concrete categories C and D
where forget C reflects isomorphisms, itself reflects isomorphisms.