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 and , by Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1), the type of pathsis equal to the type of pairs
By univalence, is for some equivalence . ByTheorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1), function extensionality, and the above analysis oftransport in the type family , is equivalent to a pairof proofs, the first of which shows that
and the second of which shows that is equal to the inducedassociativity proof constructed from in2.14.3 (http://planetmath.org/2141liftingequivalences#S0.E1). But by cancellation of inverses2.14.2 (http://planetmath.org/2141liftingequivalences#S0.E2X) is equivalent to
This says that commutes with the binary operation, in the sensethat it takes multiplication in (i.e. ) to multiplication in (i.e. ). A similar rearrangement is possible for the equation relating and . Thus, an equality of semigroups consists exactly of anequivalence on the carrier types that commutes with the semigroupstructure
.
For general types, the proof of associativity is thought of as part ofthe structure of a semigroup. However, if we restrict to set-like types(again, see http://planetmath.org/node/87576Chapter 3), theequation relating and is trivially true. Moreover, in thiscase, an equivalence between sets is exactly a bijection. Thus, we havearrived at a standard definition of a semigroup isomorphism: abijection on the carrier sets that preserves the multiplicationoperation
. It is also possible to use the category-theoretic definitionof isomorphism, by defining a semigroup homomorphism to be a mapthat preserves the multiplication, and arrive at the conclusion
that equality ofsemigroups is the same as two mutually inverse homomorphisms
; but wewill not show the details here; see §9.8 (http://planetmath.org/98thestructureidentityprinciple).
The conclusion is that, thanks to univalence, semigroups are equalprecisely when they are isomorphic as algebraic structures. As we will see in §9.8 (http://planetmath.org/98thestructureidentityprinciple), theconclusion applies more generally: in homotopy type theory, all constructions ofmathematical structures automatically respect isomorphisms, without anytedious proofs or abuse of notation.