In category theory, a 2-category is a category with "morphisms between morphisms"; that is, where each hom-set itself carries the structure of a category. It can be formally defined as a category enriched over Cat (the category of categories and functors, with the monoidal structure given by product of categories).
A 2-category C consists of:
The notion of 2-category differs from the more general notion of a bicategory in that composition of 1-cells (horizontal composition) is required to be strictly associative, whereas in a bicategory it needs only be associative up to a 2-isomorphism. The axioms of a 2-category are consequences of their definition as Cat-enriched categories:
The interchange law follows from the fact that is a functor between hom categories. It can be drawn as a pasting diagram as follows:
Here the left-hand diagram denotes the vertical composition of horizontal composites, the right-hand diagram denotes the horizontal composition of vertical composites, and the diagram in the centre is the customary representation of both.
In mathematics, a doctrine is simply a 2-category which is heuristically regarded as a system of theories. For example, algebraic theories, as invented by Lawvere, is an example of a doctrine, as are multi-sorted theories, operads, categories, and toposes.