# 2.14.2 Equality of semigroups

Using the equations for path spaces discussed in the previous sections      , we can investigate when two semigroups  are equal. Given semigroups $(A,m,a)$ and $(B,m^{\prime},a^{\prime})$, by Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1), the type of paths $(A,m,a)=_{\mathsf{Semigroup}}(B,m^{\prime},a^{\prime})$ is equal to the type of pairs

 $\displaystyle p_{1}$ $\displaystyle:A=_{\mathcal{U}}B\qquad\text{and}$ $\displaystyle p_{2}$ $\displaystyle:\mathsf{transport}^{\mathsf{SemigroupStr}}(p_{1},(m,a))={(m^{% \prime},a^{\prime})}.$

By univalence, $p_{1}$ is $\mathsf{ua}(e)$ for some equivalence $e$. By Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1), function extensionality, and the above analysis of transport in the type family $\mathsf{SemigroupStr}$, $p_{2}$ is equivalent     to a pair of proofs, the first of which shows that

 $\mathchoice{\prod_{y_{1},y_{2}:B}\,}{\mathchoice{{\textstyle\prod_{(y_{1},y_{2% }:B)}}}{\prod_{(y_{1},y_{2}:B)}}{\prod_{(y_{1},y_{2}:B)}}{\prod_{(y_{1},y_{2}:% B)}}}{\mathchoice{{\textstyle\prod_{(y_{1},y_{2}:B)}}}{\prod_{(y_{1},y_{2}:B)}% }{\prod_{(y_{1},y_{2}:B)}}{\prod_{(y_{1},y_{2}:B)}}}{\mathchoice{{\textstyle% \prod_{(y_{1},y_{2}:B)}}}{\prod_{(y_{1},y_{2}:B)}}{\prod_{(y_{1},y_{2}:B)}}{% \prod_{(y_{1},y_{2}:B)}}}e(m(\mathord{{e}^{-1}}(y_{1}),\mathord{{e}^{-1}}(y_{2% })))=m^{\prime}(y_{1},y_{2})$

and the second of which shows that $a^{\prime}$ is equal to the induced associativity proof constructed from $a$ in 2.14.3 (http://planetmath.org/2141liftingequivalences#S0.E1). But by cancellation of inverses       2.14.2 (http://planetmath.org/2141liftingequivalences#S0.E2X) is equivalent to

 $\mathchoice{\prod_{x_{1},x_{2}:A}\,}{\mathchoice{{\textstyle\prod_{(x_{1},x_{2% }:A)}}}{\prod_{(x_{1},x_{2}:A)}}{\prod_{(x_{1},x_{2}:A)}}{\prod_{(x_{1},x_{2}:% A)}}}{\mathchoice{{\textstyle\prod_{(x_{1},x_{2}:A)}}}{\prod_{(x_{1},x_{2}:A)}% }{\prod_{(x_{1},x_{2}:A)}}{\prod_{(x_{1},x_{2}:A)}}}{\mathchoice{{\textstyle% \prod_{(x_{1},x_{2}:A)}}}{\prod_{(x_{1},x_{2}:A)}}{\prod_{(x_{1},x_{2}:A)}}{% \prod_{(x_{1},x_{2}:A)}}}e(m(x_{1},x_{2}))=m^{\prime}(e(x_{2}),e(x_{2})).$

This says that $e$ commutes with the binary operation  , in the sense that it takes multiplication in $A$ (i.e. $m$) to multiplication in $B$ (i.e. $m^{\prime}$). A similar rearrangement is possible for the equation relating $a$ and $a^{\prime}$. Thus, an equality of semigroups consists exactly of an equivalence on the carrier types that commutes with the semigroup structure  .

For general types, the proof of associativity is thought of as part of the structure of a semigroup. However, if we restrict to set-like types (again, see http://planetmath.org/node/87576Chapter 3), the equation relating $a$ and $a^{\prime}$ is trivially true. Moreover, in this case, an equivalence between sets is exactly a bijection. Thus, we have arrived at a standard definition of a semigroup isomorphism        : a bijection on the carrier sets that preserves the multiplication operation  . It is also possible to use the category-theoretic definition of isomorphism, by defining a semigroup homomorphism to be a map that preserves the multiplication, and arrive at the conclusion  that equality of semigroups is the same as two mutually inverse homomorphisms    ; but we will not show the details here; see §9.8 (http://planetmath.org/98thestructureidentityprinciple).

The conclusion is that, thanks to univalence, semigroups are equal precisely when they are isomorphic as algebraic structures  . As we will see in §9.8 (http://planetmath.org/98thestructureidentityprinciple), the conclusion applies more generally: in homotopy type theory, all constructions of mathematical structures automatically respect isomorphisms, without any tedious proofs or abuse of notation.

Title 2.14.2 Equality of semigroups
\metatable