2.14.1 Lifting equivalences

When working loosely, one might say that a bijection between sets A and B β€œobviously” induces an isomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath between semigroup structuresMathworldPlanetmath on A and semigroup structures on B. With univalence, this is indeed obvious, because given an equivalence between types A and B, we can automatically derive a semigroup structure on B from one on A, and moreover show that this derivationPlanetmathPlanetmath is an equivalence of semigroup structures. The reason is that π–²π–Ύπ—†π—‚π—€π—‹π—ˆπ—Žπ—‰π–²π—π—‹Β is a family of types, and therefore has an action on paths between types given by π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—:


Moreover, this map is an equivalence, because π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—C⁒(Ξ±) is always an equivalence with inverseMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—C⁒(Ξ±-1), see Lemma 2.3.9 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem6),Lemma 2.1.4 (http://planetmath.org/21typesarehighergroupoids#Thmprelem3).

While the univalence axiom ensures that this map exists, we need to use facts about π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π— proven in the preceding sectionsPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to calculate what it actually does. Let (m,a) be a semigroup structure on A, and we investigate the induced semigroup structure on B given by


First, because π–²π–Ύπ—†π—‚π—€π—‹π—ˆπ—Žπ—‰π–²π—π—‹(X) is defined to be a Ξ£-type, by TheoremMathworldPlanetmath 2.7.4 (http://planetmath.org/27sigmatypes#Thmprethm2),

π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—π–²π–Ύπ—†π—‚π—€π—‹π—ˆπ—Žπ—‰π–²π—π—‹β’(π—Žπ–Ίβ’(e),(m,a))=(π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—X↦(Xβ†’Xβ†’X)⁒(π—Žπ–Ίβ’(e),m),π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—(X,m)β†¦π– π—Œπ—Œπ—ˆπ–Όβ’(X,m)((𝗉𝖺𝗂𝗋=(π—Žπ–Ί(e),𝗋𝖾𝖿𝗅)),a)) (2.14.2)

where π– π—Œπ—Œπ—ˆπ–Όβ’(X,m) is the type ∏(x,y,z:X)m⁒(x,m⁒(y,z))=m⁒(m⁒(x,y),z). That is, the induced semigroup structure consists of an induced multiplicationPlanetmathPlanetmath operationMathworldPlanetmath on B


together with an induced proof that mβ€² is associative. By function extensionality, it suffices to investigate the behavior of mβ€² when applied to arguments b1,b2:B. By applying (LABEL:eq:transport-arrow) twice, we have that m′⁒(b1,b2) is equal to


Then, because π—Žπ–Ί is quasi-inversePlanetmathPlanetmath to π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—X↦X, this is equal to


Thus, given two elements of B, the induced multiplication mβ€² sends them to A using the equivalence e, multiplies them in A, and then brings the result back to B by e, just as one would expect.

Moreover, though we do not show the proof, one can calculate that the induced proof that mβ€² is associative (the second component of the pair in (2.14.2)) is equal to a function sending b1,b2,b3:B to a path given by the following steps:

m′⁒(m′⁒(b1,b2),b3) =e⁒(m⁒(e-1⁒(m′⁒(b1,b2)),e-1⁒(b3))) (2.14.3)

These steps use the proof a that m is associative and the inverse laws for e. From an algebraPlanetmathPlanetmathPlanetmath perspective, it may seem strange to investigate the identity of a proof that an operation is associative, but this makes sense if we think of A and B as general spaces, with non-trivial homotopies between paths. In http://planetmath.org/node/87576Chapter 3, we will introduce the notion of a set, which is a type with only trivial homotopies, and if we consider semigroup structures on sets, then any two such associativity proofs are automatically equal.

Title 2.14.1 Lifting equivalences