There are two common ways to define a category:
As a collection $C_0$ of objects and a collection $C_1$ of morphisms, together with source and target maps $C_1\to C_0$, a composition map $C_1\times_{C_0} C_1\to C_1$, and an identity assigning map $C_0\to C_1$, satisfying axioms.
As a collection $C_0$ of objects, together with for each pair $x,y$ of objects, a collection $hom_C(x,y)$ of morphisms, together with identities $1_x\in hom_C(x,x)$ and composition maps $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 $2$-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 $1$-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 $C$, whose elements are called morphisms, together with two functions $s,t:C\to C$ and a partial function $\circ:C\times C\to C$, such that:
The first two axioms say that $s$ and $t$ are idempotent endofunctions on $C$ which have the same image. The elements of their common image (the $x$ such that $s(x)=x$, or equivalently $t(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:C\to D$ such that $f(s(x)) = s(f(x))$, $f(t(x)) = t(f(x))$, and $f(x\circ y)= f(x)\circ f(y)$ whenever $x\circ y$ is defined (which, by the first two axioms of a functor and axiom (3) of a category, implies that $f(x)\circ f(y)$ is defined).
Finally, a natural transformation between functors $f,g:C\to D$ of single-sorted categories is a function $\alpha:C\to D$ such that $s(\alpha(x)) = s(f(x))$, $t(\alpha(x)) = t(g(x))$, and $\alpha(x) \circ f(y) = g(x) \circ \alpha(y)$ whenever $x\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 $\alpha(x)$ only when $x$ 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 $2$-category Cat.
A monoid is a single-sorted category in which $s$ is a constant function (hence so is $t$, 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 $s$ and $t$; 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 $s$ or $t$ to obtain an object of objects. In general, however, the two concepts are not equivalent.
There exist similar single-sorted definitions of $n$-categories and ∞-categories. The single sort in the definition of $n$-category is the set of $n$-morphisms, but you can also think of this as the union (over all $k \leq n$) of the sets of $k$-morphisms, as long as you identify each $k$-morphism (for $k \lt n$) with its identity $(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 $k$).
Last revised on May 20, 2023 at 08:33:47. See the history of this page for a list of all contributions to it.