# 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}^{\beta \x80\xb2},{a}^{\beta \x80\xb2})$, by Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1), the type of paths
$(A,m,a){=}_{\mathrm{\pi \x9d\x96\xb2\pi \x9d\x96\u038e\pi \x9d\x97\x86\pi \x9d\x97\x82\pi \x9d\x97\x80\pi \x9d\x97\x8b\pi \x9d\x97\x88\pi \x9d\x97\x8e\pi \x9d\x97\x89}}(B,{m}^{\beta \x80\xb2},{a}^{\beta \x80\xb2})$
is equal to the type of pairs

${p}_{1}$ | $:A{=}_{\mathrm{\pi \x9d\x92\xb0}}B\mathit{\beta \x80\x83\beta \x80\x83}\text{and}$ | ||

${p}_{2}$ | $:{\mathrm{\pi \x9d\x97\x8d\pi \x9d\x97\x8b\pi \x9d\x96\u038a\pi \x9d\x97\x87\pi \x9d\x97\x8c\pi \x9d\x97\x89\pi \x9d\x97\x88\pi \x9d\x97\x8b\pi \x9d\x97\x8d}}^{\mathrm{\pi \x9d\x96\xb2\pi \x9d\x96\u038e\pi \x9d\x97\x86\pi \x9d\x97\x82\pi \x9d\x97\x80\pi \x9d\x97\x8b\pi \x9d\x97\x88\pi \x9d\x97\x8e\pi \x9d\x97\x89\pi \x9d\x96\xb2\pi \x9d\x97\x8d\pi \x9d\x97\x8b}}\beta \x81\u2019({p}_{1},(m,a))=({m}^{\beta \x80\xb2},{a}^{\beta \x80\xb2}).$ |

By univalence, ${p}_{1}$ is $\mathrm{\pi \x9d\x97\x8e\pi \x9d\x96\u038a}\beta \x81\u2019(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 $\mathrm{\pi \x9d\x96\xb2\pi \x9d\x96\u038e\pi \x9d\x97\x86\pi \x9d\x97\x82\pi \x9d\x97\x80\pi \x9d\x97\x8b\pi \x9d\x97\x88\pi \x9d\x97\x8e\pi \x9d\x97\x89\pi \x9d\x96\xb2\pi \x9d\x97\x8d\pi \x9d\x97\x8b}$, ${p}_{2}$ is equivalent^{} to a pair
of proofs, the first of which shows that

$$\underset{{y}_{1},{y}_{2}:B}{\beta \x88\x8f}e\beta \x81\u2019(m\beta \x81\u2019({e}^{-1}\beta \x81\u2019({y}_{1}),{e}^{-1}\beta \x81\u2019({y}_{2})))={m}^{\beta \x80\xb2}\beta \x81\u2019({y}_{1},{y}_{2})$$ |

and the second of which shows that ${a}^{\beta \x80\xb2}$ 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

$$\underset{{x}_{1},{x}_{2}:A}{\beta \x88\x8f}e\beta \x81\u2019(m\beta \x81\u2019({x}_{1},{x}_{2}))={m}^{\beta \x80\xb2}\beta \x81\u2019(e\beta \x81\u2019({x}_{2}),e\beta \x81\u2019({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}^{\beta \x80\xb2}$). A similar rearrangement is possible for the equation relating
$a$ and ${a}^{\beta \x80\xb2}$. 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}^{\beta \x80\xb2}$ 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 |