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