8.9 A general statement of the encode-decode method

We have used the encode-decode method to characterize the path spaces of various types, including coproducts (\crefthm:path-coprod), natural numbers (\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 the proofs of many of the other theorems mentioned in the introduction to this 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 to abstract the method into a lemma, this is difficult because slightly different variants are needed for different problems. For example, different variations on the same method can be used to characterize a loop space (as in \crefthm:path-coprod,cor:omega-s1) or a whole path space (as in \crefthm:path-nat), to give a complete characterization of a loop space (e.g. $\Omega^{1}(\mathbb{S}^{1})$ ) or only to characterize some truncation of it (e.g. van Kampen), and to calculate homotopy groups or to prove that a map is $n$ -connected (e.g. Freudenthal and Blakers–Massey).

However, we can state lemmas for specific variants of the method. The proofs of these lemmas are almost trivial; the main point is to clarify the method by stating them in generality. The simplest case is using an encode-decode method to characterize the loop space of a type, 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 by assumption 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})$ ), this stronger assumption is not necessary.

Another variation, which comes up often when calculating homotopy groups, 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 fact that $\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, by which it suffices to show

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 reducing the $\mathsf{encode}$ , use assumption 4. ∎

Title	8.9 A general statement of the encode-decode method
\metatable