nLab single-sorted definition of categories




There are two common ways to define a category:

  1. As a collection C 0C_0 of objects and a collection C 1C_1 of morphisms, together with source and target maps C 1C 0C_1\to C_0, a composition map C 1× C 0C 1C 1C_1\times_{C_0} C_1\to C_1, and an identity assigning map C 0C 1C_0\to C_1, satisfying axioms.

  2. As a collection C 0C_0 of objects, together with for each pair x,yx,y of objects, a collection hom C(x,y)hom_C(x,y) of morphisms, together with identities 1 xhom C(x,x)1_x\in hom_C(x,x) and composition maps hom C(y,z)×hom C(x,y)hom C(x,z)hom_C(y,z)\times hom_C(x,y)\to hom_C(x,z), satisfying axioms.

In logical terms, the first is formulated as a 22-sorted theory in first-order logic, while the second is a dependently typed theory; the usual way of interpreting any dependently typed theory as an independently sorted theory turns the latter into the former.

However, there is a third way of defining a category which uses only one collection (representing the collection of morphisms) and thus is formulated as an untyped (or 11-sorted) first-order theory. Note that this is not the usual way of replacing sorts with predicates, but instead a slightly clever trick. The basic idea is that an object can be identified with its identity morphism. This reformulation is occasionally useful, but mostly for technical reasons.


A category (single-sorted version) is a collection CC, whose elements are called morphisms, together with two functions s,t:CCs,t:C\to C and a partial function :C×CC\circ:C\times C\to C, such that:

  1. s(s(x))=s(x)=t(s(x))s(s(x)) = s(x) = t(s(x))
  2. t(t(x))=t(x)=s(t(x))t(t(x)) = t(x) = s(t(x))
  3. xyx\circ y is defined if and only if s(x)=t(y)s(x)=t(y).
  4. If xyx\circ y is defined, then s(xy)=s(y)s(x\circ y) = s(y) and t(xy)=t(x)t(x\circ y)=t(x).
  5. xs(x)=xx\circ s(x)=x and t(x)x=xt(x)\circ x=x (both composites are always defined, because of the first two axioms)
  6. (xy)z=x(yz)(x\circ y)\circ z = x\circ (y\circ z), if either is defined (in which case the other is defined by the axiom 3).

The first two axioms say that ss and tt are idempotent endofunctions on CC which have the same image. The elements of their common image (the xx such that s(x)=xs(x)=x, or equivalently t(x)=xt(x)=x) are called identities or objects. Once that is done, the rest of the identification is straightforward.

A functor between single-sorted categories is just a function f:CDf:C\to D such that f(s(x))=s(f(x))f(s(x)) = s(f(x)), f(t(x))=t(f(x))f(t(x)) = t(f(x)), and f(xy)=f(x)f(y)f(x\circ y)= f(x)\circ f(y) whenever xyx\circ y is defined (which, by the first two axioms of a functor and axiom (3) of a category, implies that f(x)f(y)f(x)\circ f(y) is defined).

Finally, a natural transformation between functors f,g:CDf,g:C\to D of single-sorted categories is a function α:CD\alpha:C\to D such that s(α(x))=s(f(x))s(\alpha(x)) = s(f(x)), t(α(x))=t(g(x))t(\alpha(x)) = t(g(x)), and α(x)f(y)=g(x)α(y)\alpha(x) \circ f(y) = g(x) \circ \alpha(y) whenever xyx\circ y is defined (which implies that both composites in this identity are defined). Note that while a natural transformation is ordinarily defined to consist of a component α(x)\alpha(x) only when xx is an object, this definition supplies a component to each morphism. In terms of the usual definition, the component of α\alpha at a morphism is the diagonal of the corresponding naturality square.

It can now be proved that single-sorted categories, functors, and natural transformations form a 2-category which is (strictly) equivalent to the usual 22-category Cat.



A monoid is a single-sorted category in which ss is a constant function (hence so is tt, and they are equal). This works up to isomorphism of categories, not merely equivalence, so single-sorted categories may seem to be a more direct oidification of monoids than the usual categories.


The usual definition of an internal category is two-sorted, but the one-sorted definition can also be interpreted internally. While the usual notion of internal category requires the ambient category only to have pullbacks, the one-sorted version appears to require one to make sense of an “internal partial binary operation.” However, since in this case the domain of \circ is specified explicitly in the definition, one can just require \circ to be an ordinary morphism whose domain is the pullback of ss and tt; thus only pullbacks are required for the single-sorted definition as well.

It is easy to see that any internal two-sorted category gives an internal one-sorted category (consider the object of arrows). The converse is true as long as the ambient category has split idempotents, for then given an internal one-sorted category we can split either ss or tt to obtain an object of objects. In general, however, the two concepts are not equivalent.


There exist similar single-sorted definitions of nn-categories and ∞-categories. The single sort in the definition of nn-category is the set of nn-morphisms, but you can also think of this as the union (over all knk \leq n) of the sets of kk-morphisms, as long as you identify each kk-morphism (for k<nk \lt n) with its identity (k+1)(k+1)-morphism. In the the definition of \infty-category, there is no notion of \infty-morphism to take care of everything at once, but the single sort can still be understood as this union (now over all kk).


Last revised on May 20, 2023 at 08:33:47. See the history of this page for a list of all contributions to it.