To my category-infected mind, it seems that what you really need is a little category theory. :-) I take it that your equations should define an equivalence relation? (It seems strange to call them 'equations' if not.) If that's right, then an "equational theory" is the same thing as an essentially-discrete category, i.e. a category that is equivalent to a discrete one, and an "equational correspondence" is an equivalence of categories. With the definition of "equational embedding" you give, your conjecture is false. For example, let the equational theories S and T each have two terms x and y, with equations x =_S x y =_S y x =_S y x =_T x y =_T y We can define an equational embedding S -> T by mapping both terms to x, and we can define an equational embedding T -> S by mapping x to x and y to y, but there can be no equational correspondence between S and T (since 1 != 2). It would seem more natural, at least from a categorical point of view, to define an equational embedding to be a full functor, i.e. a function f: S -> T such that s =_S s' iff f(s) =_T f(s'). With that definition, your conjecture is true by the Schröder-Bernstein theorem. Robin