2.14.1 Lifting equivalences

When working loosely, one might say that a bijection between sets $A$ and $B$ “obviously” induces an isomorphism        between semigroup structures  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 derivation  is an equivalence of semigroup structures. The reason is that $\mathsf{SemigroupStr}$ is a family of 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 use facts about $\mathsf{transport}$ proven in the preceding sections      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

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

First, because $\mathsf{SemigroupStr}$(X) is defined to be a $\Sigma$-type, by Theorem  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 induced multiplication  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 function extensionality, it suffices to investigate the behavior of $m^{\prime}$ when applied 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\mapsto X% }(\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$, 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^{\prime}$ is associative (the second component of the pair in (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 inverse laws for $e$. From an algebra   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
\metatable