Every monomorphism in Rel is regular. Keith J. Bauer, 2024 Theorem: any monomorphism in the category where objects are sets, morphisms are relations, and composition is relation composition, denoted Rel, is the equalizer of some pair of morphisms. To start, we need a few facts. Firstly, Rel is self-dual. For every relation R from A to B, there is a transpose relation R† from B to A obtained by reversing the order of the ordered pairs than define a relation. It can be shown that † is an equivalence from Rel^op to itself. Secondly, Rel is equivalent to the category of free complete join-semilattices. To make this formal requires the concept of Kleisli categories, but all that is needed for this proof is that we can consider objects in Rel to be powersets ordered by inclusion and morphisms to be join-equivariant functions, which is a subcategory of the category of join-semilattices. It is also important to note that a monomorphism in Rel is an injective function from one power set to another. Now, let p: S -> A be our monomorphism. For now, we will treat p as a relation from S to A. Let B be the set of every (v, w) in the set Hom(A, 1)^2 such that v ∘ p = w ∘ p, where 1 is a singleton set. Now define f, g: A -> B as f = Sum_{(v, w) in B) v g = Sum_{(v, w) in B) w where Sum is the direct sum in Rel. By construction, f ∘ p = g ∘ p. Our goal is to show eq(f, g) = p, up to isomorphism. Let q: T -> A be a monomorphism such that f ∘ q = g ∘ q. Our goal is to construct a morphism s: T -> S such that p ∘ s = q. At this point we are going to transform our problem in two ways. Firstly, we will take the dual problem using †, and secondly, we will transition to working in the powerset characterization of Rel. Now we have p†: P(A) -> P(S) and q†: P(A) -> P(T) are join-equivariant surjections and we are searching for a morphism s†: P(S) -> P(T) such that s† ∘ p† = q†. Because f ∘ p = g ∘ p, distributing over the sum, we get that v ∘ p = w ∘ p for all (v, w) in B. Dually, this means w† ∘ v† = p† ∘ w†. We can also treat v† and w† as elements of P(A) that p† is a function on. By construction, this is precisely the data of ker p†, in the universial algebra sense of kernel, i.e. a congruence on P(A) that encodes which elements are sent to the same element in the codomain. By an isomorphism theorem of universial algebra, we have P(A)/ker p† = P(S), up to isomorphism. The same logic above applies equally well to q, so P(A)/ker q† = P(T), up to isomorphism. We also know ker p† <= ker q† (in the sense that if p† sends two elements to the same element, q† must also do the same), so by another isomorphism theorem of universial algebra, there exists a congruence ~ such that P(S)/~ = P(T), up to isomorphism. This induces a surjection s†: P(S) -> P(T) and we must have that s† ∘ p† = q† because ker p† <= ker q†. Because coeq(f†, g†) = p†, we have eq(f, g) = p as desired.