2.14.2 Equality of semigroups

Using the equations for path spaces discussed in the previous sectionsPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, we can investigate when two semigroupsPlanetmathPlanetmath are equal. Given semigroups (A,m,a) and (B,mβ€²,aβ€²), by Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1), the type of paths (A,m,a)=π–²π–Ύπ—†π—‚π—€π—‹π—ˆπ—Žπ—‰(B,mβ€²,aβ€²) is equal to the type of pairs

p1 :A=𝒰B  and
p2 :π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—π–²π–Ύπ—†π—‚π—€π—‹π—ˆπ—Žπ—‰π–²π—π—‹β’(p1,(m,a))=(mβ€²,aβ€²).

By univalence, p1 is π—Žπ–Ίβ’(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 π–²π–Ύπ—†π—‚π—€π—‹π—ˆπ—Žπ—‰π–²π—π—‹, p2 is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to a pair of proofs, the first of which shows that


and the second of which shows that aβ€² is equal to the induced associativity proof constructed from a in 2.14.3 (http://planetmath.org/2141liftingequivalences#S0.E1). But by cancellation of inversesMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath 2.14.2 (http://planetmath.org/2141liftingequivalences#S0.E2X) is equivalent to


This says that e commutes with the binary operationMathworldPlanetmath, in the sense that it takes multiplication in A (i.e.Β m) to multiplication in B (i.e.Β mβ€²). A similar rearrangement is possible for the equation relating a and aβ€². Thus, an equality of semigroups consists exactly of an equivalence on the carrier types that commutes with the semigroup structureMathworldPlanetmath.

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β€² 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 isomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath: a bijection on the carrier sets that preserves the multiplication operationMathworldPlanetmath. 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 conclusionMathworldPlanetmath that equality of semigroups is the same as two mutually inverse homomorphismsMathworldPlanetmathPlanetmathPlanetmath; 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 structuresPlanetmathPlanetmath. 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