# Strict 2-category

In category theory, a **strict 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).

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 discovered in 1968 by Jean BĂ©nabou.^{[2]}

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:

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 William Lawvere, is an example of a doctrine, as are multi-sorted theories, operads, categories, and toposes.

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. It is this vocabulary that makes the theory of doctrines worth while.

For example, the 2-category **Cat** of categories, functors, and natural transformations is a doctrine. One sees immediately that all presheaf categories are categories of models.

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. This is the doctrine of multi-sorted algebraic theories. If one only wanted 1-sorted algebraic theories, one would restrict the objects to only those categories that are generated under products by a single object.