A functor F : C ⥤ D is full if for each X Y : C, F.map is surjective. In fact, we use a constructive definition, so the full F typeclass contains data, specifying a particular preimage of each f : F.obj X ⟶ F.obj Y.

A functor F : C ⥤ D is faithful if for each X Y : C, F.map is injective.

The specified preimage of a morphism under a full functor.

If F : C ⥤ D is fully faithful, every isomorphism F.obj X ≅ F.obj Y has a preimage.

Alias of faithful.of_comp_eq.

“Divide” a functor by a faithful functor.