2.14.1 Lifting equivalences

When working loosely, one might say that a bijection between sets $A$ and $B$ “obviously” induces an isomorphism between semigroupstructures 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$ fromone on $A$ , and moreover show that this derivation is an equivalence ofsemigroup structures. The reason is that $\\mathsf{SemigroupStr}$ is a familyof types, and therefore has an action on paths between types given by $\\mathsf{transport}$ :

\\mathsf{transport}^{\\mathsf{SemigroupStr}}{(\\mathsf{ua}(e))}:\\mathsf{%SemigroupStr}(A)\\to\\mathsf{SemigroupStr}(B).

Moreover, this map is an equivalence, because $\\mathsf{transport}^{C}(\\alpha)$ is always an equivalence with inverse $\\mathsf{transport}^{C}{(\\mathord{{\\alpha}^{-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 usefacts about $\\mathsf{transport}$ proven in the preceding sections tocalculate what it actually does. Let $(m,a)$ be a semigroup structure on $A$ , and we investigate the induced semigroup structure on $B$ given by

\\mathsf{transport}^{\\mathsf{SemigroupStr}}(\\mathsf{ua}(e),(m,a)).

First, because $\\mathsf{SemigroupStr}$ (X) is defined to be a $\\Sigma$ -type, byTheorem 2.7.4 (http://planetmath.org/27sigmatypes#Thmprethm2),

\\mathsf{transport}^{\\mathsf{SemigroupStr}}(\\mathsf{ua}(e),(m,a))=\\begin{%aligned} \\displaystyle\\big{(}&\\displaystyle\\mathsf{transport}^{X\\mapsto(X\\to X%\\to X)}(\\mathsf{ua}(e),m),\\\\&\\displaystyle\\mathsf{transport}^{(X,m)\\mapsto\\mathsf{Assoc}(X,m)}((\\mathsf{%pair}^{\\mathord{=}}(\\mathsf{ua}(e),\\mathsf{refl})),a)\\big{)}\\end{aligned}

(2.14.2)

where $\\mathsf{Assoc}(X,m)$ is the type $\\mathchoice{\\prod_{x,y,z:X}\\,}{\\mathchoice{{\\textstyle\\prod_{(x,y,z:X)}}}{%\\prod_{(x,y,z:X)}}{\\prod_{(x,y,z:X)}}{\\prod_{(x,y,z:X)}}}{\\mathchoice{{%\\textstyle\\prod_{(x,y,z:X)}}}{\\prod_{(x,y,z:X)}}{\\prod_{(x,y,z:X)}}{\\prod_{(x,%y,z:X)}}}{\\mathchoice{{\\textstyle\\prod_{(x,y,z:X)}}}{\\prod_{(x,y,z:X)}}{\\prod_%{(x,y,z:X)}}{\\prod_{(x,y,z:X)}}}m(x,m(y,z))=m(m(x,y),z)$ .That is, the induced semigroup structure consists of an inducedmultiplication operation on $B$

	$\\displaystyle m^{\\prime}:B\\to B\\to B$
	$\\displaystyle m^{\\prime}(b_{1},b_{2}):\\!\\!\\equiv\\mathsf{transport}^{X\\mapsto(X%\\to X\\to X)}(\\mathsf{ua}(e),m)(b_{1},b_{2})$

together with an induced proof that $m^{\\prime}$ is associative. By functionextensionality, it suffices to investigate the behavior of $m^{\\prime}$ whenapplied to arguments $b_{1},b_{2}:B$ . By applying(LABEL:eq:transport-arrow) twice, we have that $m^{\\prime}(b_{1},b_{2})$ is equal to

\\mathsf{transport}^{X\\mapsto X}\\big{(}\\mathsf{ua}(e),m(\\mathsf{transport}^{X%\\mapsto X}(\\mathord{{\\mathsf{ua}(e)}^{-1}},b_{1}),\\mathsf{transport}^{X\\mapstoX%}(\\mathord{{\\mathsf{ua}(e)}^{-1}},b_{2}))\\big{)}.

Then, because $\\mathsf{ua}$ is quasi-inverse to $\\mathsf{transport}^{X\\mapsto X}$ , this is equal to

e(m(\\mathord{{e}^{-1}}(b_{1}),\\mathord{{e}^{-1}}(b_{2}))).

Thus, given two elements of $B$ , the induced multiplication $m^{\\prime}$ sends them to $A$ using the equivalence $e$ , multiplies them in $A$ , andthen 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 theinduced proof that $m^{\\prime}$ is associative (the second component of the pairin (2.14.2)) is equal to a function sending $b_{1},b_{2},b_{3}:B$ to a path given by the following steps:

$\\displaystyle m^{\\prime}(m^{\\prime}(b_{1},b_{2}),b_{3})$	$\\displaystyle=e(m(\\mathord{{e}^{-1}}(m^{\\prime}(b_{1},b_{2})),\\mathord{{e}^{-1%}}(b_{3})))$	(2.14.3)
	$\\displaystyle=e(m(\\mathord{{e}^{-1}}(e(m(\\mathord{{e}^{-1}}(b_{1}),\\mathord{{e%}^{-1}}(b_{2})))),\\mathord{{e}^{-1}}(b_{3})))$
	$\\displaystyle=e(m(m(\\mathord{{e}^{-1}}(b_{1}),\\mathord{{e}^{-1}}(b_{2})),%\\mathord{{e}^{-1}}(b_{3})))$
	$\\displaystyle=e(m(\\mathord{{e}^{-1}}(b_{1}),m(\\mathord{{e}^{-1}}(b_{2}),%\\mathord{{e}^{-1}}(b_{3}))))$
	$\\displaystyle=e(m(\\mathord{{e}^{-1}}(b_{1}),\\mathord{{e}^{-1}}(e(m(\\mathord{{e%}^{-1}}(b_{2}),\\mathord{{e}^{-1}}(b_{3}))))))$
	$\\displaystyle=e(m(\\mathord{{e}^{-1}}(b_{1}),\\mathord{{e}^{-1}}(m^{\\prime}(b_{2%},b_{3}))))$
	$\\displaystyle=m^{\\prime}(b_{1},m^{\\prime}(b_{2},b_{3})).$

These steps use the proof $a$ that $m$ is associative and the inverselaws for $e$ . From an algebra perspective, it may seem strange toinvestigate the identity of a proof that an operation is associative,but this makes sense if we think of $A$ and $B$ as general spaces, withnon-trivial homotopies between paths. In http://planetmath.org/node/87576Chapter 3, we willintroduce the notion of a set, which is a type with only trivialhomotopies, and if we consider semigroup structures on sets, then anytwo such associativity proofs are automatically equal.