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 $\mathrm{𝖲𝖾𝗆𝗂𝗀𝗋𝗈𝗎𝗉𝖲𝗍𝗋}$ is a family of types, and therefore has an action on paths between types given by $\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}$:

$${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖲𝖾𝗆𝗂𝗀𝗋𝗈𝗎𝗉𝖲𝗍𝗋}}(\mathrm{𝗎𝖺}(e)):\mathrm{𝖲𝖾𝗆𝗂𝗀𝗋𝗈𝗎𝗉𝖲𝗍𝗋}(A)\to \mathrm{𝖲𝖾𝗆𝗂𝗀𝗋𝗈𝗎𝗉𝖲𝗍𝗋}(B).$$

Moreover, this map is an equivalence, because ${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^C(\alpha )$ is always an equivalence with inverse ${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^C({\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 $\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}$ 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

$${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖲𝖾𝗆𝗂𝗀𝗋𝗈𝗎𝗉𝖲𝗍𝗋}}(\mathrm{𝗎𝖺}(e),(m,a)).$$

First, because $\mathrm{𝖲𝖾𝗆𝗂𝗀𝗋𝗈𝗎𝗉𝖲𝗍𝗋}$(X) is defined to be a $\mathrm{\Sigma }$-type, by Theorem 2.7.4 (http://planetmath.org/27sigmatypes#Thmprethm2),

(2.14.2)

where $\mathrm{𝖠𝗌𝗌𝗈𝖼}(X,m)$ is the type ${\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$

$m^{\prime }:B\to B\to B$

$m^{\prime }(b_1,b_2):\equiv {\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{X\mapsto (X\to X\to X)}(\mathrm{𝗎𝖺}(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

$${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{X\mapsto X}(\mathrm{𝗎𝖺}(e),m({\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{X\mapsto X}(\mathrm{𝗎𝖺}{(e)}^{-1},b_1),{\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{X\mapsto X}(\mathrm{𝗎𝖺}{(e)}^{-1},b_2))).$$

Then, because $\mathrm{𝗎𝖺}$ is quasi-inverse to ${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{X\mapsto X}$, this is equal to

$$e(m(e^{-1}(b_1),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:

$m^{\prime }(m^{\prime }(b_1,b_2),b_3)$ $=e(m(e^{-1}(m^{\prime }(b_1,b_2)),e^{-1}(b_3)))$ (2.14.3)

$=e(m(e^{-1}(e(m(e^{-1}(b_1),e^{-1}(b_2)))),e^{-1}(b_3)))$

$=e(m(m(e^{-1}(b_1),e^{-1}(b_2)),e^{-1}(b_3)))$

$=e(m(e^{-1}(b_1),m(e^{-1}(b_2),e^{-1}(b_3))))$

$=e(m(e^{-1}(b_1),e^{-1}(e(m(e^{-1}(b_2),e^{-1}(b_3))))))$

$=e(m(e^{-1}(b_1),e^{-1}(m^{\prime }(b_2,b_3))))$

$=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