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.{v_1, u + 1} C]
{FC : outParam (C → C → Type u)}
{CC : outParam (C → Type u)}
[outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
[ConcreteCategory C FC]
(D : Type (u + 1))
[Category.{v_2, u + 1} D]
{FD : outParam (D → D → Type u)}
{CD : outParam (D → Type u)}
[outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))]
[ConcreteCategory D FD]
[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.