Equality of arrows and the definition of a category

Question

I apologise in advance if this question is too roundabout for something that is likely answerable in two lines. I will present it through a concrete example, as otherwise I fear I might trip up in technical vocabulary I'm not fully acquainted with and make a mess out of the whole thing.

I have been thinking about ways of toying with the notion of equality that is typically left implicit when a category is defined. For instance, consider the single-object category the natural numbers give rise to, with the naturals as arrows, zero as identity and addition as composition. Now, given our "extra-categorical" knowledge about the natural numbers, we know that composing the arrows $2$ and $3$ results in $5$, because $3 + 2 = 5$. This usage of equality comes straight from the definition of "category" (this particular quote is lifted from this question):

A category consists of the following data,

[...]

• Arrows: $f,g,h,\ldots$

[...]

These data are required to satisfy the following laws,

• Associativity: $h \circ (g \circ f)=(h \circ g) \circ f$ for all $f : A → B, g : B → C, h : C → D$.

• Unit: $f \circ 1_A = f = 1_B \circ f$ for all $f : A → B$.

For obvious reasons the definition of "category" says nothing concrete about the $=$ relation it uses, and that is no problem -- all we have to do is to interpret it in a sensible way according to the arrows we are dealing with.

Now, suppose we want to set up a category analogous to the first one, but with only the naturals from zero to three as arrows. That is easy enough to do: just pick $(y + x)\mod 4$ instead of $y + x$ as $y \circ x$. By doing that, $3 \circ 2$ will be $1$ rather than $5$, and all will be fine. What I wonder about, though, is the possibility of using the modulo $4$ congruence to reinterpret, rather than composition, equality in the definition of the category, as if e.g. $x = y$ really meant $x \equiv y \pmod 4$ in our category. One way of doing that without uttering strange explanations such as "that $=$ sign doesn't really mean equality" would be taking as arrows things that, whatever they are, are indexed by the natural numbers -- all of them -- and then defining equality for such things. For instance, using an entirely ad hoc notation we might say that we have arrows such as $\Delta(2)$ and $\Delta(3)$, and that $\Delta(x) = \Delta(y)$ iff $x \equiv y \pmod 4$. That would perhaps authorise us to talk coloquially of "the arrow $5$", even though deep down we are aware that $\Delta(5) = \Delta(1)$.

And now, at long last, my questions: Is this sort of reinterpretation of equality in a category usual practice? What is the typical manner of expressing such tricks with a reasonable level of rigour?

P.S.: A little background on where this question came from. I am trying to state a programming problem, originally expressed in Haskell, in categorical terms. There is one category that I want to define which leads me to a scenario analogous to the one I described in the $\mod 4$ example -- except that the relevant equivalence relations, while perfectly well-defined in terms of a handful of isomorphisms, are very annoying to express in Haskell, so that I would definitely prefer to leave them as background assumptions and act as if "these Haskell functions are equivalent in this and that way" really meant "these Haskell functions are equal".

Answer 1

I'm going to take a step back first and talk about what it means for two mathematical things to be equal. In general a pair of mathematical things are equal if they behave exactly the same no matter what we do to them.

So in the natural numbers $\mathbb{N}$ $ 1 + 1 = 2 $ is saying in any case where we talk about 2 we could replace it with $(1 + 1)$.

Now for your case where you have defined your arrow composition law as $x \circ y = (x + y) \mod 4 $. In this case $ \Delta(5) $ is exactly the same thing as $ \Delta(1) $ in much the same way $ \frac{1}{2} $ is exactly the same thing as $ \frac{2}{4}$.

Just because we are using natural numbers to label the arrows doesn't mean that equality properties of the naturals translate across. This type of redefining of equality is so standard it normally isn't remarked on and is considered just what happens when you define $ \circ $ for a category.

Answer 2

One particularly interesting way to treat equivalence relations is the notion of a setoid. Since we're talking category theory, I'll give a categorical definition of setoid:

A setoid is a category that is equivalent to a set

If $X$ is a setoid, then every hom-set has at most one element, and the relation "$\hom(x, y)$ is nonempty" is an equivalence relation on the objects of $X$. Conversely, every equivalence relation can be converted into a setoid.

---

Normally, given objects $x,y$ of a category, we require that $\hom(x,y)$ be a set. But we can just as well allow $\hom(x,y)$ to be a setoid. This would be an example of a bicategory.

So, your example could be given as the following bicategory $\mathcal{B}$:

• There is a single object
• The 1-morphisms are the natural numbers
• The 2-morphisms are instances of your equivalence relation (i.e. $\hom(m,n)$ is a one-point set if and only if $m \equiv n \bmod 4$, otherwise $\hom(m,n)$ is empty)

If we let $\mathcal{C}$ be the category given by

• There is a single object
• The 1-morphisms are the mod-4 equivalence classes of natural numbers

then $\mathcal{B}$ and $\mathcal{C}$ are equivalent as bicategories; so for basically all categorical purposes, they are the same.

For some purposes, maybe even your own, the construction leading to $\mathcal{B}$ may be easier to work with than the construction leading to $\mathcal{C}$.

On the other hand, working with bicategories instead of categories may add sufficient complication that it might not be worthwhile. This is at least somewhat mitigated by the fact that bicategories where the hom-categories are all setoids are among the least complicated bicategories. Furthermore, the specific category $\mathcal{B}$ happens to be a strict bicategory. (for example, that $h \circ (g \circ f)$ is equal to $(h \circ g) \circ f$, rather than merely being isomorphic to)