In a union-find data structure, we store an equivalence relation on the integers [n] = \{1,\ldots,n\} via a function \mathrm{root} \colon [n] \to [n] that is idempotent, i.e. \mathrm{root} \circ \mathrm{root} = \mathrm{root}.
We can then define an equivalence relation R \subset [n] \times [n] via the pullback
One weird thing is that R is an equivalence relation whether or not \mathrm{root} is idempotent. So what is the point of idempotency?
Well, another way of thinking about the equivalence relation generated by \mathrm{root} is by looking at the coequalizer of \mathrm{root}, \mathrm{id} \colon [n] \to [n].
I think that if \mathrm{root} is not idempotent, then this coequalizer will be different than the coequalizer that comes from \pi_1,\pi_2 \colon R \to [n]. For instance, if \mathrm{root} sent k to k+1 and n to 1, then the coequalizer of \mathrm{root} and \mathrm{id} is a singleton, but the coequalizer of \pi_1,\pi_2 is [n].
So here’s a fun exercise: prove (or show a counterexample) to the following statement:
In a regular category, let \mathrm{root} \colon A \to A be a morphism. Then let R be as before. Show that the coequalizer of \pi_1,\pi_2 and the coequalizer of \mathrm{root}, \mathrm{id} are isomorphic if and only if \mathrm{root} \circ \mathrm{root} = \mathrm{root}.
It seems that we really want these to be isomorphic as quotients of [n].
Since both are given as coequalizers, it suffices to check that the maps to the coequalizer of \pi_1, \pi_2 also equalizes \mathrm{root} and \mathrm{id}, and vice versa.
Let me call \mathrm{root} simply r for brevity.
Reasoning with generalized elements, in one case we identify x with \mathrm{root}(x) for all x. Then we have x,y so that r(x) = r(y) and must prove x \sim y - but this follows because x \sim r(x) = r(y) \sim y.
So it suffices to show that the coequalizer of \pi_1,\pi_2 equalizes r and \mathrm{id} if and only if r = r^2.
But since (R,\pi_1,\pi_2) is simply the equivalence relation r(x) = r(y), the quotient equalizes r and \mathrm{id} precisely when, for all x, r(r(x)) = r(x), which is exactly what we want.
Wow, I am surprised that you didn’t end up needing some structure on the category, like a regular structure. I guess the beauty of generalized elements is that it looks just like the normal set theoretic proof.
Thinking about this a bit further, I think I accidentally used regularity without thinking about it in the second step - by identifying the coequalizer map we’re considering with an equivalence relation (a subobject of [n] \times [n], in this case (R,\pi_1,\pi_2)).
I think it’s still true that if r = r^2, the coequalizers agree.
In this case (id, r) is a map [n] \to R, which proves that these two maps are equalized by the quotient [n]/R. But in general this quotient might identify id and r “for a stupid reason”. The idea of the argument I wrote down is essentially that regular epimorphisms are the same thing as natural equivalence relations on generalized elements, and R is already an equivalence relation - but this is only true in regular categories.
I guess the way to formalize this style of reasoning for regular categories is… regular logic. So we could probably rephrase this proof in terms of regular logic and have it work out nicely.