Strict 2-category

A strict 2-category consists of a class of objects and, for every ordered pair $A,B$, a hom-category $\mathcal K(A,B)$ (Category, object, morphism, domain, codomain, identity, composition, and hom-collection). Objects of a hom-category are 1-morphisms and its morphisms are 2-morphisms.

There are identity 1-morphisms and horizontal-composition functors

$\mathcal K(B,C)\times\mathcal K(A,B)\longrightarrow\mathcal K(A,C)$

where the product and functor notions are those of Product category and its projection functors and Covariant functor, identity functor, composite functor, and contravariant functor. They are associative and unital as literal equalities. Because horizontal composition is functorial, it satisfies the interchange law with the vertical composition inside each hom-category. The adjective strict refers to these equalities rather than coherent isomorphisms.