A forget₂ C D forgetful functor between concrete categories C and D
whose forgetful functors both reflect isomorphisms, itself reflects isomorphisms.
instance
CategoryTheory.instReflectsIsomorphismsForgetType :
(CategoryTheory.forget (Type u)).ReflectsIsomorphisms
theorem
CategoryTheory.reflectsIsomorphisms_forget₂
(C : Type (u + 1))
[CategoryTheory.Category.{u_1, u + 1} C]
[CategoryTheory.ConcreteCategory C]
(D : Type (u + 1))
[CategoryTheory.Category.{u_2, u + 1} D]
[CategoryTheory.ConcreteCategory D]
[CategoryTheory.HasForget₂ C D]
[(CategoryTheory.forget C).ReflectsIsomorphisms]
:
(CategoryTheory.forget₂ C D).ReflectsIsomorphisms
A forget₂ C D forgetful functor between concrete categories C and D
where forget C reflects isomorphisms, itself reflects isomorphisms.