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),
(2.14.2) |
where is the type .
That is, the induced semigroup structure consists of an induced
multiplication operation
on
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:
(2.14.3) | ||||
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 |
---|---|
\metatable |