Missing axiom in the typed definition of a category?

Question

$\newcommand\bHom{\mathbf{Hom}}\newcommand\bOb{\mathbf{Ob}}\newcommand\bRel{\mathbf{Rel}}$This question is probably stupid and definitely bureaucratic, but

Is writing $f\circ g$ for the composition of morphisms in the ‘many hom-classes’ definition of a category unambiguous?

The ‘many hom-classes’ definition of a category (as given e.g. on the nlab) says that for each pair of arrows $(f,g)\in\bHom_\mathcal{C}(Y,Z)\times\bHom_\mathcal{C}(X,Y)$ we ‘have an arrow’ $f\circ g\in\bHom_\mathcal{C}(X,Z)$, but if the hom-classes may not be disjoint how do we know that the arrows we ‘have’ from identical composable arrow pairings in differing hom-class pairs match up?

Rephrased using the language of composition functions, the above definition is the same as a collection of functions $$\{\circ_{XYZ}:\bHom_\mathcal{C}(Y,Z)\times\bHom_\mathcal{C}(X,Y)\to\bHom_\mathcal{C}(X,Z)\}_{X,Y,Z\in\bOb_\mathcal{C}}.$$ The axioms then specify associativity and unitarity, but how do we know that we don't have objects $X,Y,Z,X',Y',Z'\in\bOb_\mathcal{C}$ and arrows $$f\in\bHom_\mathcal{C}(Y,Z)\cap\bHom_\mathcal{C}(Y',Z'), \\ g\in\bHom_\mathcal{C}(X,Y)\cap\bHom_\mathcal{C}(X',Y'),$$ so $$(f,g)\in\bigl(\bHom_\mathcal{C}(Y,Z)\times\bHom_\mathcal{C}(X,Y)\bigr)\cap\bigl(\bHom_\mathcal{C}(Y',Z')\times\bHom_\mathcal{C}(X',Y')\bigr),$$ such that $$\circ_{XYZ}(f,g)\neq\circ_{X'Y'Z'}(f,g)?$$ Note that these composites live in $\bHom_\mathcal{C}(X,Z)$ and $\bHom_\mathcal{C}(X',Z')$, respectively, and as David Roberts points out in the comments these classes can be disjoint even if the original hom-classes aren't.

If it is possible to have objects and arrows as above the notation $f\circ g$ is obviously ambiguous — also obvious is that we could fix this with an additional axiom (scheme?) if it were a problem.

Is this situation already precluded by the other axioms/data present in the many hom-classes definition of a category?

---

For an example where we have identical arrow pairings in differing hom-classes but composition still matches up, consider any two composable relations $R,S\in\bOb_{\bRel}$. By definition $R$ and $S$ are subsets of some Cartesian squares $Y\times Z$ and $X\times Y$ (respectively), but we can take $X'$, $Y'$, $Z'$ to be any strict superclasses of $X$, $Y$, $Z$ (respectively) and observe that $R$ and $S$ are also subsets of $Y'\times Z'$ and $X'\times Y'$ (respectively), so $$R\in\bHom_{\bRel}(Y,Z)\cap\bHom_{\bRel}(Y',Z'), \\ S\in\bHom_{\bRel}(X,Y)\cap\bHom_{\bRel}(X',Y').$$ Here we obviously still have that the composition functions coincide, but this is arguably due to the fact that $\bRel$ is most naturally presented as a one hom-class category. Again, I understand that this question is very pedantic at best — the patience involved in any clarification is greatly appreciated.

Answer 1

There is no missing axiom. The notation is potentially ambiguous, but rarely (if ever) so in practice.

The situation is just the same as writing addition in arbitrary abelian groups as $x + y$. Formally, the operation “$+$” depends not just on $x,y$ but (before them) on a choice of group $G$ — explicitly, we could write it as $x +_G y$. And so the notation $x+y$ can potentially be ambiguous — $x$ and $y$ could belong to two different Abelian groups, whose addition operations disagree on $x+y$. But it would be nonsense to suggest that algebraists need to assume different groups considered must always be disjoint, or that their addition must always agree on intersections. We simply agree that the notation $x + y$ implicitly depends on the intended group, and make sure that this is always clear from context. And in the very rare situations where ambiguity would arise, we distinguish it explicitly by writing $+_G$ or some similar annotation. Similarly, composition $f \circ g$ is formally also dependent on the category and objects involved, $\mathrm{comp}(\mathcal{C},X,Y,Z,f,g)$ (so for a fixed category, it is a function of the objects and arrows) — but in the notation, we usually write just $f \circ g$, with the rest inferred from context.

This notational point is formally addressed in computer proof assistants, where functions have implicit arguments. This is essential for formalising many notations used in mathematical practice. In particular, the many-hom-sets definition of categories has been formalised by multiple authors many times (including myself), and shown equivalent to the class-of-arrows definition for instance here, in the TypeTheory Coq library over UniMath. So we can be very confident that there is no missing axiom.

(Counter to Duchamp Gérard’s answer, I do not think all (or even most) category theorists assume hom-sets are always disjoint. What I think all agree is that if we start from the many-hom-sets definition, then “the class of all arrows of $C$” must mean the disjoint union of the hom-sets, not the pure set-theoretic union. But when working with the many-hom-sets definition, the “class of all arrows” is not taken as primary — it is fairly rarely used, and when it’s used, there’s no problem with the original hom-sets being sub-objects of it rather than literal set-theoretic subsets.)

(Also, as Andreas Blass and Simon Henry note in comments, if we’re working in a type-theoretic or structural set-theoretic foundation, then asking if abstract sets are disjoint is not even well-defined. Intersection is defined between subsets of any given set/type; but in structural foundations, abstract sets not automatically subsets of an ambient universal class.)

Answer 2

$\newcommand\dom{\mathit{dom}}\newcommand\codom{\mathit{codom}}\newcommand\Ar{\mathit{Ar}}\newcommand\Ob{\mathit{Ob}}\newcommand\Hom{\mathit{Hom}}\newcommand\bHom{\mathbf{Hom}}\newcommand\vertex{\mathit{vert}}\newcommand\edge{\mathit{edge}}$As far as I know, it is clear in the mind of every category theorists (at least, the ones of my acquaintance and in founding texts as [5]) that, a category $\mathcal{C}$ comes with the usual axioms and two (mono-valued) maps $\dom$, $\codom$ from the class $\Ar(\mathcal{C})$ to the class $\Ob(\mathcal{C})$ so that if $f\in \Hom_{\mathcal C}(X,Y)$ is given we have $\dom(f)=X$, $\codom(f)=Y$. Now, if $$f\in\bHom_\mathcal{C}(Y,Z)\cap\bHom_\mathcal{C}(Y',Z')$$ and $$g\in\bHom_\mathcal{C}(X,Y)\cap\bHom_\mathcal{C}(X',Y')$$ we must have $X=X'$, $Y=Y'$, $Z=Z'$. The situation is very much like in graph theory, for the definition of a Directed Multigraph, a Quiver or an Automaton. I pick the definition in [1].

A Graph (understand Directed Multigraph) $\Gamma$ consists of a set $X=\vertex\Gamma$ and a set $Y=\edge\Gamma$ and two maps $o:\ Y\to X$ (origin) and $t:\ Y\to X$ (target).

This issue is explicitly unearthed and treated in [2] page 11 Remark 1.1.2 (e)

“If $f ∈ \mathcal{A}(A, B)$, we call $A$ the domain and $B$ the codomain of $f$. Every map in every category has a definite domain and a definite codomain. (If you believe it makes sense to form the intersection of an arbitrary pair of abstract sets, you should add to the definition of category the condition that $\mathcal{A}(A, B) \cap \mathcal{A}(A', B') = \emptyset$ unless $A = A'$ and $B = B'$.)”

The (mono-valued) functions are sometimes explicitly set up in the building axioms, see [3] page 11 definition 1.1.1 and, starting from axioms from which the MO could legitimately interpret these “functions” as “constructed” whereas they are “thought” as univalued (it is explicit in Serre) in the mind of many category theorists, one can repair this deficiency with triplets as in [4], page 22 Remark 3.2 point (3). I think this last construction can overcome the last construction you mention.

Late edit .- I had, this morning, the curiosity to come back to Mac Lane [5]. You can find there in chapter 1 section 2 the definition of a category through a graph with two functions $dom,cod$, very much in the spirit of Serre [1].

---

[1] Jean-Pierre Serre (1977), Trees, Springer.

[2] Tom Leinster, Basic Category Theory, Cambridge University Press (2014).

[3] Emily Riehl, Category theory in context, Cambridge University Press (2014).

[4] Jiřı́ Adámek, Horst Herrlich, and George E. Strecker, Abstract and Concrete Categories, The Joy of Cats.

[5] Mac Lane, Saunders, Categories for the Working Mathematician. Graduate Texts in Mathematics. Vol. 5 (Second ed.). Springer. ISBN 0-387-98403-8. Zbl 0906.18001.