Of course along with 2-categories, we must have 2-functors to map from one to another.
So, what’s a 2-functor? Since we defined a 2-category as a category enriched over , a 2-functor should be a functor enriched over . That is, it consists of a function on objects and a functor for each hom-category, each of which consists of a function on 1-morphisms (the objects of the hom-category) and a function for each set of 2-morphisms. Then there are a bunch of relations.
Let’s expand this a bit. A 2-category has a collection of objects, a collection of 1-morphisms for each pair of objects, and a collection of 2-morphisms for each pair of 1-morphisms between the same pair of objects. And all the same remarks go for another 2-category .
So a 2-functor has
- a function
- for each pair of objects of , a functor , each consisting of
- a function
- for each pair of 1-morphisms from to a function
Now the composition functors give us functions for composing 1-morphisms and “horizontally” composing 2-morphisms, and the hom-categories give us functions for “vertically” composing 2-morphisms. For each object we have an identity 1-morphism, and for each 1-morphism we have an identity 2-morphism. A 2-functor will preserve all these structures. First of all, since there are functors between the hom-categories the vertical composition is preserved, along with the identity 2-morphisms. The diagrams for enriched functors say that the identity 1-morphisms, the composition of 1-morphisms, and the horizontal composition of 2-morphisms are all preserved.