Abstract
The notion of semigroups with apartness has been introduced recently as a constructive counterpart of classical semigroups. On such structures, a constructive analogue of the isomorphism theorem has been proved, and quasiorder relations and related substructures have been studied. In this paper, we extend this approach by introducing inverse semigroups with apartness, a useful tool to describe partial symmetries in sets with apartness. We prove a constructive analogue of the isomorphism theorem for inverse semigroups and provide a characterisation of cocongruences on inverse semigroups.
Keywords
Set with apartness Semigroup with apartness Inverse semigroup with apartness Cocongruence1 Introduction
The concept of semigroups with apartness has been introduced in [7, 8] as yet another application of Bishop’s constructive mathematics [1, 2] to algebraic structures [14, 20]. In [3], Bridges and Reeves comment that “modern algebra has proved amenable to a [...] constructive treatment”. The reason for this can be traced back to [15], where MartinLöf argues that “if programming is understood not as the writing of instructions for this or that computing machine but as the design of methods of computation [...], then it no longer seems possible to distinguish the discipline of programming from constructive mathematics”. These considerations, alongside Howie’s motivation for the study of semigroups (and inverse semigroups) [10], motivate the constructive approach to inverse semigroups which we present in this paper.
In this work, we introduce the concept of inverse semigroups with apartness, and outline some related concepts such as that of symmetric inverse semigroups and their cocongruence pairs. We also provide constructive analogues of some classical theorems for inverse semigroups.
In Sect. 2, we introduce the basic notions of apartness and a set with apartness, as well as that of a dpartial bijection. In Sect. 3, we introduce the concept of an inverse semigroup with apartness. Theorem 2 shows that our definition is wellfounded: since inverse semigroups are semigroups of partial onetoone transformations of a set [18, 21], we prove that the set of dpartial bijections on a set with apartness leads to an inverse semigroup with apartness. Section 4 is devoted to the study of Icocongruences and their characterization in terms of cocongruence pairs. Lastly, Sect. 5 extends some of the results of [8] by providing an analogue of the Isomorphism Theorem for inverse semigroups with apartness.
2 Basic notions
Definition 1
Let X be a set, \(\cong \) an equality on X and \(\ncong \) an apartness relation on X. Then the tuple \((X,\cong ,\ncong )\) is a set with apartness.
Remark 1
By extensionality, in a set with apartness \((X,\cong ,\ncong )\) we have \(x\ncong y\) and \(y\cong z\) imply \(x\ncong z\). Notice that in [20] apartness is named “preapartness”, while the term “apartness” is used to refer to what is called a tight apartness here. Also observe that by extensionality, tightness implies \(\lnot (x\ncong y)\Leftrightarrow x\cong y\).
Definition 2

onto if for each \(y\in T\), there is \(x\in S\) such that \(f(x)\cong _T y\),

onetoone if for all \(x,y\in S\), \(f(x)\cong _T f(y)\) implies \(x\cong _S y\),

bijective if it is onto and onetoone,

injective if for all \(x,y\in S\), \(x\ncong _S y\) implies \(f(x)\ncong _T f(y)\),

strongly extensional if for all \(x,y\in S\), \(f(x)\ncong _T f(y)\) implies \(x\ncong _S y\),

an apartness bijection if it is injective, bijective and strongly extensional (see [7]).
In the sequel, we will always deal with sets with apartness and, for brevity, a set with apartness \((X,\cong ,\ncong )\) will be denoted simply by X.
Definition 3
A partial apartness bijection on S is an apartness bijection from X to Y, where X and Y are subsets of S. As usual, the sets X and Y are called respectively the domain and the image of f and denoted by \({{\,\mathrm{Dom}\,}}(f)\) and \({{\,\mathrm{Im}\,}}(f)\). A dpartial bijection on S is a partial apartness bijection whose domain and codomain are dsubsets of S. We denote by \(I^S\) the set of all dpartial bijections on S.
Example 1
Observe that in general the apartness on \(I^S\) is neither tight nor decidable w.r.t. \(\cong \). Indeed, let S be the set \(\{0,1,2,3\}\), let \(\cong \) be the standard equality on S, i.e.\(\cong {\mathop {=}\limits ^{\text { def}}}\{(0,0),(1,1),(2,2),(3,3)\}\) and let \(\ncong \) be the apartness defined by \(\ncong {\mathop {=}\limits ^{\text { def}}}\{(0,1),(1,2),(2,3),(3,0),(1,0),(2,1),(3,2),(0,3)\}\). Then let \(i,g:S\rightarrow S\) be respectively the identity map on S and the map defined by \(g(0){\mathop {=}\limits ^{\text { def}}}3\), \(g(1){\mathop {=}\limits ^{\text { def}}}2\), \(g(2){\mathop {=}\limits ^{\text { def}}}1\) and \(g(3){\mathop {=}\limits ^{\text { def}}}0\). The maps i and g are dpartial bijections and neither \(i\cong g\) nor \(i\ncong g\). Then the relation \(\ncong \) on \(I^S\) is not empty (as, for example, the identity map on the set \(\{0,2\}\) and the identity map on S are apart) but \(\ncong \) is neither tight nor decidable w.r.t. \(\cong \).
The following result is straightforward:
Theorem 1
Let \((S,\cong ,\ncong )\) be a set with apartness. Then \((I^S,\cong ,\ncong )\) is a set with apartness.
3 Inverse semigroups with apartness
Definition 4
 1.
\((S,\cong ,\ncong )\) is an inhabited set with apartness,
 2.“\(\cdot \)” is a binary operation on S such that:
 (a)
\(x\cdot (y\cdot z)\cong (x\cdot y)\cdot z\) for all \(x,y,z\in S\),
 (b)
for all \(x,y,z\in S\), \(x\cdot y\ncong z\cdot v\) implies \(x\ncong z\) or \(y\ncong v\),
 (a)
 3.“\(^{1}\)” is a unary operation such that:
 (a)
\((x^{1})^{1}\cong x\) for all \(x\in S\),
 (b)
for all \(x,y\in S\), \(x^{1}\ncong y^{1}\) implies \(x\ncong y\),
 (a)
 4.
\(x\cdot x^{1}\cdot x\cong x\) for all \(x\in S\).
As usual, we will write xy instead of \(x\cdot y\).
Remark 2
 3(b’)
\(x^{1}\ncong y^{1} \Leftrightarrow x\ncong y\) for all \(x,y\in S\).
Definition 5
 5.
\(xx^{1}yy^{1}\cong yy^{1}xx^{1}\) for all \(x,y\in S\).
Remark 3
Observe that property 5. implies that \((xy)^{1}\cong y^{1}x^{1}\).
An idempotent of S is an element \(e\in S\) such that \(ee\cong e\); we denote the set of the idempotents of S by E(S).
Proposition 1
Let S be an inverse semigroup with apartness. Then \(e\cong ee^{1}\) and \(ef\cong fe\) for each \(e,f\in E(S)\).
Proof
The proof is the same of the classical case and can be found in [11, Theorem 5.1.1, \((1)\Rightarrow (2)\)]. \(\square \)
Proposition 2
A semigroup with apartness \((S,\cong ,\ncong ,\cdot )\) is an inverse semigroup if and only if the relation \(\iota {\mathop {=}\limits ^{\text { def}}}\{(x,y)\in S\times S\mid x\cong xyx \wedge y\cong yxy\}\) is a strongly extensional function from S to S.
Proof
Let \((S,\cong ,\ncong ,\cdot ,^{1})\) be an inverse semigroup with apartness. Then for each \(x\in S\), \((x,x^{1})\in \iota \). Now we show that \(y\cong x^{1}\) for each \((x,y)\in \iota \). From \(xx^{1}x\cong xyx\cong x\) we get \(xx^{1}xy\cong xy\) and \(xyxx^{1}\cong xx^{1}\), and since xy and \(xx^{1}\) are idempotents, it follows \(xy\cong xx^{1}\). Similarly we get \(yx\cong x^{1}x\). Then \(y\cong yxy\cong x^{1}xy\cong x^{1}xx^{1}\cong x^{1}\). Thus, \(\iota \) is the function \(^{1}\), and since \(^{1}\) is strongly extensional by definition, so is \(\iota \).
Conversely, assume that S is a semigroup with apartness such that \(\iota \) is a strongly extensional function from S to S. For \((x,y)\in \iota \), put \(x^{1}\cong \iota (x)\). Then it is immediate that \((x^{1})^{1}\cong x\). Moreover, let \(e,f\in E(S)\): it is easy to verify that the element \(z{\mathop {=}\limits ^{\text { def}}}f(ef)^{1}e\) belongs to E(S). In addition, \((ef)z(ef)\cong (ef)\) and \(z(ef)z \cong z\). Then, since \(z^3\cong z\), both (z, z) and (z, ef) are in \(\iota \), so \(z\cong ef\). Whence \(fz\cong z\cong fef\) and \(ze\cong z\cong efe\), i.e., \(ef\cong _S fef \cong efe\). Similarly, we can get \(fe\cong efe \cong fef\). So, \(ef\cong fe\) for all \(e,f\in E(S)\). Moreover, \(\iota \) is strongly extensional by definition, whence S is an inverse semigroup with apartness. \(\square \)
Remark 4
The relation \(\iota \) defined above is a strongly extensional function from S to S if and only if S is equipped with a strongly extensional unary operation f such that for all \(x,x'\in X\) it holds that \(xf(x)x\cong x\), \(f(x)xf(x)\cong f(x)\), and \((xx'x\cong x \wedge x'xx'\cong x')\) implies \(x'\cong f(x)\).
Theorem 2
Let \((S,\cong ,\ncong )\) be a set with apartness. Then \((I^S,\cong ,\ncong ,\circ ,^{1})\) is an inverse semigroup with apartness, where “\(\circ \)” is the usual product of relations and “\(^{1}\)” denotes the inverse relation.
Proof
Now, suppose \(f^{1}(y)\cong f^{1}(y')\), and let \(x,x'\in X\) be such that \(x\cong f^{1}(y)\) and \(x'\cong f^{1}(y')\). Then \((y,x),(y',x')\in f^{1}\), so \(f(x)\cong y\) and \(f(x')\cong y'\). By extensionality we have \(x\cong x'\), then \(f(x)\cong f(x')\) and \(y\cong y'\), so \(f^{1}\) is onetoone. Now, suppose \(f^{1}(y)\ncong f^{1}(y')\) and, as above, let \(x,x'\in X\) be such that \(x\cong f^{1}(y)\) and \(x'\cong f^{1}(y')\) from which \(f(x)\cong y\) and \(f(x')\cong y'\). By extensionality, we have \(x\ncong x'\) and, since f is injective, it follows \(f(x)\ncong f(x')\) and then \(y\ncong y'\), so \(f^{1}\) is strongly extensional. Finally, suppose \(y\ncong y'\) and, as usual, let \(x,x'\in X\) be such that \(x\cong f^{1}(y)\), \(x'\cong f^{1}(y')\), \(f(x)\cong y\) and \(f(x')\cong y'\). By extensionality, we have \(f(x)\ncong f(x')\), and since f is strongly extensional it follows \(x\ncong x'\) and then \(f^{1}(y)\ncong f^{1}(y')\), so \(f^{1}\) is injective. Thus we have proved that \(f^{1}\in I^S\).
Now, let us consider inversion. The map \(^{1}:I^S\rightarrow I^S\) sending each f in its inverse \(f^{1}\) is clearly an unary strongly extensional operation on \(I^S\) and \((f^{1})^{1}\cong f\) for each \(f\in I^S\). Moreover, it is straightforward to prove that \(f^{1}\circ f\) is the identity function on \({{\,\mathrm{Dom}\,}}(f^{1})\) and that \(f\circ f^{1}\) is the identity function on \({{\,\mathrm{Dom}\,}}(f)\), and hence \(f\circ f^{1}\circ f\cong f\) for each \(f\in I^S\). Lastly, for all \(f,g\in I^S\), the function \((f\circ f^{1})\circ (g\circ g^{1})\) is the identity function on \({{\,\mathrm{Dom}\,}}(f)\cap {{\,\mathrm{Dom}\,}}(g)\), while \((g\circ g^{1})\circ (f\circ f^{1})\) is the identity function on \({{\,\mathrm{Dom}\,}}(g)\cap {{\,\mathrm{Dom}\,}}(f)\), and so \((f\circ f^{1})\circ (g\circ g^{1})\cong (g\circ g^{1})\circ (f\circ f^{1})\). \(\square \)
Definition 6
Lemma 1
 1.
\(Se\cong Sf \Rightarrow e\cong f\) and \(eS\cong fS \Rightarrow e\cong f\) for all \(e,f\in E(S)\);
 2.
\((Se\cap Sf)\cong S(ef)\) and \((eS\cap fS)\cong (ef)S\) for all \(e,f\in E(S)\);
 3.
\(S(aa^{1})\cong Sa^{1}\), \(S(a^{1}a)\cong Sa\), \((aa^{1})S\cong aS\) and \((a^{1}a)S\cong a^{1}S\) for all \(a\in S\).
Proof
The proof is analogous to the classical case ( [11], Lemma 5.1.6). \(\square \)
Proposition 3
Let \((S,\cong ,\ncong ,\cdot ,^{1})\) be an inverse semigroup with apartness and suppose that \(e\cong f\) or \(e\ncong f\) for all \(e,f\in E(S)\), i.e., \(\cong \) and \(\ncong \) are relatively decidable in E(S). Then, for each \(a\in S\), the sets Sa, aS, \(Sa^{1}\) and \(a^{1}S\) are detachable.
Proof
First observe that \(x\in Sa\) if and only if \(xa^{1}a\cong x\). Indeed, suppose \(x\in Sa\), i.e., \(x\cong sa\) for some \(s\in S\). Since \(sa\cong saa^{1}a\), we have immediately \(x\cong xa^{1}a\). Conversely, it is obvious that if \(x\cong xa^{1}a\), then \(x\in Sa\). Now we can prove that Sa is a dsubset. Let \(x\in S\): as \(x^{1}x\) and \(a^{1}a\) are idempotents, then \(x^{1}x\cong x^{1}xa^{1}a\) or \(x^{1}x\ncong x^{1}xa^{1}a\). By extensionality, the former condition implies \(xx^{1}x\cong xx^{1}xa^{1}a\), i.e., \(x\cong xa^{1}a\), and then \(x\in Sa\). Now suppose that \(x^{1}x\ncong x^{1}xa^{1}a\). By cotransitivity w.r.t. the product, we get \(x^{1}\ncong x^{1}\) or \(x\ncong xa^{1}a\), and, by irreflexivity, it follows \(x\ncong xa^{1}a\). So, let \(y\in Sa\), by the cotransitivity of apartness we get \(x\ncong y\) or \(y\ncong xa^{1}a\). In the last case, since \(y\in Sa\), we have \(y\cong ya^{1}a\), and then, by extensionality, \(ya^{1}a\ncong xa^{1}a\), so, by cotransitivity, \(y\ncong x\), and hence \(x\rhd Sa\). Thus we have proved that Sa is a dsubset, and similarly we obtain the same result for aS, \(Sa^{1}\) and \(a^{1}S\). \(\square \)
Definition 7
Let S and T be semigroups with apartness. A map \(f :S \rightarrow T\) is a homomorphism if \(f(xy) \cong f(x)f(y)\). A strongly extensional homomorphism (sehomomorphism for short) is an apartness embedding if it is oneone and injective. An sehomomorphism is an apartness isomorphism if it is an apartness bijection.
Definition 8
Let \((S,\cong _S,\ncong _S),\ (T,\cong _T,\ncong _T)\) be two semigroups with apartness. The semigroup \((S,\cong _S,\ncong _S)\) is seembeddable in \((T,\cong _T,\ncong _T)\) if there exists an apartness embedding \(\varphi :S\rightarrow T\).
Theorem 3
Let \((S,\cong ,\ncong ,\cdot ,^{1})\) be an inverse semigroup with apartness and suppose that \(e\cong f\) or \(e\ncong f\) for all \(e,f\in E(S)\), i.e., \(\cong \) and \(\ncong \) are relatively decidable in E(S). Then S is seembeddable in the symmetric inverse semigroup with apartness \((I^S,\cong ,\ncong ,\circ ,^{1})\) on the set \((S,\cong ,\ncong )\).
Proof
For each \(a\in S\), let \(\rho _a\) be the map with \({{\,\mathrm{Dom}\,}}(\rho _a){\mathop {=}\limits ^{\text { def}}}Sa^{1}\) defined by \(\rho _a(x){\mathop {=}\limits ^{\text { def}}}xa\). Clearly \({{\,\mathrm{Im}\,}}(\rho _a)\cong Sa\) and so, by Proposition 3, the domain and the image of \(\rho _a\) are dsubsets. Obviously, the map \(\rho _a\) is extensional. It is onto, since \(sa\cong \rho _a (saa^{1})\) for each \(s\in S\). Now let \(x,y \in Sa^{1}\), by definition \(x\cong sa^{1}\) and \(y\cong ta^{1}\) for some \(s,t\in S\). If \(\rho _a(x)\cong \rho _a(y)\), i.e., \((sa^{1})a \cong (ta^{1})a\), by extensionality we have \(sa^{1}aa^{1} \cong ta^{1}aa^{1}\), whence \(x\cong sa^{1}\cong ta^{1}\cong y\), as so \(\rho _a\) is onetoone. If \(x\ncong y\), we have \(sa^{1} \ncong ta^{1}\) and then \(sa^{1}aa^{1} \ncong ta^{1}aa^{1}\). Then \(xaa^{1} \ncong yaa^{1}\) and, by extensionality w.r.t. the product, \(xa \ncong ya\), or equivalently \(\rho _a(x)\ncong \rho _a(y)\), and thus \(\rho _a\) is injective. The fact that \(\rho _a\) is strongly extensional follows directly from the fact that the product in S is strongly extensional. Therefore \(\rho _a\) is a dpartial bijection on S.
Let \(\varphi :S\rightarrow I^S\) be the map defined by \(\varphi (a){\mathop {=}\limits ^{\text { def}}}\rho _a\) for each \(a\in S\). Then, as in the classical case, \(\varphi \) is onetoone. Indeed, assume that \(\varphi (a)\cong \varphi (b)\), then \({{\,\mathrm{Dom}\,}}(\rho _a)\cong {{\,\mathrm{Dom}\,}}(\rho _b)\) and so, by property 3 of Lemma 1, we get \(S(aa^{1})\cong S(bb^{1})\). Hence, by property 1. of Lemma 1, we obtain \(aa^{1}\cong _S bb^{1}\), and then \(a\cong aa^{1}a\cong \rho _a(aa^{1})\cong \rho _b(aa^{1})\cong \rho _b(bb^{1})\cong b\).
Now, we show that \(\varphi \) is strongly extensional. Assume that \(\varphi (a)\ncong \varphi (b)\). Since \({{\,\mathrm{Dom}\,}}(\rho _b)\) is a dsubset of S, then \(a^{1}\in {{\,\mathrm{Dom}\,}}(\rho _b)\vee a^{1}\rhd {{\,\mathrm{Dom}\,}}(\rho _b)\), and analogously \(b^{1}\in {{\,\mathrm{Dom}\,}}(\rho _a)\vee b^{1}\rhd {{\,\mathrm{Dom}\,}}(\rho _a)\).
If \(a^{1}\rhd {{\,\mathrm{Dom}\,}}(\rho _b)\) then, since \(b^{1}\in {{\,\mathrm{Dom}\,}}(\rho _b)\), we get \(a^{1}\ncong _S b^{1}\). Analogously, if \(b^{1}\rhd {{\,\mathrm{Dom}\,}}(\rho _a)\) then, since \(a^{1}\in {{\,\mathrm{Dom}\,}}(\rho _a)\), we get \(a^{1}\ncong _S b^{1}\). In both cases, from the strong extensionality of inversion, we get \(a\ncong _S b\). Then assume \(a^{1}\in {{\,\mathrm{Dom}\,}}(\rho _b)\) and \(b^{1}\in {{\,\mathrm{Dom}\,}}(\rho _a)\). Hence \({{\,\mathrm{Dom}\,}}(\rho _b)\cong Sb^{1}\cong Sa^{1}\cong {{\,\mathrm{Dom}\,}}(\rho _a)\). Since \(\varphi (a)\ncong \varphi (b)\), we get that there is \(x\in {{\,\mathrm{Dom}\,}}(\rho _a)\cong {{\,\mathrm{Dom}\,}}(\rho _b)\) such that \(\rho _a(x)\ncong _S \rho _b(x)\), i.e., \( x\cdot a\ncong _S x\cdot b\), and, by strong extensionality, it follows \(a\ncong _S b\). So, we have proved that \(\varphi \) is a dpartial bijection.
It is routine to prove that \(\rho _a\circ \rho _b\cong \rho _{a\cdot b}\) and \((\rho _a)^{1}\cong \rho _{a^{1}}\), so \(\varphi \) is an seembedding, as required. \(\square \)
Notice that Theorem 3 is stated under the assumption that \(\cong \) and \(\ncong \) are relatively decidable on the set of idempotents. In general, an inverse semigroup with apartness \((S,\cong ,\ncong ,\cdot ,^{1})\) cannot be embedded into the symmetric inverse semigroup with apartness \((I^S,\cong ,\ncong ,\circ ,^{1})\), as the next example shows.
Example 2
4 Icocongruences
Congruences play a central role in many of the structure theorems of semigroups, so it is quite natural to study their constructive counterparts. Cocongruences are introduced in [7], where the prefix “co” suggests that they cooperate with classical equivalences in order to contemplate the presence of the apartness relation. Cocongruences are then defined as follows.
Definition 9
 1.
it is consistent with respect to the apartness, i.e., \(\kappa \subseteq \ncong \),
 2.
it is cotransitive, i.e., \((x,y)\in \kappa \) implies \((x,z)\in \kappa \) or \((z,y)\in \kappa \),
 3.
it is symmetric, i.e., \((x,y)\in \kappa \) implies \((y,x)\in \kappa \),
 4.
it is cocompatible w.r.t. the semigroup multiplication, i.e., \((ax,by)\in \kappa \) implies \((a,b)\in \kappa \) or \((x,y)\in \kappa \).
Lemma 2
 4’.
\((ac,bc)\in \kappa \) implies \((a,b)\in \kappa \) and \((ca,cb)\in \kappa \) implies \((a,b)\in \kappa \) .
Proof
Let \(\kappa \) be cocompatible w.r.t. the multiplication of S, and \(a,b,c\in S\). Then \((ac,bc)\in \kappa \) implies either \((a,b)\in \kappa \) or \((c,c)\in \kappa \). As \(\kappa \) is consistent, then \(\lnot ((c,c)\in \kappa )\), and then actually \((a,b)\in \kappa \). The case \((ca,cb)\in \kappa \) is identical.
Now, let \(\kappa \) be a consistent and cotransitive binary relation that satisfies condition 4’.
Let \(a,b,x,y\in S\) be such that \((ax,by)\in \kappa \). By cotransitivity, it follows either \((ax,ay)\in \kappa \) or \((ay,by)\in \kappa \), and, by condition 4’, either \((x,y)\in \kappa \) or \((a,b)\in \kappa \), as required. \(\square \)
In the case of inverse semigroups with apartness, we have to add the cocompatibility with respect to the inversion.
Definition 10
A binary relation \(\kappa \) on an inverse semigroup with apartness \((S,\cong ,\ncong ,\cdot ,^{1})\) is an Icocongruence if it is a cocongruence on \((S,\cong ,\ncong ,\cdot )\) and it is cocompatible w.r.t. the inversion, i.e., \((a^{1},b^{1})\in \kappa \) implies \((a,b)\in \kappa \) for all \(a,b\in S\).
Proposition 4
Proof
Property (2) follows directly from the cocompatibility with respect to the inversion and condition 3(a) of Definition 4. To prove property (3), let \((a,b)\rhd \kappa \) and let \((c,d)\in \kappa \). Then also \((c^{1},d^{1})\in \kappa \), and so \((a,b)\ncong (c^{1},d^{1})\). Thus either \(a\ncong c^{1}\) or \(b\ncong d^{1}\). From condition 3(b’) of Definition 4, it follows either \(a^{1}\ncong c\) or \(b^{1}\ncong d\), thus \((a^{1},b^{1})\ncong (c,d)\) and then \((a^{1},b^{1})\rhd \kappa \). The other part of the implication follows in the same way. \(\square \)
Following a common notation, for an Icocongruence \(\kappa \) on S and for \(a\in S\) we denote by \(\kappa (a)\) the set of all \(b\in S\) such that \((a,b)\in \kappa \).
Definition 11
An Icocongruence \(\kappa \) is called conormal if for all \(a\in S\) and for all \(e,f\in E(S)\), \((a^{1}ea,a^{1}fa)\in \kappa \) implies \((e,f)\in \kappa \).
Strictly related to Icocongruences, we can define some special substructure of inverse semigroups.
Definition 12
 1.
\(xy\in M\) implies \(x\in M\vee y\in M\),
 2.
\(x^{1}\in M\) implies \(x\in M\).
 1.
cofull if \(e\rhd M\) for all \(e\in E(S)\);
 2.
coselfconjugate if \(x^{1}ax\in M\) implies \(a\in M\) for all \(a,x\in S\);
 3.
conormal if it is cofull and coselfconjugate.
In [21], Wagner proved that every congruence on an inverse semigroup is completely determined by its idempotent classes. The advances made in [9, 17, 19] lead to a general result describing the congruences on an inverse semigroup, see [13, Theorem 2, p. 135]: for an inverse semigroup S, there exists a bijection between the set of congruences on S and the set of congruence pairs (namely, a pair consisting of a normal subsemigroup and a normal congruence satisfying some special conditions) on S. Along the same line, we want to give a characterization of Icocongruences on an inverse semigroup with apartness in terms of “cocongruence pairs”.
Definition 13
 1.
\(ae\in M \vee (e,a^{1}a)\in \kappa \) for all \(a\in M\) and for all \(e\in E(S)\);
 2.
\((aa^{1},a^{1}a)\in \kappa \) implies \(a\in M\) for all \(a\in S\).
Definition 14
Theorem 4
Let S be an inverse semigroup with apartness and let \(\kappa \) be an Icocongruence on S. Let \(M{\mathop {=}\limits ^{\text { def}}}{{\,\mathrm{coker}\,}}(\kappa )\) and \(\nu {\mathop {=}\limits ^{\text { def}}}{{\,\mathrm{tr}\,}}(\kappa )\). Then \((M,\nu )\) is a cocongruence pair.
Proof
Obviously \(\nu \) is a conormal Icocongruence on E(S). Let us prove that M is an inverse antisubsemigroup of S. Let \(xy\in M\), then for all \(e,f\in E(S)\) we have \(xy\in \kappa (ef)\), i.e., \((xy,ef)\in \kappa \). By the cocompatibility w.r.t. the product, it follows that \((x,e)\in \kappa \vee (y,f)\in \kappa \). From Kripke semantics, this entails that either \((x,e)\in \kappa \) for each \(e\in E(S)\), and so \(x\in M\), or \((y,f)\in \kappa \) for all \(f\in E(S)\), and so \(y\in M\). Now suppose \(x^{1}\in M\). Then \((x^{1},e)\in \kappa \) for all \(e\in E(S)\) and, since \(e\cong e^{1}\) and \(\kappa \) is cocompatible w.r.t. the inversion, we have \((x,e)\in \kappa \), and so \(x\in M\). We now prove that M is cofull. Let \(e\in E(S)\) and \(x\in M\). Then \(x\in \kappa (e)\), i.e., \((x,e)\in \kappa \). As \(\kappa \) is consistent, this implies \(x\ncong e\), and then, for the generality of \(x\in S\), we get \(e\rhd M\). Now, to prove that M is coselfconjugate, let \(x^{1}ax\in M\). We have that for all \(e\in E(S)\), the element \(x^{1}ex\) belongs to E(S), and then \((x^{1}ax,x^{1}ex)\in \kappa \). Property 4’ of Lemma 2 implies \((a,e)\in \kappa \), i.e., for the generality of \(e\in E(S)\), that \(a\in M\). So M is a conormal inverse antisubsemigroup of S.
Lastly, we prove that \((M,\nu )\) is a cocongruence pair. Let \(a\in M\), \(e,f\in E(S)\). As M is the cokernel of \(\kappa \), by definition we have \((a,f)\in \kappa \). Considering the element \(ae\in S\), by cotransitivity of \(\kappa \), we get either \((a,ae)\in \kappa \) or \((ae,f)\in \kappa \). In the former case, we also have \((aa^{1}a,ae)\in \kappa \), and by Lemma 2, property 4’, we obtain \((a^{1}a,e)\in \kappa \) and then \((a^{1}a,e)\in \nu \). Thus, by the symmetry of \(\nu \), we have \((e,a^{1}a)\in \nu \). In the latter case, we have \(ae\in \kappa (f)\) and, for the generality of f, it follows that \(ae\in M\). Now, suppose \((aa^{1},a^{1}a)\in \nu \). Then, for each \(e\in E(S)\), we get \((aa^{1},e)\cong (aa^{1},ee^{1})\in \nu \subseteq \kappa \) or \((e,a^{1}a)\cong (e^{1}e,a^{1}a)\in \nu \subseteq \kappa \), then, by the cocompatibility of \(\kappa \) w.r.t. the product and inversion and symmetry, we have \((a,e)\in \kappa \). \(\square \)
Before proving that Theorem 4 can be in some sense inverted, we need a technical lemma.
Lemma 3
 1.
if \(ab\in M\), then \(aeb\in M\) or \((e,a^{1}a)\in \nu \);
 2.
if \(aeb\in M\), then \(ab\in M\).
Proof
Assume \(ab\in M\), since \((M,\nu )\) is a cocongruence pair and \(b^{1}eb\in E(S)\), we have \(ab(b^{1}eb)\in M\) or \((b^{1}eb,(ab)^{1}ab)\in \nu \). In the former case we have \(ab(b^{1}eb)\cong ae(bb^{1})b\cong aeb\in M\); in the latter case, by property 4’ of Lemma 2, we have \((e,a^{1}a)\in \nu \), and then the first claim is proved.
Now let \(aeb\in M\). Then \(aeb\cong aebb^{1}b\cong abb^{1}eb\in M\). From the definition of inverse antisubsemigroup it follows \(ab\in M\) or \(b^{1}eb\in M\). The second case gives a contradiction, as M is cofull, and then also the second statement is proved. \(\square \)
We are now able to prove that each cocongruence pair implicitly defines a (minimal) Icocongruence on an inverse semigroup with apartness.
Theorem 5
Proof
Let \((M,\nu )\) be a cocongruence pair. The relation \(\kappa _{(M,\nu )}\) is consistent because \(\nu \) is consistent and M is cofull. It is symmetric because \(\nu \) is symmetric and M is an inverse antisubsemigroup. We now prove that \(\kappa _{(M,\nu )}\) is also cotransitive. Let \(x,y\in S\) such that \((x,y)\in \kappa _{(M,\nu )}\) and let \(z\in S\). Note that \(z^{1}z\in E(S)\). If \(xy^{1}\in M\), then from Lemma 3 we have \(xz^{1}zy^{1}\in M\) or \((z^{1}z,x^{1}x)\in \nu \). In the former case, from the definition of inverse antisubsemigroup, we have either \(xz^{1}\in M\) or \(zy^{1}\in M\), and then either \((x,z)\in \kappa _{(M,\nu )}\) or \((z,y)\in \kappa _{(M,\nu )}\). In the latter case, it follows directly from the definition of \(\kappa _{(M,\nu )}\) that \((z,x)\in \kappa _{(M,\nu )}\), and by symmetry, also \((x,z)\in \kappa _{(M,\nu )}\). The case \(x^{1}y\in M\) is identical, so consider the case \((x^{1}x,y^{1}y)\in \nu \). By cotransitivity of \(\nu \), we have either \((x^{1}x,z^{1}z)\in \nu \) or \((z^{1}z,y^{1}y)\in \nu \), and then directly from the definition of \(\kappa _{(M,\nu )}\), it follows that either \((x,z)\in \kappa _{(M,\nu )}\) or \((z,y)\in \kappa _{(M,\nu )}\). The case \((xx^{1},yy^{1})\in \nu \) is clearly identical, so consider the case \((x^{1}fx,y^{1}fy)\in \nu \) for some \(f\in E(S)\). Again, by cotransitivity of \(\nu \), we have either \((x^{1}fx,z^{1}fz)\in \nu \) or \((z^{1}fz,y^{1}fy)\in \nu \), and then directly from the definition of \(\kappa _{(M,\nu )}\), it follows that either \((x,z)\in \kappa _{(M,\nu )}\) or \((z,y)\in \kappa _{(M,\nu )}\). The case \((xfx^{1},yfy^{1})\in \nu \) for some \(f\in E(S)\) is identical, so we have proved that \(\kappa _{(M,\nu )}\) is cotransitive.
Now we prove that \(\kappa _{(M,\nu )}\) is cocompatible w.r.t. the product showing that it satisfies condition 4’ of Lemma 2. Let \(a,b,c\in S\). First suppose \((ac,bc)\in \kappa _{(M,\nu )}\). If \(ac(bc)^{1}\cong acc^{1}b^{1}\in M\), then, as \(cc^{1}\in E(S)\), by Lemma 3 it follows \(ab^{1}\in M\) and so \((a,b)\in \kappa _{(M,\nu )}\). If \((ac)^{1}bc\cong c^{1}a^{1}bc\in M\), then, as M is coselfconjugate, it follows \(a^{1}b\in M\) and so \((a,b)\in \kappa _{(M,\nu )}\). If \(((ac)^{1}ac,(bc)^{1}bc)\cong (c^{1}a^{1}ac,c^{1}b^{1}bc)\in \nu \), then, by conormality of \(\nu \), it follows \((a^{1}a,b^{1}b)\) and so \((a,b)\in \kappa _{(M,\nu )}\). If \((ac(ac)^{1},bc(bc)^{1})\cong (acc^{1}a^{1},bcc^{1}b^{1})\in \nu \), then, as \(cc^{1}\in E(S)\), it follows directly by definition that \((a,b)\in \kappa _{(M,\nu )}\).
The cases \(((ac)^{1}fac,(bc)^{1}fbc)\in \nu \) and \((acf(ac)^{1},bcf(bc)^{1})\in \nu \) with \(f\in E(S)\) are identical to the two previous cases. Analogously we can prove that \((ca,cb)\in \kappa _{(M,\nu )}\) implies \((a,b)\in \kappa _{(M,\nu )}\). Lastly, the fact that \(\kappa _{(M,\nu )}\) is also cocompatible w.r.t. the inversion directly follows by definition, and then \(\kappa _{(M,\nu )}\) is actually a Icocongruence on S.
We now prove that the cokernel and the trace of \(\kappa _{(M,\nu )}\) are M and \(\nu \), respectively. Let \(a\in M\), and \(e\in E(S)\). Then, as \((M,\nu )\) is a cocongruence pair, we get either \(ae\cong ae^{1}\in M\) or \((e,a^{1}a)\cong (e^{1}e,a^{1}a)\in \nu \) and in both cases \((a,e)\in \kappa _{(M,\nu )}\), and so \(a\in {{\,\mathrm{coker}\,}}(\kappa _{(M,\nu )})\). Conversely, let \(a\in {{\,\mathrm{coker}\,}}(\kappa _{(M,\nu )})\). Then, for all \(e\in E(S)\) it is \((a,e)\in \kappa _{(M,\nu )}\), and in particular \((a,a^{1}a)\in \kappa _{(M,\nu )}\).
Observe that \({\lnot }((a^{1}a,a^{1}aa^{1}a)\in \nu )\) as \((a^{1}a,a^{1}aa^{1}a)\in \nu \) would entail \((a^{1}a,a^{1}a)\in \nu \), and, since \(\nu \) is consistent, this is a contradiction.
Then one of the following five cases holds. If \(aa^{1}a \in M\), then \(a\in M\). If \(a^{1}a^{1}a \in M\), then, as Mis coselfconjugate, we have \(a^{1} \in M\) and again \(a\in M\).
If \((a^{1}a,aa^{1}aa^{1})\in \nu \), then \((a^{1}a,aa^{1})\in \nu \), and, by definition of cocongruence pair, we have \(a\in M\). If \((a^{1}fa,a^{1}afa^{1}a)\in \nu \) for some \(f\in E(S)\), then it follows also \((a^{1}fa,fa^{1}af)\in \nu \). Let us consider the element \(faa^{1}f\in E(S)\). By the cotransitivity of \(\nu \) we have either \((a^{1}fa,faa^{1}f)\in \nu \) or \((faa^{1}f,fa^{1}af)\in \nu \). In the former case we have \((a^{1}fa,faa^{1}f)\cong (a^{1}f(a^{1}f)^{1},(a^{1}f)^{1}a^{1}f)\in \nu \), and then, as \((M,\nu )\) is a cocongruence pair, it follows \(a^{1}f\in M\) and, remembering that by definition \(f\rhd M\), also \(a^{1}\in M\) and \(a\in M\). In the latter case we obtain \((f^{1}aa^{1}f,f^{1}a^{1}af)\in \nu \), and by conormality of \(\nu \), we have \((aa^{1},a^{1}a)\in \nu \) and then \(a\in M\). Thus we have proved that \({{\,\mathrm{coker}\,}}(\kappa _{(M,\nu )})\cong M\).
Now let \(e,f\in E(S)\) such that \((e,f) \in \nu \). Then \((ee^{1},ff^{1}) \in \nu \), and so \((e,f) \in {{\,\mathrm{tr}\,}}(\kappa _{(M,\nu )})\). So, let \((e,f) \in {{\,\mathrm{tr}\,}}(\kappa _{(M,\nu )})\). In particular we have \((e,f) \in \kappa _{(M,\nu )}\). As \(e^{1}f\) and \(ef^{1}\) are both idempotents and M is cofull, we only have to consider the following four cases. Let \((e^{1}e,f^{1}f) \in \nu \) or \((ee^{1},ff^{1}) \in \nu \), then both cases give \((e,f) \in \nu \), as required. If \((e^{1}ge,f^{1}gf) \in \nu \) for some \(g\in E(S)\), then \((geg^{1},gfg^{1}) \in \nu \) and, by conormality of \(\nu \), again we have \((e,f) \in \nu \). The case \((ege^{1},fgf^{1}) \in \nu \) for some \(g\in E(S)\) is identical to the previous one. Thus we have proved that \({{\,\mathrm{tr}\,}}(\kappa _{(M,\nu )})\cong \nu \).
Finally, we prove that \(\kappa _{(M,\nu )}\) is the smallest Icocongruence on S having M and \(\nu \) as its cokernel and its trace, respectively. Let \(\tau \) be a cocongruence on S such that \({{\,\mathrm{coker}\,}}(\tau )\cong M\) and \({{\,\mathrm{tr}\,}}(\tau )\cong \nu \), and \((a,b)\in \kappa _{(M,\nu )}\). If \(ab^{1}\in M\), then \((ab^{1},aa^{1})\in \tau \), as M is the cokernel of \(\tau \) and \(aa^{1}\in E(S)\). As \(\tau \) is an Icocongruence, from condition 4’ of Lemma 2, we have \((b^{1},a^{1})\in \tau \), and then \((a,b)\in \tau \). The case \(a^{1}b\in M\) is analogous, as it entails \((a^{1}b,a^{1}a)\in \tau \) and then \((a,b)\in \tau \). If \((a^{1}a,b^{1}b)\in \nu \cong {{\,\mathrm{tr}\,}}(\tau )\), then \((a^{1}a,b^{1}b)\in \tau \). Let us consider the element \(a^{1}b\in S\), by cotransitivity of \(\tau \) we have either \((a^{1}a,a^{1}b)\in \tau \) or \((a^{1}b,b^{1}b)\in \tau \) and in any case, from condition 4’ of Lemma 2, we have \((a,b)\in \tau \). The case \((aa^{1},bb^{1})\in \nu \) is identical to the previous one, when one consider the element \(ba^{1}\in S\). The last two cases, namely if \((a^{1}fa,b^{1}fb)\in \nu \) or \((afa^{1},bfb^{1})\in \nu \) for some \(f\in E(S)\), are identical to the two previous case, when one consider the element \(a^{1}fb\in S\) or \(bfa^{1}\in S\), respectively. Thus, we have proved that \(\kappa _{(M,\nu )}\subseteq \tau \). \(\square \)
Lastly, we can show how Icocongruences are related to congruences in an inverse semigroup.
Definition 15
Theorem 6
This result naturally extends to inverse semigroups with apartness.
Corollary 1
Let \(\kappa \) be an Icocongruence on an inverse semigroup with apartness S. The relation \({\sim } \kappa \) is a congruence on S and \(\kappa \) is associated with \({\sim } \kappa \).
Proof
We only need to prove that \({\sim }\kappa \) is compatible w.r.t. the inversion. This follows from [11, Theorem 5.1.4, formula (5.1.2)]. More explicitly, we can observe that if \((a,b)\in {\sim }\kappa \), then \((a,b)\rhd \kappa \). By property 3 of Proposition 4, this implies also \((a^{1},b^{1})\rhd \kappa \), thus \((a^{1},b^{1})\in {\sim }\kappa \). \(\square \)
5 The isomorphism theorem
In [7], the authors have introduced the concept of a strongly extensional homomorphism between semigroups with apartness and proved that the quotient set induced by a cocongruence of a semigroup with apartness inherits the same structure (see [7], Theorems 2.4 and 3.3). This naturally leads to the Apartness Isomorphism Theorem for semigroups [7, Theorem 3.5].
We show that this result can be easily extended to the case of inverse semigroups with apartness.
Definition 16
Theorem 7
Proof
The theorem in [7] is stated for semigroups with apartness, so we only need to prove that properties 3(a), 3(b) and 4. of Definition 4 and property 5. of Definition 5 are satisfied, and this immediately follows by a direct calculation. \(\square \)
Definition 17
Now we can finally state the Apartness Isomorphism Theorem for inverse semigroups with apartness.
Theorem 8
(Corollary of [7, Theorem 2.5, Theorem 3.4]) Let \(f :S \rightarrow T\) be an sehomomorphism between inverse semigroups with apartness. Then \({{\,\mathrm{coker}\,}}(f)\) is an Icocongruence associated with the congruence \(\ker (f)\subseteq {\sim }{{\,\mathrm{coker}\,}}(f)\). Moreover, \((S/\ker (f),\cong ,\ncong ,\cdot )\) is an inverse semigroup with apartness and the map \(\Theta :S/\ker (f)\rightarrow T\) defined by \(\Theta ([x]_{\ker (f)}){\mathop {=}\limits ^{\text { def}}}f(x)\) is an seembedding such that \(f \cong \Theta \circ \pi \), where \(\pi \) is the natural projection. Lastly, if f is onto, then \(\Theta \) is an apartness isomorphism.
Proof
Theorem 3.4 in [7] is stated for semigroups with apartness, so we only have to check the properties involving inversion. First, observe that we cannot apply Theorem 7 to prove that \(S/\ker (f)\) is an inverse semigroup with apartness, since in general \(\ker (f)\) differs from \({\sim }{{\,\mathrm{coker}\,}}(f)\). Nevertheless, it is routine to prove properties 3(a), 3(b) and 4. of Definition 4 and property 5. of Definition 5, and then that \(S/\ker (f)\) is actually an inverse semigroup with apartness. So, we only have to prove that the \({{\,\mathrm{coker}\,}}(f)\) is cocompatible w.r.t. the inversion and that \(\ker (f)\) is compatible w.r.t. the inversion. Indeed, \(f(a^{1})\cong _T f(a^{1}aa^{1})\cong _T f(a^{1})f(a)f(a^{1})\), and then immediately follows \(f(a)^{1}\cong _T f(a^{1})\). Now we can prove that \({{\,\mathrm{coker}\,}}(f)\) is an Icocongruence. Let \(a,b\in S\) be such that \((a^{1},b^{1})\in {{\,\mathrm{coker}\,}}(f)\). Then, by definition, we get \(f(a^{1})\ncong _T f(b^{1})\) and, by the above observation, \(f(a)^{1}\ncong _T f(b)^{1}\). As T is an inverse semigroup with apartness, from condition 3(b) of Definition 4, it follows \(f(a)\ncong _T f(b)\), and then \((a,b)\in {{\,\mathrm{coker}\,}}(f)\). Now, let \(a,b\in S\) be such that \((a^{1},b^{1})\in \ker (f)\). By definition, we have \(f(a^{1})\cong _T f(b^{1})\), and then, again by the above observation, \(f(a)^{1}\cong _T f(b)^{1}\). From the implication (1) of Remark 2, it follows \(f(a)\cong _T f(b)\), and then \((a,b)\in \ker (f)\), as required. \(\square \)
6 Conclusion
Inverse semigroups can be seen as algebraic structures between semigroups and groups and have been proposed as a natural tool in several applications. Since a constructive approach for both groups and semigroups has been considered and constructive mathematics has relevance in applications, it is timely to consider a constructive approach to inverse semigroups as well.
Stating a constructive counterpart of Wagner–Preston Theorem has proved to be more difficult, as we are able to only do so under conditions of relative decidability of equality and apartness on the set of idempotents. However, as noticed in [8], Green’s relations are fundamental tools in the classical structure theory of semigroups but their definitions involve existential quantification which is in general problematic in constructive mathematics. In the classical inverse semigroup theory, Green’s relations can be defined avoiding the existential quantification but still including the equality of idempotents. So, the condition on idempotents could be useful to introduce a good theory of Green’s relations in this framework.
Notes
Acknowledgements
The authors acknowledge the research cooperation project among Department of Mathematics of Politecnico di Milano, Faculty of Science of the University of Novi Sad, and the Department of Mathematics and Computer Science of the University of Maribor. In this framework, Professor Crvenković gave a talk on semigroups with apartness which drew our attention to constructive algebra. The authors thank the referee for constructive comments and recommendations which helped to improve the readability and quality of the paper.
References
 1.Bishop, E.A.: Foundations of Constructive Analysis. McGrawHill, New York (1967)zbMATHGoogle Scholar
 2.Bishop, E.A., Bridges, D.S.: Constructive Analysis, Grundlehren der mathematischen Wissenschaften, vol. 279. Springer, Berlin (1985)Google Scholar
 3.Bridges, D.S., Reeves, S.: Constructive mathematics in theory and programming practice. Philosophia Mathematica 7(3), 65–104 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
 4.Bridges, D.S., Richman, F.: Varieties of Constructive Mathematics. London Mathematical Society Lecture Notes, vol. 97. Cambridge University Press, Cambridge (1987)CrossRefzbMATHGoogle Scholar
 5.Bridges, D.S., Vîţă, L.S.: Techniques in Constructive Analysis. Universitext. Springer, Berlin (2006)zbMATHGoogle Scholar
 6.Bridges, D.S., Vîţă, L.S.: Apartness and Uniformity: A Constructive Development. CiE series on theory and applications of computability. Springer, Berlin (2011)CrossRefzbMATHGoogle Scholar
 7.Crvenković, S., Mitrović, M., Romano, D.: Semigroups with apartness. Math. Log. Q. 59(6), 407–414 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
 8.Crvenković, S., Mitrović, M., Romano, D.: Basic notions of (constructive) semigroups with apartness. Semigroup Forum 92(3), 659–674 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
 9.Green, D.G.: The lattice of congruences on an inverse semigroup. Pac. J. Math. 57(1), 141–152 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
 10.Howie, J.M.: Why study semigroups? Math. Chron. 16, 1–14 (1987)MathSciNetzbMATHGoogle Scholar
 11.Howie, J.M.: Fundamentals of Semigroup Theory. Clarendon Press, Oxford (1995)zbMATHGoogle Scholar
 12.Kripke, S.: Semantical analysis of modal logic I, Normal modal propositional calculi. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 9(5–6), 67–96 (1963)MathSciNetCrossRefzbMATHGoogle Scholar
 13.Lawson, M.V.: Inverse Semigroups: The Theory of Partial Symmetries. World Scientific, Singapore (1999)zbMATHGoogle Scholar
 14.Mines, R., Richman, F., Ruitenburg, W.: A Course of Constructive Algebra. Universitext. Springer, New York (1988)CrossRefzbMATHGoogle Scholar
 15.MartinLöf, Per: Constructive mathematics and computer programming. Philos. Trans. R. Soc. Lond. A 312, 501–518 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
 16.Petrich, M.: Inverse Semigroups. Wiley, New York (1984)zbMATHGoogle Scholar
 17.Petrich, M., Reilly, N.R.: A network of congruences on an inverse semigroup. Trans. Am. Math. Soc. 270, 309–325 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
 18.Preston, G.B.: Inverse semigroups. J. Lond. Math. Soc. 29(4), 396–403 (1954)MathSciNetCrossRefzbMATHGoogle Scholar
 19.Scheiblich, H.E.: Kernels of inverse semigroup homomorphisms. J. Aust. Math. Soc. 18(3), 289–292 (1974)MathSciNetCrossRefzbMATHGoogle Scholar
 20.Troelstra, A., van Dalen, D.: Constructivism in Mathematics. An Introduction. Volume II, Studies in Logic and the Foundations of Mathematics, vol. 123. NorthHolland, Amsterdam (1988)zbMATHGoogle Scholar
 21.Wagner, V.V.: The theory of generalized heaps and generalized groups. Matematicheskii Sbornik. Novaya Seriya 32(3), 545–632 (1953). (in Russian)MathSciNetGoogle Scholar