2.4 Homotopies and Equivalences

So far, we have seen how the identity type x=Ay can be regarded as a type of identifications, paths, or equivalences between two elements x and y of a type A. 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 interpretationMathworldPlanetmathPlanetmath, this suggests that two functions f and g (perhaps dependently typed) should be the same if the type (x:A)(f(x)=g(x)) is inhabited. Under the homotopical interpretation, this dependent function type consists of continuousPlanetmathPlanetmath paths or functorial equivalences, and thus may be regarded as the type of homotopiesMathworldPlanetmathPlanetmath or of natural isomorphisms.We will adopt the topological terminology for this.

Definition 2.4.1.

Let f,g:(x:A)P(x) be two sectionsPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath of a type family P:AU. A homotopy from f to g is a dependent function of type


Note that a homotopy is not the same as an identification (f=g). However, in §2.9 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom) we will introduce an axiom making homotopies and identifications “equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath”.

The following proofs are left to the reader.

Lemma 2.4.2.

Homotopy is an equivalence relation on each function type AB. That is, we have elements of the types


Just as functions in type theoryPlanetmathPlanetmath are automatically “functorsMathworldPlanetmath”, homotopies are automatically “natural transformations”, in the following sense. Recall that for f:AB and p:x=Ay, we may write f(p) to mean 𝖺𝗉f(p).

Lemma 2.4.3.

Suppose H:fg is a homotopy between functions f,g:AB and let p:x=Ay. Then we have


We may also draw this as a commutative diagramMathworldPlanetmath:




By inductionMathworldPlanetmath, we may assume p is 𝗋𝖾𝖿𝗅x. Since 𝖺𝗉f and 𝖺𝗉g compute on reflexivityMathworldPlanetmath, in this case what we must show is


But this follows since both sides are equal to H(x). ∎

Corollary 2.4.4.

Let H:fidA be a homotopy, with f:AA. Then for any x:A we have


Here f(x) denotes the ordinary application of f to x, while f(H(x)) denotes 𝖺𝗉f(H(x)).


By naturality of H, the following diagram of paths commutes:



That is, f(Hx)\centerdotHx=H(fx)\centerdotHx. We can now whisker by (Hx)-1 to cancel Hx, 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 f:AB is an isomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath if there is a function g:BA such that both composites fg and gf are pointwise equal to the identityPlanetmathPlanetmathPlanetmathPlanetmath, i.e. such that fg𝗂𝖽B and gf𝗂𝖽A. A homotopical perspective suggests that this should be called a homotopy equivalenceMathworldPlanetmathPlanetmath, and from a categorical one, it should be called an equivalence of (higher) groupoidsPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath. However, when doing proof-relevant mathematics, the corresponding type

g:BA((fg𝗂𝖽B)×(gf𝗂𝖽A)) (2.4.5)

is poorly behaved. For instance, for a single function f:AB 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 adjointPlanetmathPlanetmath equivalences rather than plain equivalences.) For this reason, we give (2.4.5) the following historically accurate, but slightly derogatory-sounding name instead.

Definition 2.4.6.

For a function f:AB, a quasi-inversePlanetmathPlanetmath of f is a triple (g,α,β) consisting of a function g:BA and homotopies α:fgidB and β:gfidA.

Thus, (2.4.5) is the type of quasi-inverses of f; we may denote it by 𝗊𝗂𝗇𝗏(f).

Example 2.4.7.

The identity function idA:AA has a quasi-inverse given by idA itself, together with homotopies defined by α(y):refly and β(x):reflx.

Example 2.4.8.

For any p:x=Ay and z:A, the functions

(p\centerdot) :(y=Az)(x=Az)  𝑎𝑛𝑑
(\centerdotp) :(z=Ax)(z=Ay)

have quasi-inverses given by (p-1\centerdot) and (\centerdotp-1), respectively; see http://planetmath.org/node/87637Exercise 2.6.

Example 2.4.9.

For any p:x=Ay and P:AU, the function


has a quasi-inverse given by transportP(p-1,); 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 A and B “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 𝗂𝗌𝖾𝗊𝗎𝗂𝗏(f) with the following properties:

  1. 1.

    For each f:AB there is a function 𝗊𝗂𝗇𝗏(f)𝗂𝗌𝖾𝗊𝗎𝗂𝗏(f).

  2. 2.

    Similarly, for each f we have 𝗂𝗌𝖾𝗊𝗎𝗂𝗏(f)𝗊𝗂𝗇𝗏(f); thus the two are logically equivalent (see §1.11 (http://planetmath.org/111propositionsastypes)).

  3. 3.

    For any two inhabitants e1,e2:𝗂𝗌𝖾𝗊𝗎𝗂𝗏(f) we have e1=e2.

In http://planetmath.org/node/87577Chapter 4 we will see that there are many different definitions of 𝗂𝗌𝖾𝗊𝗎𝗂𝗏(f) 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:

𝗂𝗌𝖾𝗊𝗎𝗂𝗏(f):(g:BA(fg𝗂𝖽B))×(h:BA(hf𝗂𝖽A)). (2.4.10)

We can show 1 and 2 for this definition now. A function 𝗊𝗂𝗇𝗏(f)𝗂𝗌𝖾𝗊𝗎𝗂𝗏(f) is easy to define by taking (g,α,β) to (g,α,g,β). In the other direction, given (g,α,h,β), let γ be the composite homotopy


and let β:gf𝗂𝖽A be obtained from γ and β. Then (g,α,β):𝗊𝗂𝗇𝗏(f).

Property 3 for this definition is not too hard to prove either, but it requires identifying the identity types of cartesian productsMathworldPlanetmath 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 “f is an equivalence”, and that we can prove f 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 A to B is defined to be a function f:AB together with an inhabitant of 𝗂𝗌𝖾𝗊𝗎𝗂𝗏(f), i.e. a proof that it is an equivalence. We write (AB) for the type of equivalences from A to B, i.e. the type

(AB):f:AB𝗂𝗌𝖾𝗊𝗎𝗂𝗏(f). (2.4.11)

Property 3 above will ensure that if two equivalences are equal as functions (that is, the underlying elements of AB 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:

Lemma 2.4.12.

Type equivalence is an equivalence relation on U. More specifically:

  1. 1.

    For any A, the identity function 𝗂𝖽A is an equivalence; hence AA.

  2. 2.

    For any f:AB, we have an equivalence f-1:BA.

  3. 3.

    For any f:AB and g:BC, we have gf:AC.


The identity function is clearly its own quasi-inverse; hence it is an equivalence.

If f:AB is an equivalence, then it has a quasi-inverse, say f-1:BA. Then f is also a quasi-inverse of f-1, so f-1 is an equivalence BA.

Finally, given f:AB and g:BC with quasi-inverses f-1 and g-1, say, then for any a:A we have f-1g-1gfa=f-1fa=a, and for any c:C we have gff-1g-1c=gg-1c=c. Thus f-1g-1 is a quasi-inverse to gf, hence the latter is an equivalence. ∎

Title 2.4 Homotopies and Equivalences