Definition 1.4 (Functor). Let C and D be categories. A functor F:CD consists of mappings F:obCobD and F+morCmorD such that:

  • F(domf)=domFf

  • F(codf)=codFf

  • F(1A)=1FA

  • F(fg)=(Ff)(Fg) whenever fg is defined.

We write Cat for the category of small categories and the functors between them.