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.