A forget₂ C D forgetful functor between concrete categories C and D whose forgetful functors both reflect isomorphisms, itself reflects isomorphisms.

instance CategoryTheory.instReflectsIsomorphismsTypeTypesForgetTypes : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget (Type u))

Equations

• CategoryTheory.instReflectsIsomorphismsTypeTypesForgetTypes = ⋯

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.ReflectsIsomorphisms (CategoryTheory.forget C)] : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget₂ C D)

A forget₂ C D forgetful functor between concrete categories C and D where forget C reflects isomorphisms, itself reflects isomorphisms.