8.9 A general statement of the encode-decode method

We have used the encode-decode method to characterize the path spacesof various types, including coproducts (\\crefthm:path-coprod), naturalnumbers (\\crefthm:path-nat), truncations (\\crefthm:path-truncation),the circle (\\crefcor:omega-s1), suspensions (\\autorefthm:freudenthal), and pushouts(\\crefthm:van-Kampen). Variants of this technique are used in theproofs of many of the other theorems mentioned in the introduction tothis chapter, such as a direct proof of $\\pi_{n}(\\mathbb{S}^{n})$ , the Blakers–Massey theorem, and the construction of Eilenberg–Mac Lane spaces.While it is tempting to try toabstract the method into a lemma, this is difficult becauseslightly different variants are needed for different problems. Forexample, different variations on the same method can be used tocharacterize a loop space (as in \\crefthm:path-coprod,cor:omega-s1) ora whole path space (as in \\crefthm:path-nat), to give a completecharacterization of a loop space (e.g. $\\Omega^{1}(\\mathbb{S}^{1})$ ) or only tocharacterize some truncation of it (e.g. van Kampen), and to calculatehomotopy groups or to prove that a map is $n$ -connected (e.g. Freudenthal andBlakers–Massey).

However, we can state lemmas for specific variants of the method.The proofs of these lemmas are almost trivial; the main point is toclarify the method by stating them in generality. The simplestcase is using an encode-decode method to characterize the loop space of atype, as in \\crefthm:path-coprod and \\crefcor:omega-s1.

Lemma 8.9.1 (Encode-decode for Loop Spaces).

Given a pointed type $(A,a_{0})$ and a fibration $\\mathsf{code}:A\\to\\mathcal{U}$ , if

1.
$c_{0}:\\mathsf{code}(a_{0})$ ,
2.
$\\mathsf{decode}:\\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)}}}\\mathsf%{code}(x)\\to(a_{0}=x)$ ,
3.
for all $c:\\mathsf{code}(a_{0})$ , $\\mathsf{transport}^{\\mathsf{code}}(\\mathsf{decode}(c),c_{0})=c$ , and
4.
$\\mathsf{decode}(c_{0})=\\mathsf{refl}$ ,

then $(a_{0}=a_{0})$ is equivalent to $\\mathsf{code}(a_{0})$ .

Proof.

Define $\\mathsf{encode}:\\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)}}}(a_{0}=%x)\\to\\mathsf{code}(x)$ by

\\mathsf{encode}_{x}(\\alpha)=\\mathsf{transport}^{\\mathsf{code}}(\\alpha,c_{0}).

We show that $\\mathsf{encode}_{a_{0}}$ and $\\mathsf{decode}_{a_{0}}$ are quasi-inverses.The composition $\\mathsf{encode}_{a_{0}}\\circ\\mathsf{decode}_{a_{0}}$ is immediate byassumption 3. For the other composition, we show

\\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)}}}\\mathchoice{\\prod_{(p:a_{0%}=x)}\\,}{\\mathchoice{{\\textstyle\\prod_{(p:a_{0}=x)}}}{\\prod_{(p:a_{0}=x)}}{%\\prod_{(p:a_{0}=x)}}{\\prod_{(p:a_{0}=x)}}}{\\mathchoice{{\\textstyle\\prod_{(p:a_%{0}=x)}}}{\\prod_{(p:a_{0}=x)}}{\\prod_{(p:a_{0}=x)}}{\\prod_{(p:a_{0}=x)}}}{%\\mathchoice{{\\textstyle\\prod_{(p:a_{0}=x)}}}{\\prod_{(p:a_{0}=x)}}{\\prod_{(p:a_%{0}=x)}}{\\prod_{(p:a_{0}=x)}}}\\mathsf{decode}_{x}(\\mathsf{encode}_{x}p)=p.

By path induction, it suffices to show ${\\mathsf{decode}_{{a_{0}}}(\\mathsf{encode}_{{a_{o}}}\\mathsf{refl})}=\\mathsf{refl}$ .After reducing the $\\mathsf{transport}$ , it suffices to show ${\\mathsf{decode}_{{a_{0}}}(c_{0})}=\\mathsf{refl}$ , which is assumption 4.∎

If a fiberwise equivalence between $(a_{0}=\\mathord{\\hskip 1.0pt\\text{--}\\hskip 1.0pt})$ and $\\mathsf{code}$ is desired,it suffices to strengthen condition (iii) to

\\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)}}}\\mathchoice{\\prod_{(c:%\\mathsf{code}(x))}\\,}{\\mathchoice{{\\textstyle\\prod_{(c:\\mathsf{code}(x))}}}{%\\prod_{(c:\\mathsf{code}(x))}}{\\prod_{(c:\\mathsf{code}(x))}}{\\prod_{(c:\\mathsf{%code}(x))}}}{\\mathchoice{{\\textstyle\\prod_{(c:\\mathsf{code}(x))}}}{\\prod_{(c:%\\mathsf{code}(x))}}{\\prod_{(c:\\mathsf{code}(x))}}{\\prod_{(c:\\mathsf{code}(x))}%}}{\\mathchoice{{\\textstyle\\prod_{(c:\\mathsf{code}(x))}}}{\\prod_{(c:\\mathsf{%code}(x))}}{\\prod_{(c:\\mathsf{code}(x))}}{\\prod_{(c:\\mathsf{code}(x))}}}%\\mathsf{encode}_{x}(\\mathsf{decode}_{x}(c))=c.a

However, to calculate a loop space (e.g. $\\Omega(\\mathbb{S}^{1})$ ), thisstronger assumption is not necessary.

Another variation, which comes up often when calculating homotopygroups, characterizes the truncation of a loop space:

Lemma 8.9.2 (Encode-decode for Truncations of Loop Spaces).

Assume a pointed type $(A,a_{0})$ and a fibration $\\mathsf{code}:A\\to\\mathcal{U}$ , where for every $x$ , $\\mathsf{code}(x)$ is a $k$ -type.Define

\\mathsf{encode}:\\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)}}}%\\mathopen{}\\left\\|a_{0}=x\\right\\|_{k}\\mathclose{}\\to\\mathsf{code}(x).

by truncation recursion (using the factthat $\\mathsf{code}(x)$ is a $k$ -type), mapping $\\alpha:a_{0}=x$ to $\\mathsf{transport}^{\\mathsf{code}}(\\alpha,c_{0})$ . Suppose:

1.
$c_{0}:\\mathsf{code}(a_{0})$ ,
2.
$\\mathsf{decode}:\\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)}}}\\mathsf%{code}(x)\\to\\mathopen{}\\left\\|a_{0}=x\\right\\|_{k}\\mathclose{}$ ,
3.
$\\mathsf{encode}_{a_{0}}(\\mathsf{decode}_{a0}(c))=c$ for all $c:\\mathsf{code}(a_{0})$ , and
4.
$\\mathsf{decode}(c_{0})=\\mathopen{}\\left|\\mathsf{refl}\\right|\\mathclose{}$ .

Then $\\mathopen{}\\left\\|a_{0}=a_{0}\\right\\|_{k}\\mathclose{}$ is equivalent to $\\mathsf{code}(a_{0})$ .

Proof.

That $\\mathsf{decode}\\circ\\mathsf{encode}$ is identity is immediate by 3.To prove $\\mathsf{encode}\\circ\\mathsf{decode}$ , we first do a truncation induction, bywhich it suffices to show

\\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)}}}\\mathchoice{\\prod_{(p:a_{0%}=x)}\\,}{\\mathchoice{{\\textstyle\\prod_{(p:a_{0}=x)}}}{\\prod_{(p:a_{0}=x)}}{%\\prod_{(p:a_{0}=x)}}{\\prod_{(p:a_{0}=x)}}}{\\mathchoice{{\\textstyle\\prod_{(p:a_%{0}=x)}}}{\\prod_{(p:a_{0}=x)}}{\\prod_{(p:a_{0}=x)}}{\\prod_{(p:a_{0}=x)}}}{%\\mathchoice{{\\textstyle\\prod_{(p:a_{0}=x)}}}{\\prod_{(p:a_{0}=x)}}{\\prod_{(p:a_%{0}=x)}}{\\prod_{(p:a_{0}=x)}}}\\mathsf{decode}_{x}(\\mathsf{encode}_{x}(%\\mathopen{}\\left|p\\right|_{k}\\mathclose{}))=\\mathopen{}\\left|p\\right|_{k}%\\mathclose{}.

The truncation induction is allowed because paths in a $k$ -type are a $k$ -type. To show this type, we do a path induction, and after reducingthe $\\mathsf{encode}$ , use assumption 4.∎