mathlib documentation

category_theory.concrete_category.reflects_isomorphisms

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

@[instance]

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