Documentation

Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso

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