2.14.1 Lifting equivalences
When working loosely, one might say that a bijection between sets and “obviously” induces an isomorphism between semigroup structures on and semigroup structures on . With univalence, this is indeed obvious, because given an equivalence between types and , we can automatically derive a semigroup structure on from one on , and moreover show that this derivation 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 is always an equivalence with inverse , 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 sections to calculate what it actually does. Let be a semigroup structure on , and we investigate the induced semigroup structure on given by
First, because (X) is defined to be a -type, by Theorem 2.7.4 (http://planetmath.org/27sigmatypes#Thmprethm2),
together with an induced proof that is associative. By function extensionality, it suffices to investigate the behavior of when applied to arguments . By applying (LABEL:eq:transport-arrow) twice, we have that is equal to
Then, because is quasi-inverse to , this is equal to
Thus, given two elements of , the induced multiplication sends them to using the equivalence , multiplies them in , and then brings the result back to by , just as one would expect.
Moreover, though we do not show the proof, one can calculate that the induced proof that is associative (the second component of the pair in (2.14.2)) is equal to a function sending to a path given by the following steps:
These steps use the proof that is associative and the inverse laws for . 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 and 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|