Functors which reflect isomorphisms #
F reflects isomorphisms if whenever
F.map f is an isomorphism,
f was too.
It is formalized as a
Prop valued typeclass
Any fully faithful functor reflects isomorphisms.
F.map fis an iso, then so was
Define what it means for a functor
F : C ⥤ D to reflect isomorphisms: for any
f : A ⟶ B, if
F.map f is an isomorphism then
f is as well.
Note that we do not assume or require that
F is faithful.
F reflects isos and
F.map f is an iso, then
f is an iso.