2.4 Homotopies and Equivalences

So far, we have seen how the identity type $x=_{A}y$ 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 interpretation, this suggests that two functions $f$ and $g$ (perhaps dependently typed) should be the same if the type $\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}(f(x)=g(x))$ 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.

Definition 2.4.1.

Let $f,g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(% x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}P(x)$ be two sections of a type family $P:A\to\mathcal{U}$ . A homotopy from $f$ to $g$ is a dependent function of type

(f\sim g):\!\!\equiv\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(% x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle% \prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}(f(x)=g% (x)).

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 “equivalent”.

The following proofs are left to the reader.

Lemma 2.4.2.

Homotopy is an equivalence relation on each function type $A\to B$ . That is, we have elements of the types

	$\displaystyle\mathchoice{\prod_{f:A\to B}\,}{\mathchoice{{\textstyle\prod_{(f:% A\to B)}}}{\prod_{(f:A\to B)}}{\prod_{(f:A\to B)}}{\prod_{(f:A\to B)}}}{% \mathchoice{{\textstyle\prod_{(f:A\to B)}}}{\prod_{(f:A\to B)}}{\prod_{(f:A\to B% )}}{\prod_{(f:A\to B)}}}{\mathchoice{{\textstyle\prod_{(f:A\to B)}}}{\prod_{(f% :A\to B)}}{\prod_{(f:A\to B)}}{\prod_{(f:A\to B)}}}(f\sim f)$
	$\displaystyle\mathchoice{\prod_{f,g:A\to B}\,}{\mathchoice{{\textstyle\prod_{(% f,g:A\to B)}}}{\prod_{(f,g:A\to B)}}{\prod_{(f,g:A\to B)}}{\prod_{(f,g:A\to B)% }}}{\mathchoice{{\textstyle\prod_{(f,g:A\to B)}}}{\prod_{(f,g:A\to B)}}{\prod_% {(f,g:A\to B)}}{\prod_{(f,g:A\to B)}}}{\mathchoice{{\textstyle\prod_{(f,g:A\to B% )}}}{\prod_{(f,g:A\to B)}}{\prod_{(f,g:A\to B)}}{\prod_{(f,g:A\to B)}}}(f\sim g% )\to(g\sim f)$
	$\displaystyle\mathchoice{\prod_{f,g,h:A\to B}\,}{\mathchoice{{\textstyle\prod_% {(f,g,h:A\to B)}}}{\prod_{(f,g,h:A\to B)}}{\prod_{(f,g,h:A\to B)}}{\prod_{(f,g% ,h:A\to B)}}}{\mathchoice{{\textstyle\prod_{(f,g,h:A\to B)}}}{\prod_{(f,g,h:A% \to B)}}{\prod_{(f,g,h:A\to B)}}{\prod_{(f,g,h:A\to B)}}}{\mathchoice{{% \textstyle\prod_{(f,g,h:A\to B)}}}{\prod_{(f,g,h:A\to B)}}{\prod_{(f,g,h:A\to B% )}}{\prod_{(f,g,h:A\to B)}}}(f\sim g)\to(g\sim h)\to(f\sim h).$

Just as functions in type theory are automatically “functors”, homotopies are automatically “natural transformations”, in the following sense. Recall that for $f:A\to B$ and $p:x=_{A}y$ , we may write ${f}\mathopen{}\left({p}\right)\mathclose{}$ to mean $\mathsf{ap}_{f}(p)$ .

Lemma 2.4.3.

Suppose $H:f\sim g$ is a homotopy between functions $f,g:A\to B$ and let $p:x=_{A}y$ . Then we have

H(x)\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}{g}\mathopen{}\left({p}\right)\mathclose{}={f}\mathopen{}% \left({p}\right)\mathclose{}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}H(y).

We may also draw this as a commutative diagram:

\includegraphics

HoTT_fig_2.4.1.png

Proof.

By induction, we may assume $p$ is $\mathsf{refl}_{x}$ . Since $\mathsf{ap}_{f}$ and $\mathsf{ap}_{g}$ compute on reflexivity, in this case what we must show is

H(x)\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}\mathsf{refl}_{g(x)}=\mathsf{refl}_{f(x)}\mathchoice{% \mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.1% 5pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}% }}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}H(x).

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

Corollary 2.4.4.

Let $H:f\sim\mathsf{id}_{A}$ be a homotopy, with $f:A\to A$ . Then for any $x : A$ we have

H(f(x))={f}\mathopen{}\left({H(x)}\right)\mathclose{}.

Here $f(x)$ denotes the ordinary application of $f$ to $x$ , while ${f}\mathopen{}\left({H(x)}\right)\mathclose{}$ denotes $\mathsf{ap}_{f}(H(x))$ .

Proof.

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

\includegraphics

HoTT_fig_2.4.2.png

That is, ${f}\mathopen{}\left({Hx}\right)\mathclose{}\mathchoice{\mathbin{\raisebox{2.15% pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}Hx=H(fx)\mathchoice{\mathbin{% \raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$% \centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{% \mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}Hx$ . We can now whisker by $\mathord{{(Hx)}^{-1}}$ to cancel $H x$ , obtaining

{f}\mathopen{}\left({Hx}\right)\mathclose{}={f}\mathopen{}\left({Hx}\right)% \mathclose{}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}% }{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}Hx\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathord{{(Hx)}^{-1}}=H(fx)\mathchoice{% \mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.1% 5pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}% }}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}Hx% \mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}\mathord{{(Hx)}^{-1}}=H(fx)

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:A\to B$ is an isomorphism if there is a function $g:B\to A$ such that both composites $f\circ g$ and $g\circ f$ are pointwise equal to the identity, i.e. such that $f\circ g\sim\mathsf{id}_{B}$ and $g\circ f\sim\mathsf{id}_{A}$ . 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

\mathchoice{\sum_{g:B\to A}\,}{\mathchoice{{\textstyle\sum_{(g:B\to A)}}}{\sum% _{(g:B\to A)}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}}{\mathchoice{{\textstyle% \sum_{(g:B\to A)}}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}}{% \mathchoice{{\textstyle\sum_{(g:B\to A)}}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)% }}{\sum_{(g:B\to A)}}}\big{(}(f\circ g\sim\mathsf{id}_{B})\times(g\circ f\sim% \mathsf{id}_{A})\big{)}

(2.4.5)

is poorly behaved. For instance, for a single function $f:A\to B$ 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.

Definition 2.4.6.

For a function $f:A\to B$ , a quasi-inverse of $f$ is a triple $(g,\alpha,\beta)$ consisting of a function $g:B\to A$ and homotopies $\alpha:f\circ g\sim\mathsf{id}_{B}$ and $\beta:g\circ f\sim\mathsf{id}_{A}$ .

Thus, (2.4.5) is the type of quasi-inverses of $f$ ; we may denote it by $\mathsf{qinv}(f)$ .

Example 2.4.7.

The identity function $\mathsf{id}_{A}:A\to A$ has a quasi-inverse given by $\mathsf{id}_{A}$ itself, together with homotopies defined by $\alpha(y):\!\!\equiv\mathsf{refl}_{y}$ and $\beta(x):\!\!\equiv\mathsf{refl}_{x}$ .

Example 2.4.8.

For any $p:x=_{A}y$ and $z : A$ , the functions

	$\displaystyle(p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot% $}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$	$\displaystyle:(y=_{A}z)\to(x=_{A}z)\qquad\text{and}$
	$\displaystyle(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\mathchoice{\mathbin{% \raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$% \centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{% \mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}p)$	$\displaystyle:(z=_{A}x)\to(z=_{A}y)$

have quasi-inverses given by $(\mathord{{p}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$ and $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\mathchoice{\mathbin{\raisebox{2.1% 5pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathord{{p}^{-1}})$ , respectively; see http://planetmath.org/node/87637Exercise 2.6.

Example 2.4.9.

For any $p:x=_{A}y$ and $P:A\to\mathcal{U}$ , the function

\mathsf{transport}^{P}(p,\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}):P(x)\to P% (y)

has a quasi-inverse given by $\mathsf{transport}^{P}(\mathord{{p}^{-1}},\mathord{\hskip 1.0pt\text{--}\hskip 1% .0pt})$ ; 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 $\mathsf{isequiv}(f)$ with the following properties:

1.

For each $f:A\to B$ there is a function $\mathsf{qinv}(f)\to\mathsf{isequiv}(f)$ .
2.

Similarly, for each $f$ we have $\mathsf{isequiv}(f)\to\mathsf{qinv}(f)$ ; thus the two are logically equivalent (see §1.11 (http://planetmath.org/111propositionsastypes)).
3.

For any two inhabitants $e_{1},e_{2}:\mathsf{isequiv}(f)$ we have $e_{1}=e_{2}$ .

In http://planetmath.org/node/87577Chapter 4 we will see that there are many different definitions of $\mathsf{isequiv}(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:

\mathsf{isequiv}(f)\;:\!\!\equiv\;\Bigl{(}\mathchoice{\sum_{g:B\to A}\,}{% \mathchoice{{\textstyle\sum_{(g:B\to A)}}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)% }}{\sum_{(g:B\to A)}}}{\mathchoice{{\textstyle\sum_{(g:B\to A)}}}{\sum_{(g:B% \to A)}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}}{\mathchoice{{\textstyle\sum_{(% g:B\to A)}}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}}(f\circ g% \sim\mathsf{id}_{B})\Bigr{)}\times\Bigl{(}\mathchoice{\sum_{h:B\to A}\,}{% \mathchoice{{\textstyle\sum_{(h:B\to A)}}}{\sum_{(h:B\to A)}}{\sum_{(h:B\to A)% }}{\sum_{(h:B\to A)}}}{\mathchoice{{\textstyle\sum_{(h:B\to A)}}}{\sum_{(h:B% \to A)}}{\sum_{(h:B\to A)}}{\sum_{(h:B\to A)}}}{\mathchoice{{\textstyle\sum_{(% h:B\to A)}}}{\sum_{(h:B\to A)}}{\sum_{(h:B\to A)}}{\sum_{(h:B\to A)}}}(h\circ f% \sim\mathsf{id}_{A})\Bigr{)}.

(2.4.10)

We can show 1 and 2 for this definition now. A function $\mathsf{qinv}(f)\to\mathsf{isequiv}(f)$ is easy to define by taking $(g,\alpha,\beta)$ to $(g,\alpha,g,\beta)$ . In the other direction, given $(g,\alpha,h,\beta)$ , let $\gamma$ be the composite homotopy

g\overset{\beta}{\sim}h\circ f\circ g\overset{\alpha}{\sim}h

and let $\beta^{\prime}:g\circ f\sim\mathsf{id}_{A}$ be obtained from $\gamma$ and $\beta$ . Then $(g,\alpha,\beta^{\prime}):\mathsf{qinv}(f)$ .

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 “ $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:A\to B$ together with an inhabitant of $\mathsf{isequiv}(f)$ , i.e. a proof that it is an equivalence. We write $(A\simeq B)$ for the type of equivalences from $A$ to $B$ , i.e. the type

(A\simeq B):\!\!\equiv\mathchoice{\sum_{f:A\to B}\,}{\mathchoice{{\textstyle% \sum_{(f:A\to B)}}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}}{% \mathchoice{{\textstyle\sum_{(f:A\to B)}}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)% }}{\sum_{(f:A\to B)}}}{\mathchoice{{\textstyle\sum_{(f:A\to B)}}}{\sum_{(f:A% \to B)}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}}\mathsf{isequiv}(f).

(2.4.11)

Property 3 above will ensure that if two equivalences are equal as functions (that is, the underlying elements of $A\to B$ 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 $\mathcal{U}$ . More specifically:

1.

For any $A$ , the identity function $\mathsf{id}_{A}$ is an equivalence; hence $A\simeq A$ .
2.

For any $f:A\simeq B$ , we have an equivalence $f^{-1}:B\simeq A$ .
3.

For any $f:A\simeq B$ and $g:B\simeq C$ , we have $g\circ f:A\simeq C$ .

Proof.

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

If $f:A\to B$ is an equivalence, then it has a quasi-inverse, say $f^{-1}:B\to A$ . Then $f$ is also a quasi-inverse of $f^{-1}$ , so $f^{-1}$ is an equivalence $B\to A$ .

Finally, given $f:A\simeq B$ and $g:B\simeq C$ with quasi-inverses $f^{-1}$ and $g^{-1}$ , say, then for any $a : A$ we have $f^{-1}g^{-1}gfa=f^{-1}fa=a$ , and for any $c : C$ we have $gff^{-1}g^{-1}c=gg^{-1}c=c$ . Thus $f^{-1}\circ g^{-1}$ is a quasi-inverse to $g\circ f$ , hence the latter is an equivalence. ∎

Title	2.4 Homotopies and Equivalences
\metatable