2.4 Homotopies and Equivalences
So far, we have seen how the identity type can be regarded as a type of identifications, paths, or equivalences between two elements and of a type . Now we investigate the appropriate notions of “identification” or “sameness” between functions and between types. In §2.9 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom),§2.10 (http://planetmath.org/210universesandtheunivalenceaxiom), we will see that homotopy type theory allows us to identify these with instances of the identity type, but before we can do that we need to understand them in their own right.
Traditionally, we regard two functions as the same if they take equal values on all inputs. Under the propositions-as-types interpretation, this suggests that two functions and (perhaps dependently typed) should be the same if the type is inhabited. Under the homotopical interpretation, this dependent function type consists of continuous paths or functorial equivalences, and thus may be regarded as the type of homotopies or of natural isomorphisms.We will adopt the topological terminology for this.
Let be two sections of a type family . A homotopy from to is a dependent function of type
Note that a homotopy is not the same as an identification . However, in §2.9 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom) we will introduce an axiom making homotopies and identifications “equivalent”.
The following proofs are left to the reader.
Homotopy is an equivalence relation on each function type . That is, we have elements of the types
Suppose is a homotopy between functions and let . Then we have
We may also draw this as a commutative diagram:
Let be a homotopy, with . Then for any we have
Here denotes the ordinary application of to , while denotes .
By naturality of , the following diagram of paths commutes:
That is, . We can now whisker by to cancel , obtaining
as desired (with some associativity paths suppressed). ∎
Of course, like the functoriality of functions (Lemma 2.2.2 (http://planetmath.org/22functionsarefunctors#Thmprelem2)), the equality in Lemma 2.4.3 (http://planetmath.org/24homotopiesandequivalences#Thmprelem2) is a path which satisfies its own coherence laws, and so on.
Moving on to types, from a traditional perspective one may say that a function is an isomorphism if there is a function such that both composites and are pointwise equal to the identity, i.e. such that and . A homotopical perspective suggests that this should be called a homotopy equivalence, and from a categorical one, it should be called an equivalence of (higher) groupoids. However, when doing proof-relevant mathematics, the corresponding type
is poorly behaved. For instance, for a single function there may be multiple unequal inhabitants of (2.4.5). (This is closely related to the observation in higher category theory that often one needs to consider adjoint equivalences rather than plain equivalences.) For this reason, we give (2.4.5) the following historically accurate, but slightly derogatory-sounding name instead.
For a function , a quasi-inverse of is a triple consisting of a function and homotopies and .
Thus, (2.4.5) is the type of quasi-inverses of ; we may denote it by .
The identity function has a quasi-inverse given by itself, together with homotopies defined by and .
For any and , the functions
have quasi-inverses given by and , respectively; see http://planetmath.org/node/87637Exercise 2.6.
For any and , the function
has a quasi-inverse given by ; this follows from Lemma 2.3.9 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem6).
In general, we will only use the word isomorphism (and similar words such as bijection) in the special case when the types and “behave like sets” (see §3.1 (http://planetmath.org/31setsandntypes)). In this case, the type (2.4.5) is unproblematic. We will reserve the word equivalence for an improved notion with the following properties:
For each there is a function .
Similarly, for each we have ; thus the two are logically equivalent (see §1.11 (http://planetmath.org/111propositionsastypes)).
For any two inhabitants we have .
In http://planetmath.org/node/87577Chapter 4 we will see that there are many different definitions of which satisfy these three properties, but that all of them are equivalent. For now, to convince the reader that such things exist, we mention only the easiest such definition:
and let be obtained from and . Then .
Property 3 for this definition is not too hard to prove either, but it requires identifying the identity types of cartesian products and dependent pair types, which we will discuss in §2.6 (http://planetmath.org/26cartesianproducttypes),§2.7 (http://planetmath.org/27sigmatypes). Thus, we postpone it as well; see §4.3 (http://planetmath.org/43biinvertiblemaps). At this point, the main thing to take away is that there is a well-behaved type which we can pronounce as “ is an equivalence”, and that we can prove to be an equivalence by exhibiting a quasi-inverse to it. In practice, this is the most common way to prove that a function is an equivalence.
In accord with the proof-relevant philosophy, an equivalence from to is defined to be a function together with an inhabitant of , i.e. a proof that it is an equivalence. We write for the type of equivalences from to , i.e. the type
Property 3 above will ensure that if two equivalences are equal as functions (that is, the underlying elements of are equal), then they are also equal as equivalences (see §2.7 (http://planetmath.org/27sigmatypes)). Thus, we often abuse notation by denoting an equivalence by the same letter as its underlying function.
We conclude by observing:
Type equivalence is an equivalence relation on . More specifically:
For any , the identity function is an equivalence; hence .
For any , we have an equivalence .
For any and , we have .
The identity function is clearly its own quasi-inverse; hence it is an equivalence.
If is an equivalence, then it has a quasi-inverse, say . Then is also a quasi-inverse of , so is an equivalence .
Finally, given and with quasi-inverses and , say, then for any we have , and for any we have . Thus is a quasi-inverse to , hence the latter is an equivalence. ∎
|Title||2.4 Homotopies and Equivalences|