Strict 2-category

The concept of 2-category was first introduced by Charles Ehresmann in his work on enriched categories in 1965.

[1] The more general concept of bicategory (or weak 2-category), where composition of morphisms is associative only up to a 2-isomorphism, was introduced in 1968 by Jean Bénabou.

[2] A 2-category C consists of: The 0-cells, 1-cells, and 2-cells terminology is replaced by 0-morphisms, 1-morphisms, and 2-morphisms in some sources[3] (see also Higher category theory).

The axioms of a 2-category are consequences of their definition as Cat-enriched categories: The interchange law follows from the fact that

In mathematics, a doctrine is simply a 2-category which is heuristically regarded as a system of theories.

The distinction between a 2-category and a doctrine is really only heuristic: one does not typically consider a 2-category to be populated by theories as objects and models as morphisms.

For example, the 2-category Cat of categories, functors, and natural transformations is a doctrine.

As another example, one may take the subcategory of Cat consisting only of categories with finite products as objects and product-preserving functors as 1-morphisms.