# 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. 1.

$c_{0}:\mathsf{code}(a_{0})$,

2. 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. 3.

for all $c:\mathsf{code}(a_{0})$, $\mathsf{transport}^{\mathsf{code}}(\mathsf{decode}(c),c_{0})=c$, and

4. 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. 1.

$c_{0}:\mathsf{code}(a_{0})$,

2. 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. 3.

$\mathsf{encode}_{a_{0}}(\mathsf{decode}_{a0}(c))=c$ for all $c:\mathsf{code}(a_{0})$, and

4. 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

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

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