Category with domain/codomain relations

Question

This question is going to be a bit rambling; for those who just want the essence of it, please see the definition in the middle of the post and the question at the end.

---

After some recent discussion in the MO comments on a separate question, it became apparent that the 'one hom-class' definition of a category gives the wrong intuition for 'what a category looks like in nature' if taken together with domain and codomain functions, since this immediately gives a category with disjoint hom-classes and consequently very canonical things like the 'EM-category of a monad' fail to actually be categories - they have arrows with multiple domains/codomains. It is always possible to consider arrows as triplets with specified domains and codomains, but this feels very 'clunky'.

For type theorists this issue is easily resolved by pointing out that the 'hom-class for each pair of objects' typed definition of a category 'matches nature', so EM-categories are categories by their definition, and there is a $2$-equivalence (not an isomorphism) between the $2$-categories consisting of categories by either definition with appropriately defined notions of functor for each (the same notion of natural transformation works for both), so working with disjoint hom-classes is okay 'up to equivalence'. (This is distressing to me because disjoint hom-classes dramatically simplify some arguments in a way that feels like cheating, but that's a topic for another question.)

As someone who uses set theory for a foundation very comfortably and is uncomfortable with type theory foundationally, I wanted to find a 'non-typed' definition of a category that 'matched nature' and gave the correct intuition for how to reason about/inside them -- I found the notion of a protocategory after a little web searching, but it seemed very unsatisfactory for the purposes of doing actual category theory.

Seeing as the only real 'problem' with the 'non-typed definition' is that the domain and codomain notions being formalized as functions (total functional relations) gives rise to disjoint hom-classes, I figured we could just drop the requirement that these relations be functional and see how the remaining structure matched nature.

Definition A category $\mathcal{C}$ consists of

1. A class of objects, denoted ${\bf Ob}_\mathcal{C}$, whose members are denoted by capital roman letters from the end of the alphabet $X,Y,Z,\dots$.
2. A class of arrows, denoted ${\bf Hom}_\mathcal{C}$, whose members are denoted by lowercase roman letters from the middle of the alphabet $f,g,h,\dots$.
3. Entire relations $dom,cod:{\bf Hom}_\mathcal{C}\leftrightarrow{\bf Ob}_\mathcal{C}$, which specify a subset ${\bf Com}_\mathcal{C}\subseteq{\bf Hom}_\mathcal{C}\times{\bf Hom}_\mathcal{C}$ given by $${\bf Com}_\mathcal{C}=\{(f,g)\in{\bf Hom}_\mathcal{C}\times{\bf Hom}_\mathcal{C}:dom(f)\cap cod(g)\neq\emptyset\}.$$
4. A function $1:{\bf Ob}_\mathcal{C}\to{\bf Hom}_\mathcal{C}$.
5. A function $\circ:{\bf Com}_\mathcal{C}\to{\bf Hom}_\mathcal{C}$.

We write $1(X)=1_X$ and $\circ(f,g)=f\circ g$. These classes, relations and functions satisfy the following axioms for all $X\in{\bf Ob}_\mathcal{C}$ and $(f,g)\in{\bf Com}_\mathcal{C}$:

1. $X\in cod(1_X)\cap dom(1_X),$
2. $dom(f\circ g)=dom(g),$
3. $cod(f\circ g)=cod(f),$
4. $\forall Y\in cod(g)\big(1_Y\circ g=g\big),$
5. $\forall Y\in dom(f)\big(f\circ 1_Y=f\big),$
6. $(f\circ g)\circ h=f\circ(g\circ h).$

For any two objects $X,Y\in{\bf Ob}_\mathcal{C}$ we define the subclass ${\bf Hom}_\mathcal{C}(X,Y)\subseteq{\bf Hom}_\mathcal{C}$ as $${\bf Hom}_\mathcal{C}(X,Y)=\{f\in{\bf Hom}_\mathcal{C}:X\in dom(f)\wedge Y\in cod(f)\}.$$

The standard 'one hom-class' definition of a functor works for this definition of category, where we interpret the axioms $$F(dom(f))=dom(F(f))$$ $$F(cod(f))=cod(F(f))$$ as statements about classes instead of elements. This seems to suffice for the standard usage of those axioms, which serve essentially to guarantee compositionally of the image of composable arrows under a functor.

This definition seems to do the trick for matching what categories look like in nature, and we have an actual $2$-isomorphism between the $2$-category of these categories and the typed-definition categories: we pass back and forth simply by forming hom-classes as above to obtain the typed-definition from the one hom-class definition, or begin with the typed one and form the union of its hom-classes then define the domain and codomain relations by $$dom=\{(f,X):\exists Y(f\in{\bf Hom}_\mathcal{C}(X,Y)\},$$ $$cod=\{(f,Y):\exists X(f\in{\bf Hom}_\mathcal{C}(X,Y)\}.$$

This seems more natural than the $2$-equivalence described on the nlab between the 'domain/codomain functions' definition of a category and the typed definition, where we form a disjoint union of the hom-classes from the typed definition to get to the 'domain/codomain functions' definition and we have to use the triplets trick to move in the other direction.

This also allows for more natural definition of categories like ${\bf Set}$; we can say that the morphisms are functions, the domain relation is actually a function sending a function to its domain, and the codomain relation assigns a function to all supersets of its image. There are other categories that are more naturally presented using the typed definition, but it seems like the 'domain/codomain functions' definition is ultimately less natural than the other two (made explicit by the fact that the typed definition and this one are isomorphic as $2$-categories, while the 'domain/codomain functions' definition is only equivalent).

In light of all of this, the disjoint hom-classes definition actually feels like a 'strictification' of the other definitions, allowing for easier arguments etc. which are 'guaranteed to be safe' because we know that the place we're working is equivalent to the place we really care about, similar to strictification for $2$/$3$-categories allowing us to work in a $2$-category/Gray category when we really care about a bicategory/tricategory. My question is:

Has this notion appeared in the literature anywhere?

I'm sure the founders of the theory were aware of this business with disjoint hom-classes, but from what I can find it seems like 'protocategories' were what was viewed as the 'set theoretical fix' to the issue (immediately and appropriately discarded as unwieldy), whereas this fix requires almost no effort in tweaking other definitions and fixes the problem 'set theoretically'.

I'm primarily interested in reading more about it to make sure there aren't any pitfalls waiting down the line using this definition; in no sense do I think this is any kind of 'contribution', just bookkeeping. Any references are appreciated.

Answer 1

This doesn't work. In particular,

we have an actual 2-isomorphism between the 2-category of these categories and the typed-definition categories: we pass back and forth simply by forming hom-classes as above to obtain the typed-definition from the one hom-class definition, or begin with the typed one and form the union of its hom-classes then define the domain and codomain relations by [...]

is false. Since you didn't give them a separate name, I'll call the things you defined using entire relations "categories" to distinguish them from the usual notion.

---

Example: Let $C$ be the "category" with three objects $a$, $b$, $c$, their identity morphisms, and two (nonidentity) morphisms $f : a \to c$, $g : b \to c$. Let $D$ be the "category" with the same objects but only a single nonidentity morphism $h$, which can be viewed as either $h : a \to c$ or $h : b \to c$. So $C$ and $D$ both have a single morphism from $a$ to $c$ and a single morphism from $b$ to $c$, but in $C$ these are different morphisms while in $D$ they are the same morphism.

I will write $U$ for your functor which turns a "category" into a standard (typed) category by forming the hom-sets as you describe. There is a unique isomorphism $G : UC \to UD$ such that $Ga = a$, $Gb = b$ and $Gc = c$. If $U$ is supposed to be an equivalence then there should also be a (unique) isomorphism $F : C \to D$ of "categories" such that $UF = G$. But $C$ and $D$ aren't isomorphic--one has a total of 5 morphisms and the other only 4.

---

The key point is that the "overlappiness" of different hom-sets in a typed category is not part of the structure of a category. (If you like, this is because the action of a functor on morphisms consists of separate functions $\mathrm{Hom}_C(X, Y) \to \mathrm{Hom}_D(FX, FY)$ which are (importantly!!) not required to agree in the situation that by accident $f \in \mathrm{Hom}_C(X, Y)$ and also $f \in \mathrm{Hom}_C(X', Y')$.) Consequently,

begin with the typed one and form the [literal set-theoretic] union of its hom-classes

is not a functorial or isomorphism-invariant operation and so it cannot be inverse to the operation $U$.

---

You can still introduce a notion like this, of course, but to avoid confusion it would be better not to call or think of these objects as categories, but rather some related kind of objects.