functor C D represents a functor between categories C and D.

To apply a functor F to an object use F.obj X, and to a morphism use F.map f.

The axiom map_id_lemma expresses preservation of identities, and map_comp_lemma expresses functoriality.

𝟭 C is the identity functor on a category C.

F ⋙ G is the composition of a functor F and a functor G (F first, then G).