A forget₂ C D forgetful functor between concrete categories C and D
whose forgetful functors both reflect isomorphisms, itself reflects isomorphisms.
instance
CategoryTheory.reflectsIsomorphisms_forget₂
(C : Type u_1)
[Category.{v_1, u_1} C]
{FC : outParam (C → C → Type t₁)}
{CC : outParam (C → Type w)}
[outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
[ConcreteCategory C FC]
(D : Type u_2)
[Category.{v_2, u_2} D]
{FD : outParam (D → D → Type t₂)}
{CD : outParam (D → Type w)}
[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.