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".