homotopy.tex

\chapter{Homotopy theory}
\label{cha:homotopy}

\index{acceptance|(}

In this chapter, we develop some homotopy theory within type theory.  We
use the \emph{synthetic approach} to homotopy theory introduced in
\cref{cha:basics}: Spaces, points, paths, and homotopies are basic
notions, which are represented by types and elements of types, particularly
the identity type.  The algebraic structure of paths and homotopies is
represented by the natural $\infty$-groupoid
\index{.infinity-groupoid@$\infty$-groupoid}%
structure on types, which is generated
by the rules for the identity type.  Using higher inductive types, as
introduced in \cref{cha:hits}, we can describe spaces directly by their
universal properties.

\index{synthetic mathematics}%
There are several interesting aspects of this synthetic approach.
First, it combines advantages of concrete models (such as topological
spaces\index{topological!space}
or simplicial sets)\index{simplicial!sets}
with advantages of abstract categorical frameworks
for homotopy theory (such as Quillen model categories).\index{Quillen model category}
 On the one hand,
our proofs feel elementary, and refer concretely to
points, paths, and homotopies in types.  On the other hand, our approach nevertheless abstracts away from
any concrete presentation of these objects --- for example,
associativity of path concatenation is proved by path induction, rather
than by reparametrization of maps $[0,1] \to X$ or by horn-filling conditions.
Type theory seems to be a very convenient way to study the abstract homotopy theory
of $\infty$-groupoids: by using the rules for the identity type, we
can avoid the complicated combinatorics involved in many definitions of
$\infty$-groupoids, and explicate only as much of the
structure as is needed in any particular proof.

The abstract nature of type theory means that our proofs apply automatically in a variety of settings.
In particular, as mentioned previously, homotopy type theory has one interpretation in
Kan\index{Kan complex} simplicial sets\index{simplicial!sets},
which is one model for the homotopy theory of $\infty$-groupoids.  Thus,
our proofs apply to this model, and transferring them along the geometric
realization\index{geometric realization} functor from simplicial sets to topological spaces gives
proofs of corresponding theorems in classical homotopy theory.
However, though the details are work in progress, we can also
interpret type theory in a wide variety of other categories
that look like the category of $\infty$-groupoids, such as
$(\infty,1)$-toposes\index{.infinity1-topos@$(\infty,1)$-topos}.
Thus, proving a result in type theory will show
that it holds in these settings as well.
This sort of extra generality is well-known as a property of ordinary categorical logic:
univalent foundations extends it to homotopy theory as well.

Second, our synthetic approach has suggested new type-theoretic
methods and proofs.  Some of our proofs are fairly
direct transcriptions of classical proofs.  Others have a more
type-theoretic feel, and consist mainly of calculations with
$\infty$-groupoid operations, in a style that is very similar to how
computer scientists use type theory to reason about computer programs.
One thing that seems to have permitted these new proofs is the fact that type theory
emphasizes different aspects of homotopy theory than other approaches:
while tools like path induction and the universal properties of higher
inductives are available in a setting like Kan\index{Kan complex} simplicial sets, type
theory elevates their importance, because they are the \emph{only}
primitive tools available for working with these types.  Focusing on
these tools had led to new descriptions of familiar constructions such
as the universal cover of the circle and the Hopf fibration, using just the
recursion principles for higher inductive types.  These descriptions are
very direct, and many of the proofs in this chapter involve
computational calculations with such fibrations.
\index{mathematics!constructive}%
Another new aspect of our proofs is that they are constructive (assuming
univalence and higher inductives types are constructive); we describe an
application of this to homotopy groups of spheres in
\cref{sec:moreresults}.

\index{mathematics!formalized}%
\indexsee{formalization of mathematics}{mathematics, formalized}%
Third, our synthetic approach is very amenable to computer-checked
proofs in proof assistants\index{proof!assistant} such as \Coq and \Agda.
Almost all of the proofs
described in this chapter have been computer-checked, and many of these
proofs were first given in a proof assistant, and then ``unformalized''
for this book.  The computer-checked proofs are comparable in length and
effort to the informal proofs presented here, and in some cases they are
even shorter and easier to do.

\mentalpause

Before turning to the presentation of our results, we briefly review some
 basic concepts and theorems from homotopy theory for the benefit of the reader who is not familiar with them.
 We also give an overview of the
results proved in this chapter.

\index{classical!homotopy theory|(}%
Homotopy theory is a branch of algebraic topology, and uses tools from abstract algebra,
such as group theory, to investigate properties of spaces.  One question
homotopy theorists investigate is how to tell whether two spaces are the
same, where ``the same'' means \emph{homotopy equivalence}
\index{homotopy!equivalence!topological}%
(continuous
maps back and forth that compose to the identity up to homotopy---this
gives the opportunity to ``correct'' maps that don't exactly compose to
the identity).  One common way to tell whether two spaces are the same
is to calculate \emph{algebraic invariants} associated with a space,
which include its \emph{homotopy groups} and \emph{homology} and
\emph{cohomology groups}.
\index{homology}%
\index{cohomology}%
Equivalent spaces have isomorphic
homotopy/(co)homology groups, so if two spaces have different groups,
then they are not equivalent.  Thus, these algebraic invariants provide
global information about a space, which can be used to tell spaces
apart, and complements the local information provided by notions such as
continuity.  For example, the torus locally looks like the $2$-sphere, but it
has a global difference, because it as a hole in it, and this difference
is visible in the homotopy groups of these two spaces.

The simplest example of a homotopy group is the \emph{fundamental group}
\index{fundamental!group}%
of a space, which is written $\pi_1(X,x_0$): Given a space $X$ and a
point $x_0$ in it, one can make a group whose elements are loops at
$x_0$ (continuous paths from $x_0$ to $x_0$), considered up to homotopy, with the
group operations given by the identity path (standing still), path
concatenation, and path reversal.  For example, the fundamental group of
the $2$-sphere is trivial, but the fundamental group of the torus is not,
which shows that the sphere and the torus are not homotopy equivalent.
The intuition is that every loop on the sphere is homotopic to the
identity, because its inside can be filled in.  In contrast, a loop on
the torus that goes through the donut's hole is not homotopic to the
identity, so there are non-trivial elements in the fundamental group.

\index{homotopy!group}
The \emph{higher homotopy groups} provide additional information about a
space.  Fix a point $x_0$ in $X$, and consider the constant path
$\refl{x_0}$.  Then the homotopy classes of homotopies between $\refl{x_0}$
and itself form a group $\pi_2(X,x_0)$, which tells us something about
the two-dimensional structure of the space.  Then $\pi_3(X,x_0$) is the
group of homotopy classes of homotopies between homotopies, and so on.
One of the basic problems of algebraic topology  is
\emph{calculating the homotopy groups of a space $X$}, which means
giving a group isomorphism between $\pi_k(X,x_0)$ and some more direct
description of a group (e.g., by a multiplication table or
presentation).  Somewhat surprisingly, this is a very difficult
question, even for spaces as simple as the spheres.  As can be seen from
\cref{tab:homotopy-groups-of-spheres}, some patterns emerge in the
higher homotopy groups of spheres, but there is no general formula, and
many homotopy groups of spheres are currently still unknown.

\bgroup
% Colors for the table of homotopy groups of spheres
\definecolor{xA}{\OPTcolormodel}{\OPTcolxA}
\definecolor{xB}{\OPTcolormodel}{\OPTcolxB}
\definecolor{xC}{\OPTcolormodel}{\OPTcolxC}
\definecolor{xD}{\OPTcolormodel}{\OPTcolxD}
\definecolor{xE}{\OPTcolormodel}{\OPTcolxE}
\definecolor{xF}{\OPTcolormodel}{\OPTcolxF}
\definecolor{xG}{\OPTcolormodel}{\OPTcolxG}
\definecolor{xH}{\OPTcolormodel}{\OPTcolxH}
\definecolor{xI}{\OPTcolormodel}{\OPTcolxI}
\definecolor{xJ}{\OPTcolormodel}{\OPTcolxJ}
\definecolor{xK}{\OPTcolormodel}{\OPTcolxK}
\definecolor{xL}{\OPTcolormodel}{\OPTcolxL}
\definecolor{xM}{\OPTcolormodel}{\OPTcolxM}

\newcommand{\cA}{\colorbox{xG}{\hbox to 20pt {\hfil$0$\hfil}}}
\newcommand{\cB}{\colorbox{xH}{\hbox to 20pt {\hfil$\Z$\hfil}}}
\newcommand{\cC}{\colorbox{xI}{\hbox to 20pt {\hfil$\Z_{2}$\hfil}}}
\newcommand{\cD}{\colorbox{xJ}{\hbox to 20pt {\hfil$\Z_{2}$\hfil}}}
\newcommand{\cE}{\colorbox{xK}{\hbox to 20pt {\hfil$\Z_{24}$\hfil}}}
\newcommand{\cF}{\colorbox{xL}{\hbox to 20pt {\hfil$0$\hfil}}}
\newcommand{\cG}{\colorbox{xM}{\hbox to 20pt {\hfil$0$\hfil}}}
\newcommand{\cH}{\colorbox{xF}{\hbox to 20pt {\hfil$0$\hfil}}}
\newcommand{\cI}{\colorbox{xE}{\hbox to 20pt {\hfil$0$\hfil}}}
\newcommand{\cJ}{\colorbox{xD}{\hbox to 20pt {\hfil$0$\hfil}}}
\newcommand{\cK}{\colorbox{xC}{\hbox to 20pt {\hfil$0$\hfil}}}
\newcommand{\cL}{\colorbox{xB}{\hbox to 20pt {\hfil$0$\hfil}}}
\newcommand{\cM}{\colorbox{xA}{\hbox to 20pt {\hfil$0$\hfil}}}

\begin{table}[htb]
\centering\small
\begin{tabular}{p{15pt}>{\centering\arraybackslash}p{\OPTspherescolwidth}>{\centering\arraybackslash}p{\OPTspherescolwidth}>{\centering\arraybackslash}p{\OPTspherescolwidth}>{\centering\arraybackslash}p{\OPTspherescolwidth}>{\centering\arraybackslash}p{\OPTspherescolwidth}>{\centering\arraybackslash}p{\OPTspherescolwidth}>{\centering\arraybackslash}p{\OPTspherescolwidth}>{\centering\arraybackslash}p{\OPTspherescolwidth}>{\centering\arraybackslash}p{\OPTspherescolwidth}}
\toprule
           & $\Sn^0$ & $\Sn^1$ & $\Sn^{2}$ & $\Sn^{3}$ & $\Sn^{4}$ & $\Sn^{5}$ & $\Sn^{6}$ & $\Sn^{7}$ & $\Sn^{8}$ \\ \addlinespace[3pt] \midrule
$\pi_{1}$  & $0$     & $\Z$    & \cA       & \cH       & \cI       & \cJ       & \cK       & \cL       & \cM       \\ \addlinespace[3pt]
$\pi_{2}$  & $0$     & $0$     & \cB       & \cA       & \cH       & \cI       & \cJ       & \cK       & \cL       \\ \addlinespace[3pt]
$\pi_{3}$  & $0$     & $0$     & $\Z$      & \cB       & \cA       & \cH       & \cI       & \cJ       & \cK       \\ \addlinespace[3pt]
$\pi_{4}$  & $0$     & $0$     & $\Z_{2}$  & \cC       & \cB       & \cA       & \cH       & \cI       & \cJ       \\ \addlinespace[3pt]
$\pi_{5}$  & $0$     & $0$     & $\Z_{2}$  & $\Z_{2}$  & \cC       & \cB       & \cA       & \cH       & \cI       \\ \addlinespace[3pt]
$\pi_{6}$  & $0$     & $0$     & $\Z_{12}$ & $\Z_{12}$ & \cD       & \cC       & \cB       & \cA       & \cH       \\ \addlinespace[3pt]
$\pi_{7}$  & $0$     & $0$     & $\Z_{2}$  & $\Z_{2}$  & {\footnotesize $\Z {\times} \Z_{12}$} & \cD & \cC & \cB     & \cA    \\ \addlinespace[3pt]
$\pi_{8}$  & $0$     & $0$     & $\Z_{2}$  & $\Z_{2}$  & $\Z_{2}^{2}$ & \cE & \cD & \cC & \cB \\ \addlinespace[3pt]
$\pi_{9}$  & $0$     & $0$     & $\Z_{3}$  & $\Z_{3}$  & $\Z_{2}^{2}$ & $\Z_{2}$ & \cE & \cD & \cC \\ \addlinespace[3pt]
$\pi_{10}$ & $0$     & $0$     & $\Z_{15}$ & $\Z_{15}$ & \footnotesize{$\Z_{24} {\times} \Z_{3}$} & $\Z_{2}$ & \cF & \cE & \cD \\ \addlinespace[3pt]
$\pi_{11}$ & $0$     & $0$     & $\Z_{2}$  & $\Z_{2}$  & $\Z_{15}$ & $\Z_{2}$ & $\Z$ & \cF & \cE \\ \addlinespace[3pt]
$\pi_{12}$ & $0$     & $0$     & $\Z_{2}^{2}$ & $\Z_{2}^{2}$ & $\Z_{2}$ & $\Z_{30}$ & $\Z_{2}$ & \cG & \cF \\ \addlinespace[3pt]
$\pi_{13}$ & $0$     & $0$     & {\footnotesize $\Z_{12} {\times} \Z_{2}$} & {\footnotesize $\Z_{12} {\times} \Z_{2}$} & $\Z_{2}^{3}$ & $\Z_{2}$ & $\Z_{60}$ & $\Z_{2}$ & \cG \\ \addlinespace[3pt]
%$\pi_{14}$ & $0$     & $0$     & $\Z_{84} {\times} \Z_{2}^{2}$ & $\Z_{84} {\times} \Z_{2}^{2}$ & {\footnotesize $\Z_{120} {\times} \Z_{12} {\times} \Z_{2}$} & $\Z_{2}^{3}$ & $\Z_{24} {\times} \Z_{2}$ & $\Z_{120}$ & $\Z_{2}$ \\ \addlinespace[3pt]
%$\pi_{15}$ & $0$     & $0$     & $\Z_{2}^{2}$ & $\Z_{2}^{2}$ & $\Z_{84} {\times} \Z_{2}^{5}$ & $\Z_{72} {\times} \Z_{2}$ & $\Z_{2}^{3}$ & $\Z_{2}^{3}$ & $\Z {\times} \Z_{120}$ \\ \addlinespace[3pt]
\bottomrule
\end{tabular}

\caption{Homotopy groups of spheres~\cite{wikipedia-groups}.\index{homotopy!group!of sphere}
The $k^{\textrm{th}}$ homotopy group $\pi_k$ of the $n$-dimensional sphere
$\Sn^n$ is isomorphic to the group listed in each entry, where $\Z$ is
the additive group of integers,\index{integers} and $\Z_{m}$ is the cyclic group\index{group!cyclic}\index{cyclic group} of order~$m$.
}
\label{tab:homotopy-groups-of-spheres}
\end{table}
\egroup


One way of understanding this complexity is through the correspondence
between spaces and $\infty$-groupoids
\index{.infinity-groupoid@$\infty$-groupoid}%
introduced in \cref{cha:basics}.
As discussed in \cref{sec:circle}, the 2-sphere is presented by a higher
inductive type with one point and one 2-dimensional loop.  Thus, one
might wonder why $\pi_3(\Sn ^2)$ is $\Z$, when the type $\Sn ^2$ has no
generators creating 3-dimensional cells.  It turns out that the
generating element of $\pi_3(\Sn ^2)$ is constructed using the
interchange law described in the proof of \cref{thm:EckmannHilton}: the
algebraic structure of an $\infty$-groupoid includes non-trivial
interactions between levels, and these interactions create elements of
higher homotopy groups.

\index{classical!homotopy theory|)}%

Type theory provides a natural setting for investigating this structure, as
we can easily define the higher homotopy groups.  Recall from \cref{def:loopspace} that for $n:\N$, the
$n$-fold iterated loop space\index{loop space!iterated} of a pointed type $(A,a)$ is defined
recursively by:
\begin{align*}
  \Omega^0(A,a)&=(A,a)\\
  \Omega^{n+1}(A,a)&=\Omega^n(\Omega(A,a)).
\end{align*}
%
This gives a \emph{space} (i.e.\ a type) of $n$-dimensional loops\index{loop!n-@$n$-}, which itself has
higher homotopies.  We obtain the set of $n$-dimensional loops by
truncation (this was also defined as an example in
\cref{sec:free-algebras}):

\begin{defn}[Homotopy Groups]\label{def-of-homotopy-groups}
  Given $n\ge 1$ and $(A,a)$ a pointed type, we define the \define{homotopy groups} of $A$
  \indexdef{homotopy!group}%
  at $a$ by
  \[\pi_n(A,a)\defeq \Trunc0{\Omega^n(A,a)}\]
\end{defn}

\noindent
Since $n\ge 1$, the path concatenation and inversion operations on
$\Omega^n(A)$ induce operations on $\pi_n(A)$ making it into a group in
a straightforward way.  If $n\ge 2$, then the group $\pi_n(A)$ is
abelian\index{group!abelian}, by the Eckmann--Hilton argument \index{Eckmann--Hilton argument} (\cref{thm:EckmannHilton}).
It is convenient to also write $\pi_0(A) \defeq \trunc0 A$,
but this case behaves somewhat differently: not only is it not a group,
it is defined without reference to any basepoint in $A$.

\index{presentation!of an infinity-groupoid@of an $\infty$-groupoid}%
This definition is a suitable one for investigating homotopy groups
because the (higher) inductive definition of a type $X$ presents $X$ as
a free type, analogous to a free $\infty$-groupoid,
\index{.infinity-groupoid@$\infty$-groupoid}%
and this
presentation \emph{determines} but does not \emph{explicitly describe}
the higher identity types of $X$.  The identity types are populated by
both the generators ($\lloop$, for the circle) and the results of applying to them all of the groupoid
operations (identity, composition, inverses, associativity, interchange,
\ldots).  Thus, the higher-inductive presentation of a space allows us
to pose the question ``what does the identity type of $X$ really turn out
to be?'' though it can take some significant mathematics to answer it.
This is a higher-dimensional generalization of a familiar fact in type
theory: characterizing the identity type of $X$ can take some work,
even if $X$ is an ordinary inductive type, such as the natural numbers
or booleans.  For example, the theorem that $\bfalse$ is different
from $\btrue$ does not follow immediately from the definition;
see \cref{sec:compute-coprod}.

\index{univalence axiom}%
The univalence axiom plays an essential role in calculating homotopy
groups (without univalence, type theory is compatible with an
interpretation where all paths, including, for example, the loop on the
circle, are reflexivity).  We will see this in the calculation of the
fundamental group of the circle below: the map from $\Omega(\Sn^1)$ to $\Z$ is defined by mapping a loop on the circle to an
automorphism\index{automorphism!of Z, successor@of $\Z$, successor} of the set $\Z$, so that, for example, $\lloop \ct \opp
\lloop$ is sent to $\mathsf{successor} \ct \mathsf{predecessor}$ (where
$\mathsf{successor}$ and $\mathsf{predecessor}$ are automorphisms of
$\Z$ viewed, by univalence, as paths in the universe), and then applying
the automorphism to 0. Univalence produces non-trivial paths in the
universe, and this is used to extract information from paths in higher
inductive types.

In this chapter, we first calculate some homotopy groups of spheres,
including $\pi_k(\Sn ^1)$ (\cref{sec:pi1-s1-intro}), $\pi_{k}(\Sn
^n)$ for $k<n$ (\cref{sec:conn-susp,sec:pik-le-n}), $\pi_2(\Sn ^2)$ and $\pi_3(\Sn ^2)$ by
way of the Hopf fibration (\cref{sec:hopf}) and a long-exact-sequence
argument (\cref{sec:long-exact-sequence-homotopy-groups}), and
$\pi_n(\Sn ^n)$ by way of the Freudenthal suspension theorem
(\cref{sec:freudenthal}).  Next, we discuss the van Kampen theorem
(\cref{sec:van-kampen}), which characterizes the fundamental group of
a pushout, and the status of Whitehead's principle (when is a map that
induces an equivalence on all homotopy groups an equivalence?)
(\cref{sec:whitehead}).  Finally, we include brief summaries of
additional results that are not included in the book, such as
$\pi_{n+1}(\Sn ^n)$ for $n\ge 3$, the Blakers--Massey theorem, and a
construction of Eilenberg--Mac Lane spaces (\cref{sec:moreresults}).
Prerequisites for this chapter include \cref{cha:typetheory,cha:basics,cha:hits,cha:hlevels} as well as parts of \cref{cha:logic}.

\index{fundamental!group!of circle|(}
\section{\texorpdfstring{$\pi_1(S^1)$}{π₁(S¹)}}
\label{sec:pi1-s1-intro}

In this section, our goal is to show that $\id {\pi_1(\Sn ^1)} {\Z}$.
In fact, we will show that the loop space\index{loop space} ${\Omega(\Sn ^1)}$ is equivalent to $\Z$.
This is a stronger statement, because $\id{\pi_1(\Sn ^1)} {\trunc 0 {\Omega(\Sn ^1)}}$ by
definition; so if $\id {\Omega(\Sn ^1)} {\Z}$, then $\id {\trunc
  0 {\Omega(\Sn ^1)}} {\trunc 0 {\Z}}$ by congruence, and
$\Z$ is a set by definition (being a set-quotient; see \cref{defn-Z,Z-quotient-by-canonical-representatives}), so $\id {\trunc 0 {\Z}} {\Z}$.
Moreover, knowing that ${\Omega(\Sn ^1)}$ is a set will imply that $\pi_n(\Sn^1)$ is trivial for $n>1$, so we will actually have calculated \emph{all} the homotopy groups of $\Sn^1$.

\subsection{Getting started}
\label{sec:pi1s1-initial-thoughts}

It is not too hard to define functions in both directions between $\Omega(\Sn^1)$ and \Z.
By specializing \cref{thm:looptothe} to $\lloop:\base=\base$, we have a function $\lloop^{\blank} : \Z \rightarrow (\id{\base}{\base})$ defined (loosely speaking) by
\[
  \lloop^n =
  \begin{cases}
    \underbrace{\lloop \ct \lloop \ct \cdots \ct \lloop}_{n}  & \text{if $n > 0$,} \\
    \underbrace{\opp \lloop \ct \opp \lloop \ct \cdots \ct \opp \lloop}_{-n} & \text{if $n < 0$,} \\
    \refl{\base} & \text{if $n = 0$.}
\end{cases}
\]
%
Defining a function $g:\Omega(\Sn^1)\to\Z$ in the other direction is a bit trickier.
Note that the successor function $\Zsuc:\Z\to\Z$ is an equivalence,
\index{successor!isomorphism on Z@isomorphism on $\Z$}%
and hence induces a path $\ua(\Zsuc):\Z=\Z$ in the universe \type.
Thus, the recursion principle of $\Sn^1$ induces a map $c:\Sn^1\to\type$ by $c(\base)\defeq \Z$ and $\apfunc c (\lloop) \defid \ua(\Zsuc)$.
Then we have $\apfunc{c} : (\base=\base) \to (\Z=\Z)$, and we can define $g(p)\defeq \transfib{X\mapsto X}{\apfunc{c}(p)}{0}$.

With these definitions, we can even prove that $g(\lloop^n)=n$ for any $n:\Z$, using the induction principle \cref{thm:sign-induction} for $n$.
(We will prove something more general a little later on.)
However, the other equality $\lloop^{g(p)}=p$ is significantly harder.
The obvious thing to try is path induction, but path induction does not apply to loops such as $p:(\base=\base)$ that have \emph{both} endpoints fixed!
A new idea is required, one which can be explained both in terms of classical homotopy theory and in terms of type theory.
We begin with the former.


\subsection{The classical proof}
\label{sec:pi1s1-classical-proof}

\index{classical!homotopy theory|(}%
In classical homotopy theory, there is a standard proof of $\pi_1(\Sn^1)=\Z$ using universal covering spaces.
Our proof can be regarded as a type-theoretic version of this proof, with covering spaces appearing here as fibrations whose fibers are sets.
\index{fibration}%
\index{total!space}%
Recall that \emph{fibrations} over a space $B$ in homotopy theory correspond to type families $B\to\type$ in type theory.
\index{path!fibration}%
\index{fibration!of paths}%
In particular, for a point $x_0:B$, the type family $(x\mapsto (x_0=x))$ corresponds to the \emph{path fibration} $P_{x_0} B \to B$, in which the points of $P_{x_0} B$ are paths in $B$ starting at $x_0$, and the map to $B$ selects the other endpoint of such a path.
This total space $P_{x_0} B$ is contractible, since we can ``retract'' any path to its initial endpoint $x_0$ --- we have seen the type-theoretic version of this as \cref{thm:contr-paths}.
Moreover, the fiber over $x_0$ is the loop space\index{loop space} $\Omega(B,x_0)$ --- in type theory this is obvious by definition of the loop space.

\begin{figure}\centering
  \begin{tikzpicture}[xscale=1.4,yscale=.6]
    \node (R) at (2,1) {$\mathbb{R}$};
    \node (S1) at (2,-2) {$S^1$};
    \draw[->] (R) -- node[auto] {$w$} (S1);
    \draw (0,-2) ellipse (1 and .4);
    \draw[dotted] (1,0) arc (0:-30:1 and .8);
    \draw (1,0) arc (0:90:1 and .8) arc (90:270:1 and .3) coordinate (t1);
    \draw[white,line width=4pt] (t1) arc (-90:90:1 and .8);
    \draw (t1) arc (-90:90:1 and .8) arc (90:270:1 and .3) coordinate (t2);
    \draw[white,line width=4pt] (t2) arc (-90:90:1 and .8);
    \draw (t2) arc (-90:90:1 and .8) arc (90:270:1 and .3) coordinate (t3);
    \draw[white,line width=4pt] (t3) arc (-90:90:1 and .8);
    \draw (t3) arc (-90:-30:1 and .8) coordinate (t4);
    \draw[dotted] (t4) arc (-30:0:1 and .8);
    \node[fill,circle,inner sep=1pt,label={below:\scriptsize \base}] at (0,-2.4) {};
    \node[fill,circle,inner sep=1pt,label={above left:\scriptsize 0}] at (0,.2) {};
    \node[fill,circle,inner sep=1pt,label={above left:\scriptsize 1}] at (0,1.2) {};
    \node[fill,circle,inner sep=1pt,label={above left:\scriptsize 2}] at (0,2.2) {};
  \end{tikzpicture}
  \caption{The winding map in classical topology}\label{fig:winding}
\end{figure}

Now in classical homotopy theory, where $\Sn^1$ is regarded as a topological space, we may proceed as follows.
\index{winding!map}%
Consider the ``winding'' map $w:\mathbb{R}\to \Sn ^1$, which looks like a helix projecting down onto the circle (see \cref{fig:winding}).
This map $w$ sends each point on the helix\index{helix} to the point on the circle that it is ``sitting above''.
It is a fibration, and the fiber over each point is isomorphic to the integers.\index{integers}
If we lift the path that goes counterclockwise around the loop on the bottom, we go up one level in the helix, incrementing the integer in the fiber.
Similarly, going clockwise around the loop on the bottom corresponds to going down one level in the helix, decrementing this count.
This fibration is called the \emph{universal cover} of the circle.
\index{universal!cover}%
\index{cover!universal}%
\index{covering space!universal}%

Now a basic fact in classical homotopy theory is that a map $E_1\to E_2$ of fibrations over $B$ which is a homotopy equivalence between $E_1$ and $E_2$ induces a homotopy equivalence on all fibers.
(We have already seen the type-theoretic version of this as well in \cref{thm:total-fiber-equiv}.)
Since $\mathbb{R}$ and $P_{\base} S^1$ are both contractible topological spaces, they are homotopy equivalent, and thus their fibers $\Z$ and $\Omega(\Sn ^1)$ over the basepoint are also homotopy equivalent.

\index{classical!homotopy theory|)}%

\subsection{The universal cover in type theory}
\label{sec:pi1s1-universal-cover}

\index{universal!cover|(}%
\index{cover!universal|(}%
\index{covering space!universal|(}%

Let us consider how we might express the preceding proof in type theory.
We have already remarked that the path fibration of $\Sn^1$ is represented by the type family $(x\mapsto (\base=x))$.
We have also already seen a good candidate for the universal cover of $\Sn^1$: it's none other than the type family $c:\Sn^1\to\type$ which we defined in \cref{sec:pi1s1-initial-thoughts}!
By definition, the fiber of this family over $\base$ is $\Z$, while the effect of transporting around $\lloop$ is to add one --- thus it behaves just as we would expect from \cref{fig:winding}.

However, since we don't know yet that this family behaves like a universal cover is supposed to (for instance, that its total space is simply connected), we use a different name for it.
For reference, therefore, we repeat the definition.
\index{integers}

\begin{defn}[Universal Cover of $\Sn^1$] \label{S1-universal-cover}
  Define $\code : \Sn ^1 \to \type$ by circle-recursion, with
  \begin{align*}
    \code(\base) &\defeq \Z \\
    \apfunc{\code}({\lloop}) &\defid \ua(\Zsuc).
  \end{align*}
\end{defn}

We emphasize briefly the definition of this family, since it is so different from how one usually defines covering spaces in classical homotopy theory.
To define a function by circle recursion, we need to find a point and a
loop in the codomain.  In this case, the codomain is $\type$, and the point
we choose is $\Z$, corresponding to our expectation that the
fiber of the universal cover should be the integers.  The loop we choose
is the successor/predecessor
\index{successor!isomorphism on Z@isomorphism on $\Z$}%
\index{predecessor!isomorphism on Z@isomorphism on $\Z$}%
isomorphism on $\Z$, which
corresponds to the fact that going around the loop in the base goes up
one level on the helix.  Univalence is necessary for this part of the
proof, because we need to convert a \emph{non-trivial} equivalence on $\Z$ into an identity.

We call this the fibration of ``codes'', because its elements are combinatorial data that act as codes for paths on the circle: the integer $n$ codes for the path which loops around the circle $n$ times.

From this definition, it is simple to calculate that transporting with
$\code$ takes $\lloop$ to the successor function, and
$\opp{\lloop}$ to the predecessor function:
\begin{lem} \label{lem:transport-s1-code}
\id{\transfib \code \lloop x} {x + 1} and
\id{\transfib \code {\opp \lloop} x} {x - 1}.
\end{lem}
\begin{proof}
For the first equation, we calculate as follows:
\begin{align}
{\transfib \code \lloop x}
&= \transfib {A \mapsto A} {(\ap{\code}{\lloop})} x \tag{by \cref{thm:transport-compose}}\\
&= \transfib {A \mapsto A} {\ua (\Zsuc)} x \tag{by computation for $\rec{\Sn^1}$}\\
&= x + 1 \tag{by computation for \ua}.
\end{align}
The second equation follows from the first, because $\transfib{B}{p}{\blank}$ and $\transfib{B}{\opp p}{\blank}$ are always inverses, so $\transfib\code {\opp \lloop}{\blank}$ must be the inverse of $\Zsuc$.
\end{proof}

We can now see what was wrong with our first approach: we defined $f$ and $g$ only on the fibers $\Omega(\Sn^1)$ and \Z, when we should have defined a whole morphism \emph{of fibrations} over $\Sn^1$.
In type theory, this means we should have defined functions having types
\begin{align}
  \prd{x:\Sn^1} &((\base=x) \to \code(x)) \qquad\text{and/or} \label{eq:pi1s1-encode}\\
  \prd{x:\Sn^1} &(\code(x) \to (\base=x))\label{eq:pi1s1-decode}
\end{align}
instead of only the special cases of these when $x$ is \base.
This is also an instance of a common observation in type theory: when attempting to prove something about particular inhabitants of some inductive type, it is often easier to generalize the statement so that it refers to \emph{all} inhabitants of that type, which we can then prove by induction.
Looked at in this way, the proof of $\Omega(\Sn^1)=\Z$ fits into the same pattern as the characterization of the identity types of coproducts and natural numbers in \cref{sec:compute-coprod,sec:compute-nat}.

At this point, there are two ways to finish the proof.
We can continue mimicking the classical argument by constructing~\eqref{eq:pi1s1-encode} or~\eqref{eq:pi1s1-decode} (it doesn't matter which), proving that a homotopy equivalence between total spaces induces an equivalence on fibers, and then that the total space of the universal cover is contractible.
The first type-theoretic proof of $\Omega(\Sn^1)=\Z$ followed this pattern; we call it the \emph{homotopy-theoretic} proof.

Later, however, we discovered that there is an alternative proof, which has a more type-theoretic feel and more closely follows the proofs in \cref{sec:compute-coprod,sec:compute-nat}.
In this proof, we directly construct both~\eqref{eq:pi1s1-encode} and~\eqref{eq:pi1s1-decode}, and prove that they are mutually inverse by calculation.
We will call this the \emph{encode-decode} proof, because we call the functions~\eqref{eq:pi1s1-encode} and~\eqref{eq:pi1s1-decode} \emph{encode} and \emph{decode} respectively.
Both proofs use the same construction of the cover given above.
Where the classical proof induces an equivalence on fibers from an equivalence between total spaces, the encode-decode proof constructs the inverse map (\emph{decode}) explicitly as a map between fibers.
And where the classical proof uses contractibility, the encode-decode proof uses path induction, circle induction, and integer induction.
These are the same tools used to prove contractibility---indeed, path induction \emph{is} essentially contractibility of the path fibration composed with $\mathsf{transport}$---but they are applied in a different way.

Since this is a book about homotopy type theory, we present the encode-decode proof first.
A homotopy theorist who gets lost is encouraged to skip to the homotopy-theoretic proof (\cref{subsec:pi1s1-homotopy-theory}).

\index{universal!cover|)}%
\index{cover!universal|)}%
\index{covering space!universal|)}%

\subsection{The encode-decode proof}
\label{subsec:pi1s1-encode-decode}

\index{encode-decode method|(}%
\indexsee{encode}{encode-decode method}%
\indexsee{decode}{encode-decode method}%
We begin with the function~\eqref{eq:pi1s1-encode} that maps paths to codes:
\begin{defn}
Define $\encode : \prd{x : \Sn ^1} (\base=x) \rightarrow  \code(x)$ by
\[
\encode \: p \defeq \transfib{\code} p 0
\]
(we leave the argument $x$ implicit).
\end{defn}
Encode is defined by lifting a path into the universal cover, which
determines an equivalence, and then applying the resulting equivalence
to $0$.
The interesting thing about this function is that it computes a concrete
number from a loop on the circle, when this loop is represented using
the abstract groupoidal framework of homotopy type theory.  To gain an
intuition for how it does this, observe that by the above lemmas,
$\transfib \code \lloop x$ is the successor map and $\transfib \code {\opp
  \lloop} x$ is the predecessor map.
Further, $\mathsf{transport}$ is functorial (\cref{cha:basics}), so
$\transfib{\code} {\lloop \ct \lloop}{\blank}$ is
\[(\transfib \code \lloop-) \circ (\transfib \code \lloop-)\]
and so on.
Thus, when $p$ is a composition like
\[
\lloop \ct \opp \lloop \ct \lloop \ct \cdots
\]
$\transfib{\code}{p}{\blank}$ will compute a composition of functions like
\[
\Zsuc \circ \Zpred \circ \Zsuc \circ \cdots
\]
Applying this composition of functions to 0 will compute the
\index{winding!number}%
\emph{winding number} of the path---how many times it goes around the
circle, with orientation marked by whether it is positive or negative,
after inverses have been canceled.  Thus, the computational behavior of
$\encode$ follows from the reduction rules for higher-inductive types and
univalence, and the action of $\mathsf{transport}$ on compositions and inverses.

Note that the instance $\encode' \defeq \encode_{\base}$ has type
$(\id \base \base) \rightarrow \Z$.
This will be one half of our desired equivalence; indeed, it is exactly the function $g$ defined in \cref{sec:pi1s1-initial-thoughts}.

Similarly, the function~\eqref{eq:pi1s1-decode} is a generalization of the function $\lloop^{\blank}$ from \cref{sec:pi1s1-initial-thoughts}.

\begin{defn}\label{thm:pi1s1-decode}
Define $\decode : \prd{x : \Sn ^1}\code(x) \rightarrow (\base=x)$ by
circle induction on $x$.  It suffices to give a function
${\code(\base) \rightarrow (\base=\base)}$, for which we use $\lloop^{\blank}$, and
to show that $\lloop^{\blank}$ respects the loop.
\end{defn}

\begin{proof}
To show that $\lloop^{\blank}$ respects the loop, it suffices to give a path
from $\lloop^{\blank}$ to itself that lies over $\lloop$.
By the definition of dependent paths, this means a path from
\[\transfib {(x' \mapsto \code(x') \rightarrow (\base=x'))} {\lloop} {\lloop^{\blank}}\]
to $\lloop^{\blank}$.  We define such a
path as follows:
\begin{align*}
  \MoveEqLeft \transfib {(x' \mapsto \code(x') \rightarrow (\base=x'))} \lloop {\lloop^{\blank}}\\
&= \transfibf {x'\mapsto (\base=x')}(\lloop) \circ {\lloop^{\blank}} \circ \transfibf \code ({\opp \lloop}) \\
&= (- \ct \lloop) \circ (\lloop^{\blank}) \circ \transfibf \code ({\opp \lloop}) \\
&= (- \ct \lloop) \circ (\lloop^{\blank}) \circ \Zpred \\
&= (n \mapsto \lloop^{n - 1} \ct \lloop).
\end{align*}
On the first line, we apply the characterization of $\mathsf{transport}$
when the outer connective of the fibration is $\rightarrow$, which
reduces the $\mathsf{transport}$ to pre- and post-composition with
$\mathsf{transport}$ at the domain and codomain types.  On the second line,
we apply the characterization of $\mathsf{transport}$ when the type family
is $x\mapsto \id{\base}{x}$, which is post-composition of paths.  On the third line,
we use the action of $\code$ on $\opp \lloop$ from
\cref{lem:transport-s1-code}.  And on the fourth line, we simply
reduce the function composition.  Thus, it suffices to show that for all
$n$, $\id{\lloop^{n - 1} \ct \lloop}{\lloop^{n}}$.  This is an easy application of \cref{thm:sign-induction}, using the groupoid laws.
\end{proof}

We can now show that $\encode$ and $\decode$ are quasi-inverses.
What used to be the difficult direction is now easy!

\begin{lem} \label{lem:s1-decode-encode}  For all
for all $x: \Sn ^1$ and $p : \id \base x$, $\id
{\decode_x({{\encode_x(p)}})} p$.
\end{lem}

\begin{proof}
By path induction, it suffices to show that
\narrowequation{\id {\decode_{\base}({{\encode_{\base}(\refl{\base})}})} {\refl{\base}}.}
But
\narrowequation{\encode_{\base}(\refl{\base}) \jdeq \transfib{\code}{\refl{\base}} 0 \jdeq 0,}
and $\decode_{\base}(0) \jdeq \lloop^ 0 \jdeq \refl{\base}$.
\end{proof}

The other direction is not much harder.

\begin{lem} \label{lem:s1-encode-decode} For all
$x: \Sn ^1$ and $c : \code(x)$, we have $\id
{\encode_x({{\decode_x(c)}})} c$.
\end{lem}

\begin{proof}
The proof is by circle induction.  It suffices to show the case for
\base, because the case for \lloop is a path between paths in
$\Z$, which is immediate because $\Z$ is a set.

Thus, it suffices to show, for all $n : \Z$, that
\[
\id {\encode'(\lloop^n)} {n}
\]
The proof is by induction, using \cref{thm:sign-induction}.
%
\begin{itemize}

\item In the case for $0$, the result is true by definition.

\item In the case for $n+1$,
\begin{align}
 {\encode'(\lloop^{n+1})}
&= {\encode'(\lloop^{n} \ct \lloop)} \tag{by definition of $\lloop^{\blank}$} \\
&= \transfib{\code}{(\lloop^{n} \ct \lloop)}{0} \tag{by definition of $\encode$}\\
&= \transfib{\code}{\lloop}{(\transfib{\code}{\lloop^n}{0})} \tag{by functoriality}\\
&= {(\transfib{\code}{\lloop^n}{0})} + 1 \tag{by \cref{lem:transport-s1-code}}\\
&= n + 1. \tag{by the inductive hypothesis}
\end{align}

\item The case for negatives is analogous.  \qedhere
\end{itemize}
\end{proof}

Finally, we conclude the theorem.

\begin{thm}
There is a family of equivalences $\prd{x : \Sn ^1} (\eqv {(\base=x)} {\code(x)})$.
\end{thm}
\begin{proof}
The maps $\encode$ and $\decode$ are quasi-inverses by
\cref{lem:s1-decode-encode,lem:s1-decode-encode}.
\end{proof}

Instantiating at {\base} gives
\begin{cor}\label{cor:omega-s1}
$\eqv {\Omega(\Sn^1,\base)} {\Z}$.
\end{cor}

A simple induction shows that this equivalence takes addition to
composition, so that $\Omega(\Sn ^1) = \Z$ as groups.

\begin{cor} \label{cor:pi1s1}
$\id{\pi_1(\Sn ^1)} {\Z}$, while $\id{\pi_n(\Sn ^1)}0$ for $n>1$.
\end{cor}
\begin{proof}
For $n=1$, we sketched the proof from \cref{cor:omega-s1} above.
For $n > 1$, we have $\trunc 0 {\Omega^{n}(\Sn ^1)} = \trunc 0 {\Omega^{n-1}(\Omega{\Sn ^1})} = \trunc 0 {\Omega^{n-1}(\Z)}$.
And since $\Z$ is a set, $\Omega^{n-1}(\Z)$ is contractible, so this is trivial.
\end{proof}

\index{encode-decode method|)}%


\subsection{The homotopy-theoretic proof}
\label{subsec:pi1s1-homotopy-theory}

In \cref{sec:pi1s1-universal-cover}, we defined the putative universal cover $\code:\Sn^1\to\type$ in type theory, and in \cref{subsec:pi1s1-homotopy-theory} we defined a map $\encode : \prd{x:\Sn^1} (\base=x) \to \code(x)$ from the path fibration to the universal cover.
What remains for the classical proof is to show that this map induces an equivalence on total spaces because both are contractible, and to deduce from this that it must be an equivalence on each fiber.

\index{total!space}%
In \cref{thm:contr-paths} we saw that the total space $\sm{x:\Sn^1} (\base=x)$ is contractible.
For the other, we have:

\begin{lem}\label{thm:iscontr-s1cover}
  The type $\sm{x:\Sn^1}\code(x)$ is contractible.
\end{lem}
\begin{proof}
  We apply the flattening lemma (\cref{thm:flattening}) with the following values:
  \begin{itemize}
  \item $A\defeq\unit$ and $B\defeq\unit$, with $f$ and $g$ the obvious functions.
    Thus, the base higher inductive type $W$ in the flattening lemma is equivalent to $\Sn^1$.
  \item $C:A\to\type$ is constant at \Z.
  \item $D:\prd{b:B} (\eqv{\Z}{\Z})$ is constant at $\Zsuc$.
  \end{itemize}
  Then the type family $P:\Sn^1\to\type$ defined in the flattening lemma is equivalent to $\code:\Sn^1\to\type$.
  Thus, the flattening lemma tells us that $\sm{x:\Sn^1}\code(x)$ is equivalent to a higher inductive type with the following generators, which we denote $R$:
  \begin{itemize}
  \item A function $\mathsf{c}: \Z \to R$.
  \item For each $z:\Z$, a path $\mathsf{p}_z:\mathsf{c}(z) = \mathsf{c}(\Zsuc(z))$.
  \end{itemize}
  We might call this type the \define{homotopical reals};
  \indexdef{real numbers!homotopical}%
  it plays the same role as the topological space $\mathbb{R}$ in the classical proof.

  Thus, it remains to show that $R$ is contractible.
  As center of contraction we choose $\mathsf{c}(0)$; we must now show that $x=\mathsf{c}(0)$ for all $x:R$.
  We do this by induction on $R$.
  Firstly, when $x$ is $\mathsf{c}(z)$, we must give a path $q_z:\mathsf{c}(0) = \mathsf{c}(z)$, which we can do by induction on $z:\Z$, using \cref{thm:sign-induction}:
  \begin{align*}
    q_0 &\defid \refl{\mathsf{c}(0)}\\
    q_{n+1} &\defid q_n \ct \mathsf{p}_n & &\text{for $n\ge 0$}\\
    q_{n-1} &\defid q_n \ct \opp{\mathsf{p}_{n-1}} & &\text{for $n\le 0$.}
  \end{align*}
  Secondly, we must show that for any $z:\Z$, the path $q_z$ is transported along $\mathsf{p}_z$ to $q_{z+1}$.
  By transport of paths, this means we want $q_z \ct \mathsf{p}_z = q_{z+1}$.
  This is easy by induction on $z$, using the definition of $q_z$.
  This completes the proof that $R$ is contractible, and thus so is $\sm{x:\Sn^1}\code(x)$.
\end{proof}

\begin{cor}\label{thm:encode-total-equiv}
  The map induced by \encode:
  \[ \tsm{x:\Sn^1} (\base=x) \to \tsm{x:\Sn^1}\code(x) \]
  is an equivalence.
\end{cor}
\begin{proof}
  Both types are contractible.
\end{proof}

\begin{thm}
  $\eqv {\Omega(\Sn^1,\base)} {\Z}$.
\end{thm}
\begin{proof}
  Apply \cref{thm:total-fiber-equiv} to $\encode$, using \cref{thm:encode-total-equiv}.
\end{proof}

In essence, the two proofs are not very different: the encode-decode one may be seen as a ``reduction'' or ``unpackaging'' of the homotopy-theoretic one.
Each has its advantages; the interplay between the two points of view is part of the interest of the subject.
\index{fundamental!group!of circle|)}


\subsection{The universal cover as an identity system}
\label{sec:pi1s1-idsys}

Note that the fibration $\code:\Sn^1\to\type$ together with $0:\code(\base)$ is a \emph{pointed predicate} in the sense of \cref{defn:identity-systems}.
From this point of view, we can see that the encode-decode proof in \cref{subsec:pi1s1-encode-decode} consists of proving that \code satisfies \cref{thm:identity-systems}\ref{item:identity-systems3}, while the homotopy-theoretic proof in \cref{subsec:pi1s1-homotopy-theory} consists of proving that it satisfies \cref{thm:identity-systems}\ref{item:identity-systems4}.
This suggests a third approach.

\begin{thm}
  The pair $(\code,0)$ is an identity system at $\base:\Sn^1$ in the sense of \cref{defn:identity-systems}.
\end{thm}
\begin{proof}
  Let $D:\prd{x:\Sn^1} \code(x) \to \type$ and $d:D(\base,0)$ be given; we want to define a function $f:\prd{x:\Sn^1}{c:\code(x)} D(x,c)$.
  By circle induction, it suffices to specify $f(\base):\prd{c:\code(\base)} D(\base,c)$ and verify that $\trans{\lloop}{f(\base)} = f(\base)$.

  Of course, $\code(\base)\jdeq \Z$.
  By \cref{lem:transport-s1-code} and induction on $n$, we may obtain a path $p_n : \transfib{\code}{\lloop^n}{0} = n$ for any integer $n$.
  Therefore, by paths in $\Sigma$-types, we have a path $\pairpath(\lloop^n,p_n) : (\base,0) = (\base,n)$ in $\sm{x:\Sn^1} \code(x)$.
  Transporting $d$ along this path in the fibration $\widehat{D}:(\sm{x:\Sn^1} \code(x)) \to\type$ associated to $D$, we obtain an element of $D(\base,n)$ for any $n:\Z$.
  We define this element to be $f(\base)(n)$:
  \[ f(\base)(n) \defeq \transfib{\widehat{D}}{\pairpath(\lloop^n,p_n)}{d}. \]
  %
  Now we need $\transfib{\lam{x} \prd{c:\code(x)} D(x,c)}{\lloop}{f(\base)} = f(\base)$.
  By \cref{thm:dpath-forall}, this means we need to show that for any $n:\Z$,
  %
  \begin{narrowmultline*}
    \transfib{\widehat D}{\pairpath(\lloop,\refl{\trans\lloop n})}{f(\base)(n)}
    =_{D(\base,\trans\lloop n)} \narrowbreak
    f(\base)(\trans\lloop n).
  \end{narrowmultline*}
  %
  Now we have a path $q:\trans\lloop n = n+1$, so transporting along this, it suffices to show
  \begin{multline*}
    \transfib{D(\base)}{q}{\transfib{\widehat D}{\pairpath(\lloop,\refl{\trans\lloop n})}{f(\base)(n)}}\\
    =_{D(\base,n+1)} \transfib{D(\base)}{q}{f(\base)(\trans\lloop n)}.
  \end{multline*}
  By a couple of lemmas about transport and dependent application, this is equivalent to
  \[ \transfib{\widehat D}{\pairpath(\lloop,q)}{f(\base)(n)} =_{D(\base,n+1)} f(\base)(n+1). \]
  However, expanding out the definition of $f(\base)$, we have
  \begin{narrowmultline*}
    \transfib{\widehat D}{\pairpath(\lloop,q)}{f(\base)(n)}
    \narrowbreak
    \begin{aligned}[t]
      &= \transfib{\widehat D}{\pairpath(\lloop,q)}{\transfib{\widehat{D}}{\pairpath(\lloop^n,p_n)}{d}}\\
      &= \transfib{\widehat D}{\pairpath(\lloop^n,p_n) \ct \pairpath(\lloop,q)}{d}\\
      &= \transfib{\widehat D}{\pairpath(\lloop^{n+1},p_{n+1})}{d}\\
      &= f(\base)(n+1).
    \end{aligned}
  \end{narrowmultline*}
  We have used the functoriality of transport, the characterization of composition in $\Sigma$-types (which was an exercise for the reader), and a lemma relating $p_n$ and $q$ to $p_{n+1}$ which we leave it to the reader to state and prove.

  This completes the construction of $f:\prd{x:\Sn^1}{c:\code(x)} D(x,c)$.
  Since
  \[f(\base,0) \jdeq \trans{\pairpath(\lloop^0,p_0)}{d} = \trans{\refl{\base}}{d} = d,\]
  we have shown that $(\code,0)$ is an identity system.
\end{proof}

\begin{cor}
  For any $x:\Sn^1$, we have $\eqv{(\base=x)}{\code(x)}$.
\end{cor}
\begin{proof}
  By \cref{thm:identity-systems}.
\end{proof}

Of course, this proof also contains essentially the same elements as the previous two.
Roughly, we can say that it unifies the proofs of \cref{thm:pi1s1-decode,lem:s1-encode-decode}, performing the requisite inductive argument only once in a generic case.

\begin{rmk}
  Note that all of the above proofs that $\eqv{\pi_1(\Sn^1)}{\Z}$ use the univalence axiom in an essential way.
  This is unavoidable: univalence or something like it is \emph{necessary} in order to prove $\eqv{\pi_1(\Sn^1)}{\Z}$.
  In the absence of univalence, it is consistent to assume the statement ``all types are sets'' (a.k.a.\ ``uniqueness of identity proofs'' or ``Axiom K'', as discussed in \cref{sec:hedberg}), and this statement implies instead that $\eqv{\pi_1(\Sn^1)}{\unit}$.
  In fact, the (non)triviality of $\pi_1(\Sn^1)$ detects exactly whether all types are sets: the proof of \cref{thm:loop-nontrivial} showed conversely that if $\lloop=\refl{\base}$ then all types are sets.
\end{rmk}

\section{Connectedness of suspensions}
\label{sec:conn-susp}

Recall from \cref{sec:connectivity} that a type $A$ is called \define{$n$-connected} if $\trunc nA$ is contractible.
The aim of this section is to prove that the operation of suspension from \cref{sec:suspension} increases connectedness.

\begin{thm} \label{thm:suspension-increases-connectedness}
  If $A$ is $n$-connected then the suspension of $A$ is $(n+1)$-connected.
\end{thm}

\begin{proof}
  We remarked in \cref{sec:colimits} that the suspension of $A$ is the pushout $\unit\sqcup^A\unit$, so we need to
  prove that the following type is contractible:
  %
  \[\trunc{n+1}{\unit\sqcup^A\unit}.\]
  %
  By \cref{reflectcommutespushout} we know that
  $\trunc{n+1}{\unit\sqcup^A\unit}$ is a pushout in $\typelep{n+1}$ of the diagram
  \[\xymatrix{\trunc{n+1}A \ar[d] \ar[r] & \trunc{n+1}{\unit} \\
    \trunc{n+1}{\unit} & }.\]
  %
  Given that $\trunc{n+1}{\unit}=\unit$, the type
  $\trunc{n+1}{\unit\sqcup^A\unit}$ is also a pushout of the following diagram in
  $\typelep{n+1}$ (because both diagrams are equal)
  %
  \[\Ddiag=\vcenter{\xymatrix{\trunc{n+1}A \ar[d] \ar[r] & \unit \\
    \unit & }}.\]
  %
  We will now prove that $\unit$ is also a pushout of $\Ddiag$ in
  $\typelep{n+1}$.
  %
  Let $E$ be an $(n+1)$-truncated type; we need to prove that the following map
  is an equivalence
  %
  \[\function{(\unit \to E)}{\cocone{\Ddiag}{E}}{y}
  {(y,y,\lamu{u:{\trunc{n+1}A}} \refl{y(\ttt)})}.\]
  %
  where we recall that $\cocone{\Ddiag}{E}$ is the type
  \[\sm{f:\unit \to E}{g:\unit \to E}(\trunc{n+1}A\to
  (f(\ttt)=_E{}g(\ttt))).\]
  %
  The map $\function{(\unit\to E)}{E}{f}{f(\ttt)}$ is an equivalence, hence
  we also have
  \[\cocone{\Ddiag}{E}=\sm{x:E}{y:E}(\trunc{n+1}A\to(x=_Ey)).\]
  %
  Now $A$ is $n$-connected hence so is $\trunc{n+1}A$ because
  $\trunc n{\trunc{n+1}A}=\trunc nA=\unit$, and $(x=_Ey)$ is $n$-truncated because
  $E$ is $(n+1)$-connected. Hence by \cref{connectedtotruncated} the
  following map is an equivalence
  %
  \[\function{(x=_Ey)}{(\trunc{n+1}A\to(x=_Ey))}{p}{\lam{z} p}\]
  %
  Hence we have
  %
  \[\cocone{\Ddiag}{E}=\sm{x:E}{y:E}(x=_Ey).\]
  %
  But the following map is an equivalence
  %
  \[\function{E}{\sm{x:E}{y:E}(x=_Ey)}{x}{(x,x,\refl{x})}.\]
  %
  Hence
  %
  \[\cocone{\Ddiag}{E}=E.\]
  %
  Finally we get an equivalence
  %
  \[(\unit \to E)\eqvsym\cocone{\Ddiag}{E}\]
  %
  We can now unfold the definitions in order to get the explicit expression of
  this map, and we see easily that this is exactly the map we had at the
  beginning.

  Hence we proved that $\unit$ is a pushout of $\Ddiag$ in $\typelep{n+1}$. Using
  uniqueness of pushouts we get that $\trunc{n+1}{\unit\sqcup^A\unit}=\unit$
  which proves that the suspension of $A$ is $(n+1)$-connected.
\end{proof}

\begin{cor} \label{cor:sn-connected}
  For all $n:\N$, the sphere $\Sn^n$ is $(n-1)$-connected.
\end{cor}

\begin{proof}
  We prove this by induction on $n$.
  %
  For $n=0$ we have to prove that $\Sn^0$ is merely inhabited, which is clear.
  %
  Let $n:\N$ be such that $\Sn^n$ is $(n-1)$-connected. By definition $\Sn^{n+1}$
  is the suspension of $\Sn^n$, hence by the previous lemma $\Sn^{n+1}$ is
  $n$-connected.
\end{proof}

\section{\texorpdfstring{$\pi_{k \le n}$}{π\_(k≤n)} of an \texorpdfstring{$n$}{n}-connected space and \texorpdfstring{$\pi_{k < n}(\Sn ^n)$}{π\_(k<n)(Sⁿ)}}
\label{sec:pik-le-n}

Let $(A,a)$ be a pointed type and $n:\N$.  Recall from
\cref{thm:homotopy-groups} that if $n>0$ the set $\pi_n(A,a)$ has a group
structure, and if $n>1$ the group is abelian\index{group!abelian}.

We can now say something about homotopy groups of $n$-truncated and
$n$-connected types.

\begin{lem}
  If $A$ is $n$-truncated and $a:A$, then $\pi_k(A,a)=\unit$ for all $k>n$.
\end{lem}

\begin{proof}
  The loop space of an $n$-type  is an
  $(n-1)$-type, hence $\Omega^k(A,a)$ is an $(n-k)$-type, and we have
  $(n-k)\le-1$ so $\Omega^k(A,a)$ is a mere proposition. But $\Omega^k(A,a)$ is inhabited,
  so it is actually contractible and
  $\pi_k(A,a)=\trunc0{\Omega^k(A,a)}=\trunc0{\unit}=\unit$.
\end{proof}

\begin{lem} \label{lem:pik-nconnected}
  If $A$ is $n$-connected and $a:A$, then $\pi_k(A,a)=\unit$ for all $k\le{}n$.
\end{lem}

\begin{proof}
  We have the following sequence of equalities:
  %
  \begin{narrowmultline*}
    \pi_k(A,a) = \trunc0{\Omega^k(A,a)}
    = \Omega^k(\trunc k{(A,a)})
    = \Omega^k(\trunc k{\trunc n{(A,a)}})
    = \narrowbreak
      \Omega^k(\trunc k{\unit})
    = \Omega^k(\unit)
    = \unit.
  \end{narrowmultline*}
  %
  The third equality uses the fact that $k\le{}n$ in order to use that
  $\truncf k\circ\truncf n=\truncf k$ and the fourth equality uses the fact that $A$ is
  $n$-connected.
\end{proof}

\begin{cor}
  $\pi_k(\Sn ^n) = \unit$ for $k < n$.
\end{cor}
\begin{proof}
  The sphere $\Sn^n$ is $(n-1)$-connected by \cref{cor:sn-connected}, so
  we can apply \cref{lem:pik-nconnected}.
\end{proof}

\section{Fiber sequences and the long exact sequence}
\label{sec:long-exact-sequence-homotopy-groups}

\index{fiber sequence|(}%
\index{sequence!fiber|(}%

If the codomain of a function $f:X\to Y$ is equipped with a basepoint $y_0:Y$, then we refer to the fiber $F\defeq \hfib f {y_0}$ of $f$ over $y_0$ as \define{the fiber of $f$}\index{fiber}.
(If $Y$ is connected, then $F$ is determined up to mere equivalence; see \cref{ex:unique-fiber}.)
We now show that if $X$ is also pointed and $f$ preserves basepoints, then there is a relation between the homotopy groups of $F$, $X$, and $Y$ in the form of a \emph{long exact sequence}.
We derive this by way of the \emph{fiber sequence} associated to such an $f$.

\begin{defn}\label{def:pointedmap}
  A \define{pointed map}
  \indexdef{pointed!map}%
  \indexsee{function!pointed}{pointed map}%
  between pointed types $(X,x_0)$ and $(Y,y_0)$ is a
  map $f:X\to Y$ together with a path $f_0:f(x_0)=y_0$.
\end{defn}

For any pointed types $(X,x_0)$ and $(Y,y_0)$, there is a pointed map $(\lam{x} y_0) : X\to Y$ which is constant at the basepoint.
We call this the \define{zero map}\indexdef{zero!map}\indexdef{function!zero} and sometimes write it as $0:X\to Y$.

Recall that every pointed type $(X,x_0)$ has a loop space\index{loop space} $\Omega (X,x_0)$.
We now note that this operation is functorial on pointed maps.\index{loop space!functoriality of}\index{functor!loop space}

\begin{defn}
  Given a pointed map between pointed types $f:X \to Y$, we define a pointed
  map $\Omega f:\Omega X
  \to \Omega Y$ by
  \[(\Omega f)(p) \defeq \rev{f_0}\ct\ap{f}{p}\ct f_0.\]
  The path $(\Omega f)_0 : (\Omega f) (\refl{x_0}) = \refl{y_0}$, which exhibits $\Omega f$ as a pointed map, is the obvious path of type
  \[\rev{f_0}\ct\ap{f}{\refl{x_0}}\ct f_0=\refl{y_0}.\]
\end{defn}

There is another functor on pointed maps, which takes $f:X\to Y$ to $\proj1 : \hfib f {y_0} \to X$.
When $f$ is pointed, we always consider $\hfib f {y_0}$ to be pointed with basepoint $(x_0,f_0)$, in which case $\proj1$ is also a pointed map, with witness $(\proj1)_0 \defeq \refl{x_0}$.
Thus, this operation can be iterated.

\begin{defn}
  The \define{fiber sequence}
  \indexdef{fiber sequence}%
  \indexdef{sequence!fiber}%
  of a pointed map $f:X\to Y$ is the infinite sequence of pointed types and pointed maps
  \[\xymatrix{\dots \ar[r]^{f^{(n+1)}} & X^{(n+1)} \ar[r]^{f^{(n)}} & X^{(n)} \ar^-{f^{(n-1)}}[r] & \dots \ar[r] & X^{(2)} \ar^-{f^{(1)}}[r] & X^{(1)} \ar[r]^{f^{(0)}} & X^{(0)}}\]
  defined recursively by
  \[ X^{(0)} \defeq Y\qquad
    X^{(1)} \defeq X\qquad
    f^{(0)} \defeq f\qquad
    \]
  and
  \begin{alignat*}{2}
    X^{(n+1)} &\defeq \hfib {f^{(n-1)}}{x^{(n-1)}_0}\\
    f^{(n)} &\defeq \proj1 &: X^{(n+1)} \to X^{(n)}.
  \end{alignat*}
  where $x^{(n)}_0$ denotes the basepoint of $X^{(n)}$, chosen recursively as above.
\end{defn}

Thus, any adjacent pair of maps in this fiber sequence is of the form
\[ \xymatrix{ X^{(n+1)} \jdeq \hfib{f^{(n-1)}}{x^{(n-1)}_0} \ar[rr]^-{f^{(n)}\jdeq \proj1} && X^{(n)} \ar[r]^{f^{(n-1)}} & X^{(n-1)}. } \]
In particular, we have $f^{(n-1)} \circ f^{(n)} = 0$.
We now observe that the types occurring in this sequence are the iterated loop spaces\index{loop space!iterated} of the base
space $Y$, the total space\index{total!space} $X$, and the fiber $F\defeq \hfib f {y_0}$, and similarly for the maps.

\begin{lem}\label{thm:fiber-of-the-fiber}
  Let $f:X\to Y$ be a pointed map of pointed spaces.  Then:
  \begin{enumerate}
  \item The fiber of $f^{(1)}\defeq \proj1 : \hfib f {y_0} \to X$ is equivalent to $\Omega Y$.\label{item:fibseq1}
  \item Similarly, the fiber of $f^{(2)} : \Omega Y \to \hfib f {y_0}$ is equivalent to $\Omega X$.\label{item:fibseq2}
  \item Under these equivalences, the map $f^{(3)} : \Omega X\to \Omega Y$ is identified with $\Omega f\circ\rev{(\blank)}$.\label{item:fibseq3}
  \end{enumerate}
\end{lem}
\begin{proof}
  For~\ref{item:fibseq1}, we have
  \begin{align*}
    \hfib{f^{(1)}}{x_0}
    &\defeq \sm{z:\hfib{f}{y_0}} (\proj{1}(z) = x_0)\\
    &\eqvsym \sm{x:A}{p:f(x)=y_0} (x = x_0) &\text{(by \cref{ex:sigma-assoc})}\\
    &\eqvsym (f(x_0) = y_0) &\text{(as $\tsm{x:A} (x=x_0)$ is contractible)}\\
    &\eqvsym (y_0 = y_0) &\text{(by $(f_0 \ct \blank)$)}\\
    &\jdeq \Omega Y.
  \end{align*}
  Tracing through, we see that this equivalence sends $((x,p),q)$ to $\opp{f_0} \ct \ap{f}{\opp q} \ct p$, while its inverse sends $r:y_0=y_0$ to $((x_0, f_0 \ct r), \refl{x_0})$.
  In particular, the basepoint $((x_0,f_0),\refl{x_0})$ of $\hfib{f^{(1)}}{x_0}$ is sent to $\opp{f_0} \ct \ap{f}{\opp {\refl{x_0}}} \ct f_0$, which equals $\refl{y_0}$.
  Hence this equivalence is a pointed map (see \cref{ex:pointed-equivalences}).
  Moreover, under this equivalence, $f^{(2)}$ is identified with $\lam{r} (x_0, f_0 \ct r): \Omega Y \to \hfib f {y_0}$.

  \cref{item:fibseq2} follows immediately by applying~\ref{item:fibseq1} to $f^{(1)}$ in place of $f$.
  % The resulting equivalence sends $(((x,p),p'),q') : \hfib{f^{(2)}}{(x_0,f_0)}$ to $\ap{f}{\opp {q'}} \ct p'$, while its inverse sends $s:x_0=x_0$ to $(((x_0,f_0), s), \refl{(x_0,f_0)})$.
  Since $(f^{(1)})_0 \defeq \refl{x_0}$, under this equivalence $f^{(3)}$ is identified with the map $\Omega X \to \hfib {f^{(1)}}{x_0}$ defined by $s \mapsto ((x_0,f_0),s)$.
  Thus, when we compose with the previous equivalence $\hfib {f^{(1)}}{x_0} \eqvsym \Omega Y$, we see that $s$ maps to $\opp{f_0} \ct \ap{f}{\opp s} \ct f_0$, which is by definition $(\Omega f)(\opp s)$, giving~\ref{item:fibseq3}.
\end{proof}

Thus, the fiber sequence of $f:X\to Y$ can be pictured as:
\[\xymatrix@C=1.5pc{
  \dots \ar[r] &
  \Omega^2 X \ar[r]^-{\Omega^2 f} &
  \Omega^2 Y \ar[r]^-{-\Omega \partial} &
  \Omega F \ar[r]^-{-\Omega i} &
  \Omega X \ar[r]^-{-\Omega f} &
  \Omega Y \ar[r]^-{\partial} &
  F \ar[r]^-{i} &
  X \ar[r]^{f} & Y.}\]
where the minus signs denote composition with path inversion $\rev{(\blank)}$.
Note that by \cref{ex:ap-path-inversion}, we have
\[ \Omega\left(\Omega f\circ \opp{(\blank)}\right) \circ \opp{(\blank)}
= \Omega^2 f \circ \opp{(\blank)} \circ \opp{(\blank)}
= \Omega^2 f.
\]
Thus, there are minus signs on the $k$-fold loop maps whenever $k$ is odd.

From this fiber sequence we will deduce an \emph{exact sequence of pointed sets}.
\index{image}%
Let $A$ and $B$ be sets and $f:A\to B$ a function, and recall from \cref{defn:modal-image} the definition of the \emph{image} $\im(f)$, which can be regarded as a subset of $B$:
\[\im(f) \defeq \setof{b:B | \exis{a:A} f(a)=b}. \]
If $A$ and $B$ are moreover pointed with basepoints $a_0$ and $b_0$, and $f$ is a pointed map, we define the \define{kernel}
\indexdef{kernel}%
\indexdef{pointed!map!kernel of}%
of $f$ to be the following subset of $A$:
\symlabel{kernel}
\[\ker(f) \defeq \setof{x:A | f(x) = b_0}. \]
Of course, this is just the fiber of $f$ over the basepoint $b_0$; it a subset of $A$ because $B$ is a set.

Note that any group is a pointed set, with its unit element as basepoint, and any group homomorphism is a pointed map.
In this case, the kernel and image agree with the usual notions from group theory.

\begin{defn}
  An \define{exact sequence of pointed sets}
  \indexdef{exact sequence}%
  \indexdef{sequence!exact}%
  is a (possibly bounded) sequence of pointed sets and pointed maps:
  \[\xymatrix{\dots \ar[r] & A^{(n+1)} \ar[r]^-{f^{(n)}} & A^{(n)} \ar[r]^{f^{(n-1)}} & A^{(n-1)} \ar[r] &
    \dots}\]
  such that for every $n$, the image of $f^{(n)}$ is equal, as a subset of $A^{(n)}$, to the kernel of $f^{(n-1)}$.
  In other words, for all $a:A^{(n)}$ we have
  \[ (f^{(n-1)}(a) = a^{(n-1)}_0) \iff \exis{b:A^{(n+1)}} (f^{(n)}(b)=a). \]
  where $a^{(n)}_0$ denotes the basepoint of $A^{(n)}$.
\end{defn}

Usually, most or all of the pointed sets in an exact sequence are groups, and often abelian groups.
When we speak of an \define{exact sequence of groups}, it is assumed moreover that the maps are group homomorphisms and not just pointed maps.

\index{exact sequence}
\begin{thm}\label{thm:les}
  Let $f:X \to Y$ be a pointed map between pointed spaces with fiber $F\defeq \hfib f {y_0}$.
  Then we have the following long exact sequence, which consists of groups except for the last three terms, and abelian groups except for the last six.

  \[
  \xymatrix@R=1.2pc@C=3pc{
    \vdots & \vdots & \vdots \ar[lld] \\
    \pi_k(F) \ar[r] & \pi_k(X) \ar[r] & \pi_k(Y) \ar[lld] \\
    \vdots & \vdots & \vdots \ar[lld] \\
    \pi_2(F) \ar[r] & \pi_2(X) \ar[r] & \pi_2(Y) \ar[lld] \\
    \pi_1(F) \ar[r] & \pi_1(X) \ar[r] & \pi_1(Y) \ar[lld]\\
    \pi_0(F) \ar[r] & \pi_0(X) \ar[r] & \pi_0(Y)}
  \]
\end{thm}

% In US trade we might want a page break here, and extra stretch, otherwise the
% whole page looks ugly.
\vspace*{0pt plus 10ex}
\goodbreak

\begin{proof}
  We begin by showing that the 0-truncation of a fiber sequence is an exact sequence of pointed sets.
  Thus, we need to show that for any adjacent pair of maps in a fiber sequence:
  %
  \[\xymatrix{\hfib{f}{z_0} \ar^-g[r] & W \ar^-f[r] & Z}\]
  %
  with $g\defeq \proj1$, the sequence
  %
  \[\xymatrix{\trunc{0}{\hfib{f}{z_0}} \ar^-{\trunc0g}[r] & \trunc0{W}
    \ar^-{\trunc0{f}}[r] & \trunc0{Z}}\]
  %
  is exact, i.e.\ that $\im(\trunc0g)\subseteq\ker(\trunc0f)$ and $\ker(\trunc0f)\subseteq\im(\trunc0g)$.

  The first inclusion is equivalent to $\trunc0g\circ\trunc0f=0$, which holds by functoriality of $\truncf0$ and the fact that $g\circ f=0$.
  For the second, we assume $w':\trunc0W$ and $p':\trunc0f(w')=\tproj0{z_0}$ and show there merely exists ${t:\hfib{f}{z_0}}$ such that $g(t)=w'$.
  Since our goal is a mere proposition, we can assume that $w'$ is of the
  form $\tproj0w$ for some $w:W$.
  Now by \cref{thm:path-truncation}, $p' : \tproj0{f(w)}=\tproj0{z_0}$ yields $p'': \trunc{-1}{f(w)=z_0}$, so by a further truncation induction we may assume some $p:f(w)=z_0$.
  But now we have $\tproj0{(w,p)}:\tproj0{\hfib{f}{z_0}}$ whose image under $\trunc0g$ is $\tproj0w\jdeq w'$, as desired.

  Thus, applying $\truncf0$ to the fiber sequence of $f$, we obtain a long exact sequence involving the pointed sets $\pi_k(F)$, $\pi_k(X)$, and $\pi_k(Y)$ in the desired order.
  And of course, $\pi_k$ is a group for $k\ge1$, being the 0-truncation of a loop space, and an abelian group for $k\ge 2$ by the Eckmann--Hilton argument
  \index{Eckmann--Hilton argument} (\cref{thm:EckmannHilton}).
  Moreover, \cref{thm:fiber-of-the-fiber} allows us to identify the maps $\pi_k(F) \to \pi_k(X)$ and $\pi_k(X) \to \pi_k(Y)$ in this exact sequence as $(-1)^k \pi_k(i)$ and $(-1)^k \pi_k(f)$ respectively.

  More generally, every map in this long exact sequence except the last three is of the form $\trunc0{\Omega h}$ or $\trunc0{-\Omega h}$ for some $h$.
  In the former case it is a group homomorphism, while in the latter case it is a homomorphism if the groups are abelian; otherwise it is an ``anti-homomorphism''.
  However, the kernel and image of a group homomorphism are unchanged when we replace it by its negative, and hence so is the exactness of any sequence involving it.
  Thus, we can modify our long exact sequence to obtain one involving $\pi_k(i)$ and $\pi_k(f)$ directly and in which all the maps are group homomorphisms (except the last three).
\end{proof}

The usual properties of exact sequences of abelian groups\index{group!abelian!exact sequence of} can be proved as
usual. In particular we have:
\begin{lem}\label{thm:ses}
  Suppose given an exact sequence of abelian groups:
  %
  \[\xymatrix{K \ar[r]& G \ar^f[r] & H \ar[r] & Q.}\]
  %
  \begin{enumerate}
  \item If $K=0$, then $f$ is injective.\label{item:sesinj}
  \item If $Q=0$, then $f$ is surjective.\label{item:sessurj}
  \item If $K=Q=0$, then $f$ is an isomorphism.\label{item:sesiso}
  \end{enumerate}
\end{lem}
\begin{proof}
  Since the kernel of $f$ is the image of $K\to G$, if $K=0$ then the kernel of $f$ is $\{0\}$;
  hence $f$ is injective because it's a group morphism.
  Similarly, since the image of $f$ is the kernel of $H\to Q$, if $Q=0$ then the image of $f$ is all of $H$, so $f$ is surjective.
  Finally,~\ref{item:sesiso} follows from~\ref{item:sesinj} and~\ref{item:sessurj} by \cref{thm:mono-surj-equiv}.
\end{proof}

As an immediate application, we can now quantify in what way $n$-connectedness of a map is stronger than inducing an equivalence on $n$-truncations.

\begin{cor}\label{thm:conn-pik}
  Let $f:A\to B$ be $n$-connected and $a:A$, and define $b\defeq f(a)$.  Then:
  \begin{enumerate}
  \item If $k\le n$, then $\pi_k(f):\pi_k(A,a) \to \pi_k(B,b)$ is an isomorphism.
  \item If $k=n+1$, then $\pi_k(f):\pi_k(A,a) \to \pi_k(B,b)$ is surjective.
  \end{enumerate}
\end{cor}
\begin{proof}
  As part of the long exact sequence, for each $k$ we have an exact sequence
  \[\xymatrix{\pi_k(\hfib f b) \ar[r]& \pi_k(A,a) \ar^f[r] & \pi_k(B,b) \ar[r] & \pi_{k-1}(\hfib f b).}\]
  Now since $f$ is $n$-connected, $\trunc n{\hfib f b}$ is contractible.
  Therefore, if $k\le n$, then $\pi_k(\hfib f b) = \trunc0{\Omega^k(\hfib f b)} = \Omega^k(\trunc k{\hfib f b})$ is also contractible.
  Thus, $\pi_k(f)$ is an isomorphism for $k\le n$ by \cref{thm:ses}\ref{item:sesiso}, while for $k=n+1$ it is surjective by \cref{thm:ses}\ref{item:sessurj}.
\end{proof}

In \cref{sec:whitehead} we will see that the converse of \cref{thm:conn-pik} also holds.

\index{fiber sequence|)}%
\index{sequence!fiber|)}%

\section{The Hopf fibration}
\label{sec:hopf}

In this section we will define the \define{Hopf fibration}.
\indexdef{Hopf!fibration}%

\begin{thm}[Hopf Fibration]\label{thm:hopf-fibration}
There is a fibration $H$ over $\Sn ^2$ whose fiber over the basepoint is $\Sn ^1$ and
whose total space is $\Sn ^3$.
\end{thm}

The Hopf fibration will allow us to compute several homotopy groups of
spheres.
Indeed, it yields the following long exact sequence
\index{homotopy!group!of sphere}
\index{sequence!exact}
of homotopy groups
(see
\cref{sec:long-exact-sequence-homotopy-groups}):
%
\[
\xymatrix@R=1.2pc{
  \pi_k(\Sn^1) \ar[r] & \pi_k(\Sn^3) \ar[r] & \pi_k(\Sn^2) \ar[lld] \\
  \vdots & \vdots & \vdots \ar[lld] \\
  \pi_2(\Sn^1) \ar[r] & \pi_2(\Sn^3) \ar[r] & \pi_2(\Sn^2) \ar[lld] \\
  \pi_1(\Sn^1) \ar[r] & \pi_1(\Sn^3) \ar[r] & \pi_1(\Sn^2)}
\]
%
We've already computed all $\pi_n(\Sn^1)$, and $\pi_k(\Sn^n)$ for $k<n$, so this
becomes the following:
%
\[
\xymatrix@R=1.2pc{
  0 \ar[r] & \pi_k(\Sn^3) \ar[r] & \pi_k(\Sn^2) \ar[lld] \\
  \vdots & \vdots & \vdots \ar[lld] \\
  0 \ar[r] & \pi_3(\Sn^3) \ar[r] & \pi_3(\Sn^2) \ar[lld] \\
  0 \ar[r] & 0 \ar[r] & \pi_2(\Sn^2) \ar[lld] \\
  \Z \ar[r] & 0 \ar[r] & 0}
\]
%
In particular we get the following result:

\begin{cor} \label{cor:pis2-hopf}
  We have $\eqv{\pi_2(\Sn^2)}{\Z}$ and $\eqv{\pi_k(\Sn^3)}{\pi_k(\Sn^2)}$ for
  every $k\ge3$ (where the map is induced by the Hopf fibration, seen as a map
  from the total space $\Sn^3$ to the base space $\Sn^2$).
\end{cor}

In fact, we can say more: the fiber sequence of the Hopf fibration will show that $\Omega^3(\Sn^3)$ is the fiber of a map from $\Omega^3(\Sn^2)$ to $\Omega^2(\Sn^1)$.
Since $\Omega^2(\Sn^1)$ is contractible, we have $\eqv{\Omega^3(\Sn^3)}{\Omega^3(\Sn^2)}$.
In classical homotopy theory, this fact would be a consequence of \cref{cor:pis2-hopf} and Whitehead's theorem, but Whitehead's theorem is not necessarily valid in homotopy type theory (see \cref{sec:whitehead}).
We will not use the more precise version here though.

\subsection{Fibrations over pushouts}
\label{sec:fib-over-pushout}

We first start with a lemma explaining how to construct fibrations over
pushouts.
\index{pushout}%

\begin{lem}\label{lem:fibration-over-pushout}
  Let $\Ddiag=(Y\xleftarrow{j}X\xrightarrow{k}Z)$ be a span\index{span} and assume
  that we have
  \begin{itemize}
  \item Two fibrations $E_Y:Y\to\type$ and $E_Z:Z\to\type$.
  \item An equivalence $e_X$ between $E_Y\circ j:X\to\type$ and $E_Z\circ
    k:X\to\type$, i.e.
    \[e_X:\prd{x:X}\eqv{E_Y(j(x))}{E_Z(k(x))}.\]
  \end{itemize}

  Then we can construct a fibration $E:Y\sqcup^XZ\to\type$ such that
  \begin{itemize}
  \item For all $y:Y$, $E(\inl(y))\judgeq E_Y(y)$.
  \item For all $z:Z$, $E(\inr(z))\judgeq E_Z(z)$.
  \item For all $x:X$, $\map E{\glue(x)}=\ua(e_X(x))$ (note that both sides of
    the equation are paths in $\type$ from $E_Y(j(x))$ to $E_Z(k(x))$).
  \end{itemize}
  Moreover, the total space of this fibration fits in the following pushout
  square:
  \[\xymatrix{ \sm{x:X}E_Y(j(x)) \ar[r]_\sim^{\idfunc\times e_X}
    \ar[d]_{j\times\idfunc} &
    \sm{x:X}E_Z(k(x)) \ar[r]^-{k\times\idfunc}
    & \sm{z:Z}E_Z(z) \ar[d]^\inr \\
    \sm{y:Y}E_Y(y) \ar[rr]_\inl & & \sm{t:Y\sqcup^XZ}E(t) }\]
\end{lem}

\begin{proof}
  We define $E$ by the recursion principle of the pushout $Y\sqcup^XZ$. For
  that, we need to specify the value of $E$ on elements of the form $\inl(y)$, $\inr(z)$
  and the action of $E$ on paths $\glue(x)$, so we can just choose the following
  values:
  \begin{align*}
    E(\inl(y)) & \defeq E_Y(y),\\
    E(\inr(z)) & \defeq E_Z(z),\\
    \map E{\glue(x)} & \defid \ua(e_X(x)).
  \end{align*}
  %
  To see that the total space of this fibration is a pushout, we apply the
  flattening lemma (\cref{thm:flattening}) with the following values:\index{flattening lemma}
  \begin{itemize}
  \item $A\defeq Y+Z$, $B\defeq X$ and $f,g:B\to A$ are defined by
    $f(x)\defeq\inl(j(x))$, $g(x)\defeq\inr(k(x))$,
  \item the type family $C:A\to\type$ is defined by
    \begin{equation*}
      C(\inl(y)) \defeq E_Y(y)
      \qquad\text{and}\qquad
      C(\inr(z)) \defeq E_Z(z),
    \end{equation*}
  \item the family of equivalences $D:\prd{b:B}C(f(b))\eqvsym C(g(b))$ is defined
    to be $e_X$.
  \end{itemize}
  %
  The base higher inductive type $W$ in the flattening lemma is equivalent to
  the pushout $Y\sqcup^XZ$ and the type family $P:Y\sqcup^XZ\to\type$ is
  equivalent to the $E$ defined above.

  Thus the flattening lemma tells us that $\sm{t:Y\sqcup^XZ}E(t)$ is equivalent
  the higher inductive type ${E^{\mathrm{tot}}}'$ with the following generators:
  %
  \begin{itemize}
  \item a function $\mathsf{z}:\sm{a:Y+Z}C(a)\to {E^{\mathrm{tot}}}'$,
  \item for each $x:X$ and $t:E_Y(j(x))$, a path
    \narrowequation{\mathsf{z}(\inl(j(x)),t)=\mathsf{z}(\inr(k(x)),e_C(t)).}
  \end{itemize}
  %
  Using the flattening lemma again or a direct computation, it is easy to see
  that $\eqv{\sm{a:Y+Z}C(a)}{\sm{y:Y}E_Y(y)+\sm{z:Z}E_Z(z)}$, hence
  ${E^{\mathrm{tot}}}'$ is equivalent to the higher inductive type
  $E^{\mathrm{tot}}$ with the following generators:
  %
  \begin{itemize}
  \item a function $\inl:\sm{y:Y}E_Y(y)\to E^{\mathrm{tot}}$,
  \item a function $\inr:\sm{z:Z}E_Z(z)\to E^{\mathrm{tot}}$,
  \item for each $(x,t):\sm{x:X}E_Y(j(x))$ a path
    \narrowequation{\glue(x,t):\inl(j(x),t) = \inr(k(x),e_X(t)).}
  \end{itemize}
  %
  Thus the total space of $E$ is the pushout of the total spaces of
  $E_Y$ and $E_Z$, as required.
\end{proof}

\subsection{The Hopf construction}

\begin{defn}
  An \define{H-space}
  \indexdef{H-space}%
  consists of
  \begin{itemize}
  \item a type $A$,
  \item a base point $e:A$,
  \item a binary operation $\mu:A\times A\to A$, and
  \item for every $a:A$, equalities $\mu(e,a)=a$ and $\mu(a,e)=a$.
  \end{itemize}
\end{defn}

\begin{lem}
  Let $A$ be a connected H-space. Then for every $a:A$, the maps $\mu(a,\blank):A\to
  A$ and $\mu(\blank,a):A\to A$ are equivalences.
\end{lem}

\begin{proof}
  Let us prove that for every $a:A$ the map $\mu(a,\blank)$ is an equivalence. The
  other statement is symmetric.
  %
  The statement that $\mu(a,\blank)$ is an equivalence corresponds to a type family
  $P:A\to\prop$ and proving it corresponds to finding a section of this type
  family.

  The type $\prop$ is a set (\cref{thm:hleveln-of-hlevelSn}) hence we can
  define a new type family $P':\trunc0A\to\prop$ by $P'(\tproj0a)\defeq
  P(a)$. But $A$ is connected by assumption, hence $\trunc0A$ is
  contractible. This implies that in order to find a section of $P'$, it is
  enough to find a point in the fiber of $P'$ over $\tproj0e$. But we have
  $P'(\tproj0e)=P(e)$ which is inhabited because $\mu(e,\blank)$ is equal to the
  identity map by definition of an H-space, hence is an equivalence.

  We have proved that for every $x:\trunc0A$ the proposition $P'(x)$ is true,
  hence in particular for every $a:A$ the proposition $P(a)$ is true because
  $P(a)$ is $P'(\tproj0a)$.
\end{proof}

\begin{defn}
  Let $A$ be a connected H-space. We define a fibration over $\susp A$ using
  \cref{lem:fibration-over-pushout}.

  Given that $\susp A$ is the pushout $\unit\sqcup^A\unit$, we can define a
  fibration over $\susp A$ by specifying
  \begin{itemize}
  \item two fibrations over $\unit$ (i.e. two types $F_1$ and $F_2$), and
  \item a family $e:A\to(\eqv{F_1}{F_2})$ of equivalences between
    $F_1$ and $F_2$, one for every element of $A$.
  \end{itemize}
  %
  We take $A$ for $F_1$ and $F_2$, and for $a:A$ we take the equivalence
  $\mu(a,\blank)$ for $e(a)$.
\end{defn}

According to \cref{lem:fibration-over-pushout}, we have the following
diagram:
%
\[\xymatrix{A \ar@{->>}[d] & A \times A \ar[l]_-{\proj2} \ar@{->>}_{\proj1}[d]
  \ar[r]^-{\mu} & A \ar@{->>}[d] \\
  1 & A \ar[r] \ar[l] & 1}\]
%
and the fibration we just constructed is a fibration over $\susp A$ whose total
space is the pushout of the top line.

Moreover, with $f(x,y)\defeq(\mu(x,y),y)$ we have the following diagram:
%
\[\xymatrix{A \ar_\idfunc[d] & A \times A \ar[l]_-{\proj2} \ar^f[d]
  \ar[r]^-{\mu} & A \ar^\idfunc[d] \\
  A & A\times A \ar^-{\proj2}[l] \ar_-{\proj1}[r] & A}\]
%
The diagram commutes and the three vertical maps are equivalences, the inverse
of $f$ being the function $g$ defined by
\[g(u,v)\defeq(\opp{\mu(\blank,v)}(u),v).\]
%
This shows that the two lines are equivalent (hence equal) spans, so the total
space of the fibration we constructed is equivalent to the pushout of the bottom
line.
And by definition, this latter pushout is the \emph{join} of $A$ with itself (see \cref{sec:colimits}).
%
We have proven:

\begin{lem}\label{lem:hopf-construction}
  Given a connected H-space $A$, there is a fibration, called the
  \define{Hopf construction},
  \indexdef{Hopf!construction}%
  over $\susp A$ with fiber $A$ and total space $A*A$.
\end{lem}

\subsection{The Hopf fibration}

\index{Hopf fibration|(}
\indexsee{fibration!Hopf}{Hopf fibration}
We will first construct a structure of H-space on the circle $\Sn^1$, hence by
\cref{lem:hopf-construction} we will get a fibration over $\Sn^2$ with fiber
$\Sn^1$ and total space $\Sn^1*\Sn^1$. We will then prove that this join is
equivalent to $\Sn^3$.

\begin{lem}\label{lem:hspace-S1}
  There is an H-space structure on the circle $\Sn^1$.
\end{lem}
\begin{proof}
  For the base point of the H-space structure we choose $\base$.
  %
  Now we need to define the multiplication operation
  $\mu:\Sn^1\times\Sn^1\to\Sn^1$.
  We will define the curried form $\widetilde\mu:\Sn^1\to(\Sn^1\to\Sn^1)$ of $\mu$
  by recursion on $\Sn^1$:
  \begin{equation*}
    \widetilde\mu(\base) \defeq\idfunc[\Sn^1],
    \qquad\text{and}\qquad
    \ap{\widetilde\mu}{\lloop} \defid\funext(h).
  \end{equation*}
  where $h:\prd{x:\Sn^1}(x=x)$ is the function defined in \cref{thm:S1-autohtpy},
  which has the property that $h(\base) \defeq\lloop$.

  Now we just have to prove that $\mu(x,\base)=\mu(\base,x)=x$ for every
  $x:\Sn^1$.
  %
  By definition, if $x:\Sn^1$ we have
  $\mu(\base,x)=\widetilde\mu(\base)(x)=\idfunc[\Sn^1](x)=x$. For the equality
  $\mu(x,\base)=x$ we do it by induction on $x:\Sn^1$:
  \begin{itemize}
  \item If $x$ is $\base$ then $\mu(\base,\base)=\base$ by definition, so we
    have $\refl\base:\mu(\base,\base)=\base$.
  \item When $x$ varies along $\lloop$, we need to prove that
    \[\refl\base\ct\apfunc{\lam{x}x}({\lloop})=
    \apfunc{\lam{x}\mu(x,\base)}({\lloop})\ct\refl\base.\]
    The left-hand side is equal to $\lloop$, and for the right-hand side we have:
    \begin{align*}
      \apfunc{\lam{x}\mu(x,\base)}({\lloop})\ct\refl\base &=
      \apfunc{\lam{x}(\widetilde\mu(x))(\base)}({\lloop})\\
      &=\happly(\apfunc{\lam{x}(\widetilde\mu(x))}({\lloop}),\base)\\
      &=\happly(\funext(h),\base)\\
      &=h(\base)\\
      &=\lloop. \qedhere
    \end{align*}
  \end{itemize}
\end{proof}

Now recall from \cref{sec:colimits} that the \emph{join} $A*B$ of types $A$ and $B$ is the pushout of the diagram
\index{join!of types}%
\[A \xleftarrow{\proj1}A\times B \xrightarrow{\proj2} B. \]

\begin{lem}
  \index{associativity!of join}%
  The operation of join is associative: if $A$, $B$ and $C$ are three types
  then we have an equivalence $\eqv{(A*B)*C}{A*(B*C)}$.
\end{lem}

\begin{proof}
  We define a map $f:(A*B)*C\to A*(B*C)$ by induction. We first need to define
  $f\circ\inl:A*B\to A*(B*C)$ which will be done by induction, then
  $f\circ\inr:C\to A*(B*C)$, and then $\apfunc{f}\circ\glue:\prd{t:(A*B)\times
    C}f(\inl(\fst(t)))=f(\inr(\snd(t)))$ which will be done by induction on the
  first component of $t$:
  \begin{align*}
    (f\circ\inl)(\inl(a))) &\defeq \inl(a), \\
    (f\circ\inl)(\inr(b))) &\defeq \inr(\inl(b)), \\
    \apfunc{f\circ\inl}(\glue(a,b)) &\defid \glue(a,\inl(b)), \\
    f(\inr(c)) &\defeq \inr(\inr(c)),\\
    \apfunc{f}(\glue(\inl(a),c)) &\defid\glue(a,\inr(c)),\\
    \apfunc{f}(\glue(\inr(b),c)) &\defid\apfunc{\inr}(\glue(b,c)),\\
    \apdfunc{\lam{x}\apfunc{f}(\glue(x,c))}(\glue(a,b)) &\defid
    ``\apdfunc{\lam{x}\glue(a,x)}(\glue(b,c))''.
  \end{align*}
  %
  For the last equation, note that the right-hand side is of type
  \[\transfib{\lam{x}\inl(a)=\inr(x)}{\glue(b,c)}{\glue(a,\inl(b))}=
  \glue(a,\inr(c))\]
  whereas it is supposed to be of type
  %
  \begin{narrowmultline*}
    \transfib{\lam{x}f(\inl(x))=f(\inr(c))}{\glue(a,b)}{\apfunc{f}(\glue(\inl(a),c))}
    = \narrowbreak
    \apfunc{f}(\glue(\inr(b),c)).
  \end{narrowmultline*}
  %
  But by the previous clauses in the definition, both of these types are equivalent to the following type:
  \[\glue(a,\inr(c))=\glue(a,\inl(b))\ct\apfunc\inr(\glue(b,c)),\]
  and so we can coerce by an equivalence to obtain the necessary element.
  %
  Similarly, we can define a map $g:A*(B*C)\to(A*B)*C$, and checking that $f$ and
  $g$ are inverse to each other is a long and tedious but essentially
  straightforward computation.
\end{proof}

A more conceptual proof sketch is as follows.

\begin{proof}
  Let us consider the following diagram where the maps are the obvious
  projections:
  \[\xymatrix{
    A & A\times C \ar[l] \ar[r] & A\times C\\
    A\times B \ar[u] \ar[d] & A\times B\times C \ar[l]\ar[u]\ar[r]\ar[d] &
    A\times C \ar[u] \ar[d] \\
    B & B\times C \ar[l] \ar[r] & C}\]
  %
  Taking the colimit of the columns gives the following
  diagram, whose colimit is $(A*B)*C$:
  \[\xymatrix{A*B & (A*B)\times C \ar[l]\ar[r] & C}\]
  %
  On the other hand, taking the colimit of the lines gives a diagram whose
  colimit is $A*(B*C)$.

  Hence using a Fubini-like theorem for colimits (that we haven’t proved) we
  have an equivalence $\eqv{(A*B)*C}{A*(B*C)}$. The proof of this Fubini theorem
  \index{Fubini theorem for colimits}
  for colimits still requires the long and tedious computation, though.
\end{proof}

\begin{lem}
  For any type $A$, there is an equivalence $\eqv{\susp A}{\bool*A}$.
\end{lem}

\begin{proof}
  It is easy to define the two maps back and forth and to prove that they are
  inverse to each other. The details are left as an exercise to the reader.
\end{proof}

We can now construct the Hopf fibration:

\begin{thm}
  There is a fibration over $\Sn^2$ of fiber $\Sn^1$ and total space $\Sn^3$.
  \index{total!space}%
\end{thm}
\begin{proof}
  We proved that $\Sn^1$ has a structure of H-space (cf \cref{lem:hspace-S1})
  hence by \cref{lem:hopf-construction} there is a fibration over $\Sn^2$ of
  fiber $\Sn^1$ and total space $\Sn^1*\Sn^1$. But by the two previous results
  and \cref{thm:suspbool} we have:
  \begin{equation*}
    \Sn^1*\Sn^1 = (\susp\bool)*\Sn^1
    =(\bool*\bool)*\Sn^1
    =\bool*(\bool*\Sn^1)
    =\susp(\susp\Sn^1)
    =\Sn^3. \qedhere
  \end{equation*}
\end{proof}
\index{Hopf fibration|)}

\section{The Freudenthal suspension theorem}
\label{sec:freudenthal}

\index{Freudenthal suspension theorem|(}%
\index{theorem!Freudenthal suspension|(}%

Before proving the Freudenthal suspension theorem, we need some auxiliary lemmas about connectedness.
In \cref{cha:hlevels} we proved a number of facts about $n$-connected maps and $n$-types for fixed $n$; here we are now interested in what happens when we vary $n$.
For instance, in \cref{prop:nconnected_tested_by_lv_n_dependent types} we showed that $n$-connected maps are characterized by an ``induction principle'' relative to families of $n$-types.
If we want to ``induct along'' an $n$-connected map into a family of $k$-types for $k> n$, we don't immediately know that there is a function by such an induction principle, but the following lemma says that at least our ignorance can be quantified.

\begin{lem}\label{thm:conn-trunc-variable-ind}
  If $f:A\to B$ is $n$-connected and $P:B\to \ntype{k}$ is a family of $k$-types for $k\ge n$, then the induced function
  \[ (\blank\circ f) : \Parens{\prd{b:B} P(b)} \to \Parens{\prd{a:A} P(f(a)) } \]
  is $(k-n-2)$-truncated.
\end{lem}
\begin{proof}
  We induct on the natural number $k-n$.
  When $k=n$, this is \cref{prop:nconnected_tested_by_lv_n_dependent types}.
  %
  For the inductive step, suppose $f$ is $n$-connected and $P$ is a family of $(k+1)$-types.
  To show that $(\blank\circ f)$ is $(k-n-1)$-truncated, let $\ell:\prd{a:A} P(f(a))$; then we have
  \[ \hfib{(\blank\circ f)}{\ell} \eqvsym \sm{g:\prd{b:B} P(b)} \prd{a:A} g(f(a)) = \ell(a).\]
  Let $(g,p)$ and $(h,q)$ lie in this type, so $p:g\circ f \htpy \ell$ and $q:h\circ f \htpy \ell$; then we also have
  \[ \big((g,p) = (h,q)\big) \eqvsym
  \Parens{\sm{r:g\htpy h} r\circ f = p \ct \opp{q}}.
  \]
  However, here the right-hand side is a fiber of the map
  \[ (\blank\circ f) : \Parens{\prd{b:B} Q(b)} \to \Parens{\prd{a:A} Q(f(a)) } \]
  where $Q(b) \defeq (g(b)=h(b))$.
  Since $P$ is a family of $(k+1)$-types, $Q$ is a family of $k$-types, so the inductive hypothesis implies that this fiber is a $(k-n-2)$-type.
  Thus, all path spaces of $\hfib{(\blank\circ f)}{\ell}$ are $(k-n-2)$-types, so it is a $(k-n-1)$-type.
\end{proof}

Recall that if $\pairr{A,a_0}$ and $\pairr{B,b_0}$ are pointed types, then
their \define{wedge}
\index{wedge}%
$A\vee B$ is defined to be the pushout of $A\xleftarrow{a_0}
\unit\xrightarrow{b_0} B$.
There is a canonical map $i:A\vee B \to A\times B$ defined by the two maps $\lam{a} (a,b_0)$ and $\lam{b} (a_0,b)$; the following lemma essentially says that this map is highly connected if $A$ and $B$ are so.
It is a bit more convenient both to prove and use, however, if we use the characterization of connectedness from \cref{prop:nconnected_tested_by_lv_n_dependent types} and substitute in the universal property of the wedge (generalized to type families).

\begin{lem}[Wedge connectivity lemma]\label{thm:wedge-connectivity}
  Suppose that $\pairr{A,a_0}$ and $\pairr{B,b_0}$ are $n$- and $m$-connected pointed types, respectively, with $n,m\geq0$, and let
%
\narrowequation{P:A\to B\to \ntype{(n+m)}.}
%
Then for any ${f:\prd{a:A} P(a,b_0)}$ and ${g:\prd{b:B} P(a_0,b)}$ with $p:f(a_0) = g(b_0)$, there exists $h:\prd{a:A}{b:B} P(a,b)$ with homotopies
%
\begin{equation*}
  q:\prd{a:A} h(a,b_0)=f(a)
  \qquad\text{and}\qquad
  r:\prd{b:B} h(a_0,b)=g(b)
 \end{equation*}
%
such that $p = \opp{q(a_0)} \ct r(b_0)$.
\end{lem}
\begin{proof}
  Define $P:A\to\type$ by
  \[ P(a) \defeq \sm{k:\prd{b:B} P(a,b)} (f(a) = k(b_0)). \]
  Then we have $(g,p):P(a_0)$.
  Since $a_0:\unit\to A$ is $(n-1)$-connected, if $P$ is a family of $(n-1)$-types then we will have $\ell:\prd{a:A} P(a)$ such that $\ell(a_0) = (g,p)$, in which case we can define $h(a,b) \defeq \proj1(\ell(a))(b)$.
  However, for fixed $a$, the type $P(a)$ is the fiber over $f(a)$ of the map
  \[ \Parens{\prd{b:B} P(a,b) } \to P(a,b_0) \]
  given by precomposition with $b_0:\unit\to B$.
  Since $b_0:\unit\to B$ is $(m-1)$-connected, for this fiber to be $(n-1)$-truncated, by \cref{thm:conn-trunc-variable-ind} it suffices for each type $P(a,b)$ to be an $(n+m)$-type, which we have assumed.
\end{proof}

Let $(X,x_0)$ be a pointed type, and recall the definition of the suspension $\susp X$ from \cref{sec:suspension}, with constructors $\north,\south:\susp X$ and $\merid:X \to (\north=\south)$.
We regard $\susp X$ as a pointed space with basepoint $\north$, so that we have $\Omega\susp X \defeq (\id[\susp X]\north\north)$.
Then there is a canonical map
\begin{align*}
  \sigma &: X \to \Omega\susp X\\
  \sigma(x) &\defeq \merid(x) \ct \opp{\merid(x_0)}.
\end{align*}

\begin{rmk}
  In classical algebraic topology, one considers the \emph{reduced suspension}, in which the path $\merid(x_0)$ is collapsed down to a point, identifying $\north$ and $\south$.
  The reduced and unreduced suspensions are homotopy equivalent, so the distinction is invisible to our purely homotopy-theoretic eyes --- and higher inductive types only allow us to ``identify'' points up to a higher path anyway, there is no purpose to considering reduced suspensions in homotopy type theory.
  However, the ``unreducedness'' of our suspension is the reason for the (possibly unexpected) appearance of $\opp{\merid(x_0)}$ in the definition of $\sigma$.
\end{rmk}

Our goal is now to prove the following.

\begin{thm}[The Freudenthal suspension theorem]\label{thm:freudenthal}
  Suppose that $X$ is $n$-connected and pointed, with $n\geq 0$.
  Then the map $\sigma:X\to \Omega\susp(X)$ is $2n$-connected.
\end{thm}

\index{encode-decode method|(}%

We will use the encode-decode method, but applied in a slightly different way.
In most cases so far, we have used it to characterize the loop space $\Omega (A,a_0)$ of some type as equivalent to some other type $B$, by constructing a family $\code:A\to \type$ with $\code(a_0)\defeq B$ and a family of equivalences $\decode:\prd{x:A}\code(x) \eqvsym (a_0=x)$.
% We have also generalized it to characterize truncations of loop spaces by way of a family of equivalences $\prd{x:A}\code(x) \eqvsym \trunc n{a_0=x}$.

In this case, however, we want to show that $\sigma:X\to \Omega \susp X$ is $2n$-connected.
We could use a truncated version of the previous method, such as we will see in \cref{sec:van-kampen}, to prove that $\trunc{2n}X\to \trunc{2n}{\Omega \susp X}$ is an equivalence---but this is a slightly weaker statement than the map being $2n$-connected (see \cref{thm:conn-pik,thm:pik-conn}).
However, note that in the general case, to prove that $\decode(x)$ is an equivalence, we could equivalently be proving that its fibers are contractible, and we would still be able to use induction over the base type.
This we can generalize to prove connectedness of a map into a loop space, i.e.\ that the \emph{truncations} of its fibers are contractible.
Moreover, instead of constructing $\code$ and $\decode$ separately, we can construct directly a family of \emph{codes for the truncations of the fibers}.

\begin{defn}\label{thm:freudcode}
  If $X$ is $n$-connected and pointed with $n\geq 0$, then there is a family
  \begin{equation}
    \code:\prd{y:\susp X} (\north=y) \to \type\label{eq:freudcode}
  \end{equation}
  such that
  \begin{align}
    \code(\north,p) &\defeq \trunc{2n}{\hfib{\sigma}{p}}
    \jdeq \trunc{2n}{\tsm{x:X} (\merid(x) \ct \opp{\merid(x_0)} = p)}\label{eq:freudcodeN}\\
    \code(\south,q) &\defeq \trunc{2n}{\hfib{\merid}{q}}
    \jdeq \trunc{2n}{\tsm{x:X} (\merid(x) = q)}.\label{eq:freudcodeS}
  \end{align}
\end{defn}

Our eventual goal will be to prove that $\code(y,p)$ is contractible for all $y:\susp X$ and $p:\north=y$.
Applying this with $y\defeq \north$ will show that all fibers of $\sigma$ are $2n$-connected, and thus $\sigma$ is $2n$-connected.

\begin{proof}[Proof of \cref{thm:freudcode}]
  We define $\code(y,p)$ by induction on $y:\susp X$, where the first two cases are~\eqref{eq:freudcodeN} and~\eqref{eq:freudcodeS}.
  It remains to construct, for each $x_1:X$, a dependent path
  \[ \dpath{\lam{y}(\north=y)\to\type}{\merid(x_1)}{\code(\north)}{\code(\south)}. \]
  By \cref{thm:dpath-arrow}, this is equivalent to giving a family of paths
  \[ \prd{q:\north=\south} \code(\north)(\transfib{\lam{y}(\north=y)}{\opp{\merid(x_1)}}{q}) = \code(\south)(q). \]
  And by univalence and transport in path types, this is equivalent to a family of equivalences
  \[ \prd{q:\north=\south} \code(\north,q \ct \opp{\merid(x_1)}) \eqvsym \code(\south,q). \]
  We will define a family of maps
  \begin{equation}\label{eq:freudmap}
    \prd{q:\north=\south} \code(\north,q \ct \opp{\merid(x_1)}) \to \code(\south,q).
  \end{equation}
  and then show that they are all equivalences.
  Thus, let $q:\north=\south$; by the universal property of truncation and the definitions of $\code(\north,\blank)$ and $\code(\south,\blank)$, it will suffice to define for each $x_2:X$, a map
  \begin{equation*}
    \big(\merid(x_2)\ct \opp{\merid(x_0)} = q \ct \opp{\merid(x_1)}\big)
    \to \trunc{2n}{\tsm{x:X} (\merid(x) = q)}.
  \end{equation*}
  Now for each $x_1,x_2:X$, this type is $2n$-truncated, while $X$ is $n$-connected.
  Thus, by \cref{thm:wedge-connectivity}, it suffices to define this map when $x_1$ is $x_0$, when $x_2$ is $x_0$, and check that they agree when both are $x_0$.

  When $x_1$ is $x_0$, the hypothesis is $r:\merid(x_2)\ct \opp{\merid(x_0)} = q \ct \opp{\merid(x_0)}$.
  Thus, by canceling $\opp{\merid(x_0)}$ from $r$ to get $r':\merid(x_2)=q$, so we can define the image to be $\tproj{2n}{(x_2,r')}$.

  When $x_2$ is $x_0$, the hypothesis is $r:\merid(x_0)\ct \opp{\merid(x_0)} = q \ct \opp{\merid(x_1)}$.
  Rearranging this, we obtain $r'':\merid(x_1)=q$, and we can define the image to be $\tproj{2n}{(x_1,r'')}$.

  Finally, when both $x_1$ and $x_2$ are $x_0$, it suffices to show the resulting $r'$ and $r''$ agree; this is an easy lemma about path composition.
  This completes the definition of~\eqref{eq:freudmap}.
  To show that it is a family of equivalences, since being an equivalence is a mere proposition and $x_0:\unit\to X$ is (at least) $(-1)$-connected, it suffices to assume $x_1$ is $x_0$.
  In this case, inspecting the above construction we see that it is essentially the $2n$-truncation of the function that cancels $\opp{\merid(x_0)}$, which is an equivalence.
\end{proof}

In addition to~\eqref{eq:freudcodeN} and~\eqref{eq:freudcodeS}, we will need to extract from the construction of $\code$ some information about how it acts on paths.
For this we use the following lemma.

\begin{lem}\label{thm:freudlemma}
  Let $A:\UU$, $B:A\to \UU$, and $C:\prd{a:A} B(a)\to\UU$, and also $a_1,a_2:A$ with $m:a_1=a_2$ and $b:B(a_2)$.
  Then the function
  \[\transfib{\widehat{C}}{\pairpath(m,t)}{\blank} : C(a_1,\transfib{B}{\opp m}{b}) \to C(a_2,b),\]
  where $t:\transfib{B}{m}{\transfib{B}{\opp m}{b}} = b$ is the obvious coherence path and $\widehat{C}:(\sm{a:A} B(a)) \to\type$ is the uncurried form of $C$, is equal to the equivalence obtained by univalence from the composite
  \begin{align}
    C(a_1,\transfib{B}{\opp m}{b})
    &= \transfib{\lam{a} B(a)\to \UU}{m}{C(a_1)}(b)
    \tag{by~\eqref{eq:transport-arrow}}\\
    &= C(a_2,b). \tag{by $\happly(\apd{C}{m},b)$}
  \end{align}
\end{lem}
\begin{proof}
  By path induction, we may assume $a_2$ is $a_1$ and $m$ is $\refl{a_1}$, in which case both functions are the identity.
\end{proof}

We apply this lemma with $A\defeq\susp X$ and $B\defeq \lam{y}(\north=y)$ and $C\defeq\code$, while $a_1\defeq\north$ and $a_2\defeq\south$ and $m\defeq \merid(x_1)$ for some $x_1:X$, and finally $b\defeq q$ is some path $\north=\south$.
The computation rule for induction over $\susp X$ identifies $\apd{C}{m}$ with a path constructed in a certain way out of univalence and function extensionality.
The second function described in \cref{thm:freudlemma} essentially consists of undoing these applications of univalence and function extensionality, reducing back to the particular functions~\eqref{eq:freudmap} that we defined using \cref{thm:wedge-connectivity}.
Therefore, \cref{thm:freudlemma} says that transporting along $\pairpath(q,t)$ essentially recovers these functions.

Finally, by construction, when $x_1$ or $x_2$ coincides with $x_0$ and the input is in the image of $\tproj{2n}{\blank}$, we know more explicitly what these functions are.
Thus, for any $x_2:X$, we have
\begin{equation}
  \transfib{\hat{\code}}{\pairpath(\merid(x_0),t)}{\tproj{2n}{(x_2,r)}}
  =\tproj{2n}{(x_1,r')}\label{eq:freudcompute1}
\end{equation}
where $r:\merid(x_2) \ct \opp{\merid(x_0)} = \transfib{B}{\opp{\merid(x_0)}}{q}$ is arbitrary as before, and $r':\merid(x_2)=q$ is obtained from $r$ by identifying its end point with $q \ct \opp{\merid(x_0)}$ and canceling $\opp{\merid(x_0)}$.
Similarly, for any $x_1:X$, we have
\begin{equation}
  \transfib{\hat{\code}}{\pairpath(\merid(x_1),t)}{\tproj{2n}{(x_0,r)}}
  = \tproj{2n}{(x_1,r'')}\label{eq:freudcompute2}
\end{equation}
where $r:\merid(x_0) \ct \opp{\merid(x_0)} = \transfib{B}{\opp{\merid(x_1)}}{q}$, and $r'':\merid(x_1)=q$ is obtained by identifying its end point and rearranging paths.

\begin{proof}[Proof of \cref{thm:freudenthal}]
  It remains to show that $\code(y,p)$ is contractible for each $y:\susp X$ and $p:\north=y$.
  First we must choose a center of contraction, say $c(y,p):\code(y,p)$.
  This corresponds to the definition of the function $\encode$ in our previous proofs, so we define it by transport.
  Note that in the special case when $y$ is $\north$ and $p$ is $\refl{\north}$, we have
  \[\code(\north,\refl{\north}) \jdeq \trunc{2n}{\tsm{x:X} (\merid(x) \ct \opp{\merid(x_0)} = \refl{\north})}.\]
  Thus, we can choose $c(\north,\refl{\north})\defeq \tproj{2n}{(x_0,\mathsf{rinv}_{\merid(x_0)})}$, where $\mathrm{rinv}_q$ is the obvious path $q\ct\opp q = \refl{}$ for any $q$.
  We can now obtain $c:\prd{y:\susp X}{p:\north=y} \code(y,p)$ by path induction on $p$, but it will be important below that we can also give a concrete definition in terms of transport:
  \[ c(y,p) \defeq \transfib{\hat{\code}}{\pairpath(p,\mathsf{tid}_p)}{c(\north,\refl{\north})}
  \]
  where $\hat{\code}: \big(\sm{y:\susp X} (\north=y)\big) \to \type$ is the uncurried version of \code, and $\mathsf{tid}_p:\trans{p}{\refl{}} = p$ is a standard lemma.

  Next, we must show that every element of $\code(y,p)$ is equal to $c(y,p)$.
  Again, by path induction, it suffices to assume $y$ is $\north$ and $p$ is $\refl{\north}$.
  In fact, we will prove it more generally when $y$ is $\north$ and $p$ is arbitrary.
  That is, we will show that for any $p:\north=\north$ and $d:\code(\north,p)$ we have $d = c(\north,p)$.
  Since this equality is a $(2n-1)$-type, we may assume $d$ is of the form $\tproj{2n}{(x_1,r)}$ for some $x_1:X$ and $r:\merid(x_1) \ct \opp{\merid(x_0)} = p$.

  Now by a further path induction, we may assume that $r$ is reflexivity, and $p$ is $\merid(x_1) \ct \opp{\merid(x_0)}$.
  (This is why we generalized to arbitrary $p$ above.)
  Thus, we have to prove that
  \begin{equation}
    \tproj{2n}{(x_1, \refl{\merid(x_1) \ct \opp{\merid(x_0)}})}
    \;=\;
    c\left(\north,\refl{\merid(x_1) \ct \opp{\merid(x_0)}}\right).\label{eq:freudgoal}
  \end{equation}
  By definition, the right-hand side of this equality is
  \begin{multline*}
    \Transfib{\hat{\code}}{\pairpath(\merid(x_1) \ct \opp{\merid(x_0)}, \nameless)}{\tproj{2n}{(x_0,\nameless)}} \\
    = \transfibf{\hat{\code}}
    \begin{aligned}[t]
      \Big(
      &{\pairpath(\opp{\merid(x_0)}, \nameless)},\\
      &{\Transfib{\hat{\code}}{\pairpath(\merid(x_1), \nameless)}{\tproj{2n}{(x_0,\nameless)}}}
      \Big)
    \end{aligned}
    \\
    = \Transfib{\hat{\code}}{\pairpath(\opp{\merid(x_0)}, \nameless)}{\tproj{2n}{(x_1,\nameless)}}
    = \tproj{2n}{(x_1,\nameless)}
  \end{multline*}
  where the underscore $\nameless$ ought to be filled in with suitable coherence paths.
  Here the first step is functoriality of transport, the second invokes~\eqref{eq:freudcompute2}, and the third invokes~\eqref{eq:freudcompute1} (with transport moved to the other side).
  Thus we have the same first component as the left-hand side of~\eqref{eq:freudgoal}.
  We leave it to the reader to verify that the coherence paths all cancel, giving reflexivity in the second component.
\end{proof}

% As a corollary, we have the following equivalence.

\begin{cor}[Freudenthal Equivalence] \label{cor:freudenthal-equiv}
Suppose that $X$ is $n$-connected and pointed, with $n\geq 0$.
Then $\eqv{\trunc{2n}{X}}{\trunc{2n}{\Omega\susp(X)}}$.
\end{cor}
\begin{proof}
By \cref{thm:freudenthal}, $\sigma$ is $2n$-connected.  By
\cref{lem:connected-map-equiv-truncation}, it is therefore an
equivalence on $2n$-truncations.
\end{proof}

\index{encode-decode method|)}%

\index{Freudenthal suspension theorem|)}%
\index{theorem!Freudenthal suspension|)}%

\index{homotopy!group!of sphere}%
\index{stability!of homotopy groups of spheres}%
\index{type!n-sphere@$n$-sphere}%
One important corollary of the Freudenthal suspension theorem is that the homotopy groups of
spheres are stable in a certain range (these are the northeast-to-southwest diagonals
in \cref{tab:homotopy-groups-of-spheres}):

\begin{cor}[Stability for Spheres] \label{cor:stability-spheres}
If $k \le 2n-2$, then $\pi_{k+1}(S^{n+1}) = \pi_{k}(S^{n})$.
\end{cor}
\begin{proof}
Assume $k \le 2n-2$.
%
By \cref{cor:sn-connected}, $\Sn ^{n}$ is $\nminusone$-connected.  Therefore,
by \cref{cor:freudenthal-equiv},
\[
\trunc{2(n-1)}{\Omega(\susp(\Sn^{n}))} = \trunc{2(n-1)}{\Sn^{n}}.
\]
By \cref{lem:truncation-le}, because $k \le 2(n-1)$, applying $\trunc{k}{\blank}$
to both sides shows that this equation holds for $k$:
\begin{equation}\label{eq:freudenthal-for-spheres}
\trunc{k}{\Omega(\susp(\Sn^{n}))} = \trunc{k}{\Sn^{n}}.
\end{equation}
%
Then, the main idea of the proof is as follows; we omit checking that these
equivalences act appropriately on the base points of these spaces:
%
\begin{align*}
\pi_{k+1}(\Sn^{n+1}) &\jdeq \trunc{0}{\Omega^{k+1}(\Sn^{n+1})} \\
                     &\jdeq \trunc{0}{\Omega^k(\Omega(\Sn^{n+1}))} \\
                     &\jdeq \trunc{0}{\Omega^k(\Omega(\susp(\Sn^{n})))} \\
                     &= \Omega^k(\trunc{k}{(\Omega(\susp(\Sn^{n})))})
                     \tag{by \cref{thm:path-truncation}}\\
                     &= \Omega^k(\trunc{k}{\Sn^{n}})
                     \tag{by \eqref{eq:freudenthal-for-spheres}}\\
                     &= \trunc{0}{\Omega^k(\Sn^{n})}
                     \tag{by \cref{thm:path-truncation}}\\
                     &\jdeq \pi_k(\Sn^{n}). \qedhere
\end{align*}
%
\end{proof}

This means that once we have calculated one entry in one of these stable
diagonals, we know all of them.  For example:
\begin{thm}\label{thm:pinsn}
$\pi_n(\Sn^n)=\Z$ for every $n\geq 1$.
\end{thm}

\begin{proof}
The proof is by induction on $n$.  We already have $\pi_1(\Sn ^1) = \Z$
(\cref{cor:pi1s1}) and $\pi_2(\Sn ^2) = \Z$ (\cref{cor:pis2-hopf}).
When $n \ge 2$, $n \le (2n - 2)$. Therefore, by
\cref{cor:stability-spheres}, $\pi_{n+1}(S^{n+1}) = \pi_{n}(S^{n})$, and
this equivalence, combined with the inductive hypothesis, gives the result.
\end{proof}

\begin{cor}
  $\Sn^{n+1}$ is not an $n$-type for any $n\ge -1$.
\end{cor}

\begin{cor}\label{thm:pi3s2}
  $\pi_3(\Sn^2)=\Z$.
\end{cor}
\begin{proof}
  By \cref{cor:pis2-hopf}, $\pi_3(\Sn^2) = \pi_3(\Sn^3)$.
  But by \cref{thm:pinsn}, $\pi_3(\Sn^3) = \Z$.
\end{proof}

\section{The van Kampen theorem}
\label{sec:van-kampen}

\index{van Kampen theorem|(}%
\index{theorem!van Kampen|(}%

\index{fundamental!group}%
The van Kampen theorem calculates the fundamental group $\pi_1$ of a (homotopy) pushout of spaces.
It is traditionally stated for a topological space $X$ which is the union of two open subspaces $U$ and $V$, but in homotopy-theoretic terms this is just a convenient way of ensuring that $X$ is the pushout of $U$ and $V$ over their intersection.
Thus, we will prove a version of the van Kampen theorem for arbitrary pushouts.

In this section we will describe a proof of the van Kampen theorem which uses the same encode-decode method that we used for $\pi_1(\Sn^1)$ in \cref{sec:pi1-s1-intro}.
There is also a more homotopy-theoretic approach; see \cref{ex:rezk-vankampen}.

We need a more refined version of the encode-decode method.
In \cref{sec:pi1-s1-intro} (as well as in \cref{sec:compute-coprod,sec:compute-nat}) we used it to characterize the path space of a (higher) inductive type $W$ --- deriving as a consequence a characterization of the loop space $\Omega(W)$, and thereby also of its 0-truncation $\pi_1(W)$.
In the van Kampen theorem, our goal is only to characterize the fundamental group $\pi_1(W)$, and we do not have any explicit description of the loop spaces or the path spaces to use.

It turns out that we can use the same technique directly for a truncated version of the path fibration, thereby characterizing not only the fundamental \emph{group} $\pi_1(W)$, but also the whole fundamental \emph{groupoid}.
\index{fundamental!pregroupoid}%
Spe\-cif\-ical\-ly, for a type $X$, write $\Pi_1 X: X\to X\to \type$ for the $0$-truncation of its identity type, i.e.\ $\Pi_1 X(x,y) \defeq \trunc0{x=y}$.
Note that we have induced groupoid operations
\begin{align*}
  (\blank\ct\blank) &\;:\; \Pi_1X(x,y) \to \Pi_1X(y,z) \to \Pi_1X(x,z)\\
  \opp{(\blank)} &\;:\; \Pi_1X(x,y) \to \Pi_1X(y,x)\\
  \refl{x} &\;:\; \Pi_1X(x,x)\\
  \apfunc{f} &\;:\; \Pi_1X(x,y) \to \Pi_1Y(fx,fy)
\end{align*}
for which we use the same notation as the corresponding operations on paths.

\subsection{Naive van Kampen}
\label{sec:naive-vankampen}

We begin with a ``naive'' version of the van Kampen theorem, which is useful but not quite as useful as the classical version.
In \cref{sec:better-vankampen} we will improve it to a more useful version.

\index{encode-decode method|(}%

Given types $A,B,C$ and functions $f:A\to B$ and $g:A\to C$, let $P$ be their pushout $B\sqcup^A C$.
As we saw in \cref{sec:colimits}, $P$ is the higher inductive type generated by
\begin{itemize}
\item $i:B\to P$,
\item $j:C\to P$, and
\item for all $x:A$, a path $k x:ifx = jgx$.
\end{itemize}
Define $\code:P\to P\to \type$ by double induction on $P$ as follows.
\begin{itemize}
\item $\code(ib,ib')$ is a set-quotient (see \cref{sec:set-quotients}) of the type of sequences %pairs $(\vec a, \vec a', \vec p, \vec q)$
  \[ (b, p_0, x_1, q_1, y_1, p_1, x_2, q_2, y_2, p_2, \dots, y_n, p_n, b') \]
  where
  \begin{itemize}
  \item $n:\mathbb{N}$
  \item $x_k:A$ and $y_k:A$ for $0<k \le n$
  \item $p_0:\Pi_1B(b,f x_1)$ and $p_n:\Pi_1B(f y_n, b')$ for $n>0$, and $p_0:\Pi_1B(b,b')$ for $n=0$
  \item $p_k:\Pi_1B(f y_k, fx_{k+1})$ for $1\le k < n$
  \item $q_k:\Pi_1C(gx_k, gy_k)$ for $1\le k\le n$
  \end{itemize}
  The quotient is generated by the following equalities:
  \begin{align*}
    (\dots, q_k, y_k, \refl{fy_k}, y_k, q_{k+1},\dots)
    &= (\dots, q_k\ct q_{k+1},\dots)\\
    (\dots, p_k, x_k, \refl{gx_k}, x_k, p_{k+1},\dots)
    &= (\dots, p_k\ct p_{k+1},\dots)
  \end{align*}
  (see \cref{rmk:naive} below).
  We leave it to the reader to define this type of sequences precisely as an inductive type.
\item $\code(jc,jc')$ is identical, with the roles of $B$ and $C$ reversed.
  We likewise notationally reverse the roles of $x$ and $y$, and of $p$ and $q$.
\item $\code(ib,jc)$ and $\code(jc,ib)$ are similar, with the parity changed so that they start in one type and end in the other.
\item For $a:A$ and $b:B$, we require an equivalence
  \begin{equation}
    \code(ib, ifa) \eqvsym \code(ib,jga).\label{eq:bfa-bga}
  \end{equation}
  We define this to consist of the two functions defined on sequences by
  \begin{align*}
    (\dots, y_n, p_n,fa) &\mapsto (\dots,y_n,p_n,a,\refl{ga},ga),\\
    (\dots, x_n, p_n, a, \refl{fa}, fa) &\mapsfrom (\dots, x_n, p_n, ga).
  \end{align*}
  Both of these functions are easily seen to respect the equivalence relations, and hence to define functions on the types of codes.
  The left-to-right-to-left composite is
  \[ (\dots, y_n, p_n,fa) \mapsto
  (\dots,y_n,p_n,a,\refl{ga},a,\refl{fa},fa)
  \]
  which is equal to the identity by a generating equality of the quotient.
  The other composite is analogous.
  Thus we have defined an equivalence~\eqref{eq:bfa-bga}.
\item Similarly, we require equivalences
  \begin{align*}
    \code(jc,ifa) &\eqvsym \code(jc,jga)\\
    \code(ifa,ib)&\eqvsym (jga,ib)\\
    \code(ifa,jc)&\eqvsym (jga,jc)
  \end{align*}
  all of which are defined in exactly the same way (the second two by adding reflexivity terms on the beginning rather than the end).
\item Finally, we need to know that for $a,a':A$, the following diagram commutes:
  \begin{equation}\label{eq:bfa-bga-comm}
  \vcenter{\xymatrix{
      \code(ifa,ifa') \ar[r]\ar[d] &
      \code(ifa,jga')\ar[d]\\
      \code(jga,ifa')\ar[r] &
      \code(jga,jga')
      }}
  \end{equation}
  This amounts to saying that if we add something to the beginning and then something to the end of a sequence, we might as well have done it in the other order.
\end{itemize}

\begin{rmk}\label{rmk:naive}
  One might expect to see in the definition of \code some additional generating equations for the set-quotient, such as
  \begin{align*}
    (\dots, p_{k-1} \ct fw, x_{k}', q_{k}, \dots) &=
    (\dots, p_{k-1}, x_{k}, gw \ct q_{k}, \dots)
    \tag{for $w:\Pi_1A(x_{k},x_{k}')$}\\
    (\dots, q_k \ct gw, y_k', p_k, \dots) &=
    (\dots, q_k, y_k, fw \ct p_k, \dots).
    \tag{for $w:\Pi_1A(y_k, y_k')$}
  \end{align*}
  However, these are not necessary!
  In fact, they follow automatically by path induction on $w$.
  This is the main difference between the ``naive'' van Kampen theorem and the more refined one we will consider in the next subsection.
\end{rmk}

Continuing on, we can characterize transporting in the fibration $\code$:
\begin{itemize}
\item For $p:b=_B b'$ and $u:P$, we have
  \[ \mathsf{transport}^{b\mapsto \code(u,ib)}(p, (\dots, y_n,p_n,b))
  = (\dots,y_n,p_n\ct p,b').
  \]
\item For $q:c=_C c'$ and $u:P$, we have
  \[ \mathsf{transport}^{c\mapsto \code(u,jc)}(q, (\dots, x_n,q_n,c))
  = (\dots,x_n,q_n\ct q,c').
  \]
\end{itemize}
Here we are abusing notation by using the same name for a path in $X$ and its image in $\Pi_1X$.
Note that transport in $\Pi_1X$ is also given by concatenation with (the image of) a path.
From this we can prove the above statements by induction on $u$.
We also have:
\begin{itemize}
\item For $a:A$ and $u:P$,
  \[ \mathsf{transport}^{v\mapsto \code(u,v)}(ha, (\dots, y_n,p_n,fa))
  = (\dots,y_n,p_n,a,\refl{ga},ga).
  \]
\end{itemize}
This follows essentially from the definition of $\code$.

We also construct a function
\[ r : \prd{u:P} \code(u,u) \]
by induction on $u$ as follows:
\begin{align*}
  rib &\defeq (b,\refl{b},b)\\
  rjc &\defeq (c,\refl{c},c)
\end{align*}
and for $rka$ we take the composite equality
\begin{align*}
  (ka,ka)_* (fa,\refl{fa},fa)
  &= (ga,\refl{ga},a,\refl{fa},a,\refl{ga},ga) \\
  &= (ga,\refl{ga},ga)
\end{align*}
where the first equality is by the observation above about transporting in $\code$, and the second is an instance of the set quotient relation used to define $\code$.

We will now prove:
\begin{thm}[Naive van Kampen theorem]\label{thm:naive-van-kampen}
  For all $u,v:P$ there is an equivalence
  \[ \Pi_1P(u,v) \eqvsym \code(u,v). \]
\end{thm}
\begin{proof}

To define a function
\[ \encode : \Pi_1P(u,v) \to \code(u,v) \]
it suffices to define a function $(u=_P v) \to \code(u,v)$,
since $\code(u,v)$ is a set.
We do this by transport:
\[\encode(p) \defeq \mathsf{transport}^{v\mapsto \code(u,v)}(p,r(u)).\]
Now to define
\[ \decode: \code(u,v) \to \Pi_1P(u,v) \]
we proceed as usual by induction on $u,v:P$.
In each case for $u$ and $v$, we apply $i$ or $j$ to all the equalities $p_k$ and $q_k$ as appropriate and concatenate the results in $P$, using $h$ to identify the endpoints.
For instance, when $u\jdeq ib$ and $v\jdeq ib'$, we define
\begin{narrowmultline}\label{eq:decode}
 \decode(b, p_0, x_1, q_1, y_1, p_1, \dots, y_n, p_n, b') \defeq\narrowbreak
 (p_0)\ct h(x_1) \ct j(q_1) \ct \opp{h(y_1)} \ct i(p_1) \ct \cdots \ct \opp{h(y_n)}\ct i(p_n).
\end{narrowmultline}
This respects the set-quotient equivalence relation and the equivalences such as~\eqref{eq:bfa-bga}, since $h: fi \htpy gj$ is natural and $f$ and $g$ are functorial.

As usual, to show that the composite
\[ \Pi_1P(u,v) \xrightarrow{\encode} \code(u,v) \xrightarrow{\decode} \Pi_1P(u,v) \]
is the identity, we first peel off the 0-truncation (since the codomain is a set) and then apply path induction.
The input $\refl{u}$ goes to $ru$, which then goes back to $\refl u$ (applying a further induction on $u$ to decompose $\decode(ru)$).

Finally, consider the composite
\[  \code(u,v) \xrightarrow{\decode} \Pi_1P(u,v) \xrightarrow{\encode} \code(u,v). \]
We proceed by induction on $u,v:P$.
When $u\jdeq ib$ and $v\jdeq ib'$, this composite is
%
\begin{narrowmultline*}
(b, p_0, x_1, q_1, y_1, p_1, \dots, y_n, p_n, b')
\narrowbreak
\begin{aligned}[t]
  &\mapsto \Big(ip_0\ct hx_1 \ct jq_1 \ct \opp{hy_1} \ct ip_1 \ct \cdots \ct \opp{hy_n}\ct ip_n\Big)_*(rib)\\
  &= (ip_n)_* \cdots(jq_1)_* (hx_1)_*(ip_0)_*(b,\refl{b},b)\\
  &= (ip_n)_* \cdots(jq_1)_* (hx_1)_*(b,p_0,ifx_1)\\
  &= (ip_n)_* \cdots(jq_1)_* (b,p_0,x_1,\refl{gx_1},jgx_1)\\
  &= (ip_n)_* \cdots (b,p_0,x_1,q_1,jgy_1)\\
  &= \quad\vdots\\
  &= (b, p_0, x_1, q_1, y_1, p_1, \dots, y_n, p_n, b').
\end{aligned}
\end{narrowmultline*}
%
i.e., the identity function.
(To be precise, there is an implicit inductive argument needed here.)
The other three point cases are analogous, and the path cases are trivial since all the types are sets.
\end{proof}

\index{encode-decode method|)}%

\cref{thm:naive-van-kampen} allows us to calculate the fundamental groups of many types, provided $A$ is a set,
for in that case, each $\code(u,v)$ is, by definition, a set-quotient of a \emph{set} by a relation.

\begin{eg}\label{eg:circle}
  Let $A\defeq \bool$, $B\defeq\unit$, and $C\defeq \unit$.
  Then $P \eqvsym S^1$.
  Inspecting the definition of, say, $\code(i(\ttt),i(\ttt))$, we see that the paths all may as well be trivial, so the only information is in the sequence of elements $x_1,y_1,\dots,x_n,y_n: \bool$.
  Moreover, if we have $x_k=y_k$ or $y_k=x_{k+1}$ for any $k$, then the set-quotient relations allow us to excise both of those elements.
  Thus, every such sequence is equal to a canonical \emph{reduced} one in which no two adjacent elements are equal.
  Clearly such a reduced sequence is uniquely determined by its length (a natural number $n$) together with, if $n>1$, the information of whether $x_1$ is $\bfalse$ or $\btrue$, since that determines the rest of the sequence uniquely.
  And these data can, of course, be identified with an integer, where $n$ is the absolute value and $x_1$ encodes the sign.
  Thus we recover $\pi_1(S^1)\cong \Z$.
\end{eg}

Since \cref{thm:naive-van-kampen} asserts only a bijection of families of sets, this isomorphism $\pi_1(S^1)\cong \Z$ is likewise only a bijection of sets.
We could, however, define a concatenation operation on $\code$ (by concatenating sequences) and show that $\encode$ and $\decode$ form an isomorphism respecting this structure.
(In the language of \cref{cha:category-theory}, these would be ``pregroupoids''.)
We leave the details to the reader.

\index{fundamental!group|(}%

\begin{eg}\label{eg:suspension}
  More generally, let $B\defeq\unit$ and $C\defeq \unit$ but $A$ be arbitrary, so that $P$ is the suspension of $A$.
  Then once again the paths $p_k$ and $q_k$ are trivial, so that the only information in a path code is a sequence of elements $x_1,y_1,\dots,x_n,y_n: A$.
  The first two generating equalities say that adjacent equal elements can be canceled, so it makes sense to think of this sequence as a word of the form
  \[ x_1 y_1^{-1} x_2 y_2^{-1} \cdots x_n y_n^{-1} \]
  in a group.
  Indeed, it looks similar to the free group on $A$ (or equivalently on $\trunc0A$; see \cref{thm:freegroup-nonset}), but we are considering only words that start with a non-inverted element, alternate between inverted and non-inverted elements, and end with an inverted one.
  This effectively reduces the size of the generating set by one.
  For instance, if $A$ has a point $a:A$, then we can identify $\pi_1(\susp A)$ with the group presented by $\trunc0A$ as generators with the relation $\tproj0a = e$; see \cref{ex:vksusppt,ex:vksuspnopt} for details.
\end{eg}

\begin{eg}\label{eg:wedge}
  Let $A\defeq\unit$ and $B$ and $C$ be arbitrary, so that $f$ and $g$ simply equip $B$ and $C$ with basepoints $b$ and $c$, say.
  Then $P$ is the \emph{wedge} $B\vee C$ of $B$ and $C$ (the coproduct in the category of based spaces).
  In this case, it is the elements $x_k$ and $y_k$ which are trivial, so that the only information is a sequence of loops $(p_0,q_1,p_1,\dots,p_n)$ with $p_k:\pi_1(B,b)$ and $q_k:\pi_1(C,c)$.
  Such sequences, modulo the equivalence relation we have imposed, are easily identified with the explicit description of the \emph{free product} of the groups $\pi_1(B,b)$ and $\pi_1(C,c)$, as constructed in \cref{sec:free-algebras}.
  Thus, we have $\pi_1(B\vee C) \cong \pi_1(B) * \pi_1(C)$.
\end{eg}

\index{fundamental!group|)}%

However, \cref{thm:naive-van-kampen} stops just short of being the full classical van Kampen theorem, which handles
the case where $A$ is not necessarily a set,
and states that $\pi_1(B\sqcup^A C) \cong \pi_1(B) *_{\pi_1(A)} \pi_1(C)$ (with base point coming from $A$).
Indeed, the conclusion of \cref{thm:naive-van-kampen} says nothing at all about $\pi_1(A)$; the paths in $A$ are ``built into the quotienting'' in a type-theoretic way that makes it hard to extract explicit information, in that $\code(u,v)$ is a set-quotient of a non-set by a relation.
For this reason, in the next subsection we consider a better version of the van Kampen theorem.


\subsection{The van Kampen theorem with a set of basepoints}
\label{sec:better-vankampen}

\index{basepoint!set of}%
The improvement of van Kampen we present now is closely analogous to a similar improvement in classical algebraic topology, where $A$ is equip\-ped with a \emph{set $S$ of base points}.
In fact, it turns out to be unnecessary for our proof to assume that the ``set of basepoints'' is a \emph{set} --- it might just as well be an arbitrary type; the utility of assuming $S$ is a set arises later, when applying the theorem to obtain computations.
What is important is that $S$ contains at least one point in each connected component of $A$.
We state this in type theory by saying that we have a type $S$ and a function $k:S \to A$ which is surjective, i.e.\ $(-1)$-connected.
If $S\jdeq A$ and $k$ is the identity function, then we will recover the naive van Kampen theorem.
Another example to keep in mind is when $A$ is pointed and (0-)connected, with $k:\unit\to A$ the point: by \cref{thm:minusoneconn-surjective,thm:connected-pointed} this map is surjective just when $A$ is 0-connected.

Let $A,B,C,f,g,P,i,j,h$ be as in the previous section.
We now define, given our surjective map $k:S\to A$, an auxiliary type which improves the connectedness of $k$.
Let $T$ be the higher inductive type generated by
\begin{itemize}
\item A function $\ell:S\to T$, and
\item For each $s,s':S$, a function $m:(\id[A]{ks}{ks'}) \to (\id[T]{\ell s}{\ell s'})$.
\end{itemize}
There is an obvious induced function $\kbar:T\to A$ such that $\kbar \ell = k$, and any $p:ks=ks'$ is equal to the composite $ks = \kbar \ell s \overset{\kbar m p}{=} \kbar \ell s' = k s'$.

\begin{lem}\label{thm:kbar}
  $\kbar$ is 0-connected.
\end{lem}
\begin{proof}
  We must show that for all $a:A$, the 0-truncation of the type $\sm{t:T}(\kbar t = a)$ is contractible.
  Since contractibility is a mere proposition and $k$ is $(-1)$-connected, we may assume that $a=ks$ for some $s:S$.
  Now we can take the center of contraction to be $\tproj0{(\ell s,q)}$ where $q$ is the equality $\kbar\ell s = k s$.

  It remains to show that for any $\phi:\trunc0{\sm{t:T} (\kbar t = ks)}$ we have $\phi = \tproj0{(\ell s,q)}$.
  Since the latter is a mere proposition, and in particular a set, we may assume that $\phi=\tproj0{(t,p)}$ for $t:T$ and $p:\kbar t = ks$.

  Now we can do induction on $t:T$.
  If $t\jdeq\ell s'$, then $ks' = \kbar \ell s' \overset{p}{=} ks$ yields via $m$ an equality $\ell s = \ell s'$.
  Hence by definition of $\kbar$ and of equality in homotopy fibers, we obtain an equality $(ks',p) = (ks,q)$, and thus $\tproj0{(ks',p)} = \tproj0{(ks,q)}$.
  Next we must show that as $t$ varies along $m$ these equalities agree.
  But they are equalities in a set (namely $\trunc0{\sm{t:T} (\kbar t = ks)}$), and hence this is automatic.
\end{proof}

\begin{rmk}
  \index{kernel!pair}%
  $T$ can be regarded as the (homotopy) coequalizer of the ``kernel pair'' of $k$.
  If $S$ and $A$ were sets, then the $(-1)$-connectivity of $k$ would imply that $A$ is the $0$-truncation of this coequalizer (see \cref{cha:set-math}).
  For general types, higher topos theory suggests that $(-1)$-con\-nec\-tiv\-i\-ty of $k$ will imply instead that $A$ is the colimit (a.k.a.\ ``geometric realization'') of the ``simplicial kernel'' of $k$.
  \index{.infinity1-topos@$(\infty,1)$-topos}%
  \index{geometric realization}%
  \index{simplicial!kernel}%
  \index{kernel!simplicial}%
  The type $T$ is the colimit of the ``1-skeleton'' of this simplicial kernel, so it makes sense that it improves the connectivity of $k$ by $1$.
  More generally, we might expect the colimit of the $n$-skeleton\index{skeleton!of a CW-complex} to improve connectivity by $n$.
\end{rmk}

\index{encode-decode method|(}%

Now we define $\code:P\to P\to \type$ by double induction as follows
\begin{itemize}
\item $\code(ib,ib')$ is now a set-quotient of the type of sequences
  \[ (b, p_0, x_1, q_1, y_1, p_1, x_2, q_2, y_2, p_2, \dots, y_n, p_n, b') \]
  where
  \begin{itemize}
  \item $n:\mathbb{N}$,
  \item $x_k:S$ and $y_k:S$ for $0<k \le n$,
  \item $p_0:\Pi_1B(b,f k x_1)$ and $p_n:\Pi_1B(f k y_n, b')$ for $n>0$, and $p_0:\Pi_1B(b,b')$ for $n=0$,
  \item $p_k:\Pi_1B(fk y_k, fkx_{k+1})$ for $1\le k < n$,
  \item $q_k:\Pi_1C(gkx_k, gky_k)$ for $1\le k\le n$.
  \end{itemize}
  The quotient is generated by the following equalities (see \cref{rmk:naive}):
  \begin{align*}
    (\dots, q_k, y_k, \refl{fy_k}, y_k, q_{k+1},\dots)
    &= (\dots, q_k\ct q_{k+1},\dots)\\
    (\dots, p_k, x_k, \refl{gx_k}, x_k, p_{k+1},\dots)
    &= (\dots, p_k\ct p_{k+1},\dots)\\
    (\dots, p_{k-1} \ct fw, x_{k}', q_{k}, \dots) &=
    (\dots, p_{k-1}, x_{k}, gw \ct q_{k}, \dots)
    \tag{for $w:\Pi_1A(kx_{k},kx_{k}')$}\\
    (\dots, q_k \ct gw, y_k', p_k, \dots) &=
    (\dots, q_k, y_k, fw \ct p_k, \dots).
    \tag{for $w:\Pi_1A(ky_k, ky_k')$}
  \end{align*}
  We will need below the definition of the case of $\decode$ on such a sequence, which as before concatenates all the paths $p_k$ and $q_k$ together with instances of $h$ to give an element of $\Pi_1P(ifb,ifb')$, cf.~\eqref{eq:decode}.
  As before, the other three point cases are nearly identical.
\item For $a:A$ and $b:B$, we require an equivalence
  \begin{equation}
    \code(ib, ifa) \eqvsym \code(ib,jga).\label{eq:bfa-bga2}
  \end{equation}
  Since $\code$ is set-valued, by \cref{thm:kbar} we may assume that $a=\kbar t$ for some $t:T$.
  Next, we can do induction on $t$.
  If $t\jdeq \ell s$ for $s:S$, then we define~\eqref{eq:bfa-bga2} as in \cref{sec:naive-vankampen}:
  \begin{align*}
    (\dots, y_n, p_n,fks) &\mapsto (\dots,y_n,p_n,s,\refl{gks},gks),\\
    (\dots, x_n, p_n, s, \refl{fks}, fks) &\mapsfrom (\dots, x_n, p_n, gks).
  \end{align*}
  These respect the equivalence relations, and define quasi-inverses just as before.
  Now suppose $t$ varies along $m_{s,s'}(w)$ for some $w:ks=ks'$; we must show that~\eqref{eq:bfa-bga2} respects transporting along $\kbar mw$.
  By definition of $\kbar$, this essentially boils down to transporting along $w$ itself.
  By the characterization of transport in path types, what we need to show is that
  \[ w_*(\dots, y_n, p_n,fks) = (\dots,y_n, p_n \ct fw, fks') \]
  is mapped by~\eqref{eq:bfa-bga2} to
  \[ w_*(\dots,y_n,p_n,s,\refl{gks},gks) = (\dots, y_n, p_n, s, \refl{gks} \ct gw, gks') \]
  But this follows directly from the new generators we have imposed on the set-quotient relation defining \code.
\item The other three requisite equivalences are defined similarly.
\item Finally, since the commutativity~\eqref{eq:bfa-bga-comm} is a mere proposition, by $(-1)$-connectedness of $k$ we may assume that $a=ks$ and $a'=ks'$, in which case it follows exactly as before.
\end{itemize}

\begin{thm}[van Kampen with a set of basepoints]\label{thm:van-Kampen}
  For all $u,v:P$ there is an equivalence
  \[ \Pi_1P(u,v) \eqvsym \code(u,v). \]
  with \code defined as in this section.
\end{thm}

\begin{proof}
  Basically just like before.
  To show that $\decode$ respects the new generators of the quotient relation, we use the naturality of $h$.
  And to show that $\decode$ respects the equivalences such as~\eqref{eq:bfa-bga2}, we need to induct on $\kbar$ and on $T$ in order to decompose those equivalences into their definitions, but then it becomes again simply functoriality of $f$ and $g$.
  The rest is easy.
  In particular, no additional argument is required for $\encode\circ\decode$, since the goal is to prove an equality in a set, and so the case of $h$ is trivial.
\end{proof}

\index{encode-decode method|)}%

\index{fundamental!group|(}%
\cref{thm:van-Kampen} allows us to calculate the fundamental group of a space~$A$,
even when $A$ is not a set, provided $S$ is a set, for in that case,
each $\code(u,v)$ is, by definition, a set-quotient of a \emph{set} by a
relation.  In that respect, it is an improvement over
\cref{thm:naive-van-kampen}.

\begin{eg}\label{eg:clvk}
  Suppose $S\defeq \unit$, so that $A$ has a basepoint $a \defeq k(\ttt)$ and is connected.
  Then code for loops in the pushout can be identified with alternating sequences of loops in $\pi_1(B,f(a))$ and $\pi_1(C,g(a))$, modulo an equivalence relation which allows us to slide elements of $\pi_1(A,a)$ between them (after applying $f$ and $g$ respectively).
  Thus, $\pi_1(P)$ can be identified with the \emph{amalgamated free product}
  \index{amalgamated free product}%
  \index{free!product!amalgamated}%
  $\pi_1(B) *_{\pi_1(A)} \pi_1(C)$ (the pushout in the category of groups), as constructed in \cref{sec:free-algebras}.
  This (in the case when $B$ and $C$ are open subspaces of $P$ and $A$ their intersection) is probably the most classical version of the van Kampen theorem.
\end{eg}

\begin{eg}\label{eg:cofiber}
  \index{cofiber}
  As a special case of \cref{eg:clvk}, suppose additionally that $C\defeq\unit$, so that $P$ is the cofiber $B/A$.
  Then every loop in $C$ is equal to reflexivity, so the relations on path codes allow us to collapse all sequences to a single loop in $B$.
  The additional relations require that multiplying on the left, right, or in the middle by an element in the image of $\pi_1(A)$ is the identity.
  We can thus identify $\pi_1(B/A)$ with the quotient of the group $\pi_1(B)$ by the normal subgroup generated by the image of $\pi_1(A)$.
\end{eg}

\begin{eg}\label{eg:torus}
  \index{torus}
  As a further special case of \cref{eg:cofiber}, let $B\defeq S^1 \vee S^1$, let $A\defeq S^1$, and let $f:A\to B$ pick out the composite loop $p \ct q \ct \opp p \ct \opp q$, where $p$ and $q$ are the generating loops in the two copies of $S^1$ comprising $B$.
  Then $P$ is a presentation of the torus $T^2$.
  Indeed, it is not hard to identify $P$ with the presentation of $T^2$ as described in \cref{sec:hubs-spokes}, using the cone on a particular loop.
  Thus, $\pi_1(T^2)$ is the quotient of the free group on two generators\index{generator!of a group} (i.e., $\pi_1(B)$) by the relation $p \ct q \ct \opp p \ct \opp q = 1$.
  This clearly yields the free \emph{abelian}\index{group!abelian} group on two generators, which is $\Z\times\Z$.
\end{eg}


\begin{eg}
  \index{CW complex}
  \index{hub and spoke}
  More generally, any CW complex can be obtained by repeatedly ``coning off'' spheres, as described in \cref{sec:hubs-spokes}.
  That is, we start with a set $X_0$ of points (``0-cells''), which is the ``0-skeleton'' of the CW complex.
  We take the pushout
  \begin{equation*}
    \vcenter{\xymatrix{
        S_1 \times \Sn^0\ar[r]^-{f_1}\ar[d] &
        X_0\ar[d]\\
        \unit \ar[r] &
        X_1
      }}
  \end{equation*}
  for some set $S_1$ of 1-cells and some family $f_1$ of ``attaching maps'', obtaining the ``1-skeleton''\index{skeleton!of a CW-complex} $X_1$.
  \index{attaching map}%
  Then we take the pushout
  \begin{equation*}
    \vcenter{\xymatrix{
        S_2 \times \Sn^1\ar[r]^{f_2}\ar[d] &
        X_1\ar[d]\\
        \unit \ar[r] &
        X_2
      }}
  \end{equation*}
  for some set $S_2$ of 2-cells and some family $f_2$ of attaching maps, obtaining the 2-skeleton $X_2$, and so on.
  The fundamental group of each pushout can be calculated from the van Kampen theorem: we obtain the group presented by generators derived from the 1-skeleton, and relations derived from $S_2$ and $f_2$.
  The pushouts after this stage do not alter the fundamental group, since $\pi_1(\Sn^n)$ is trivial for $n>1$ (see \cref{sec:pik-le-n}).
\end{eg}


\begin{eg}\label{eg:kg1}
  In particular, suppose given any presentation\index{presentation!of a group} of a (set-)group $G = \langle X \mid R \rangle$, with $X$ a set of generators and $R$ a set of words in these generators\index{generator!of a group}.
  Let $B\defeq \bigvee_X S^1$ and $A\defeq \bigvee_R S^1$, with $f:A\to B$ sending each copy of $S^1$ to the corresponding word in the generating loops of $B$.
  It follows that $\pi_1(P) \cong G$; thus we have constructed a connected type whose fundamental group is $G$.
  Since any group has a presentation, any group is the fundamental group of some type.
  If we 1-truncate such a type, we obtain a type whose only nontrivial homotopy group is $G$; this is called an \define{Eilenberg--Mac Lane space} $K(G,1)$.%
  \indexdef{Eilenberg--Mac Lane space}%
\end{eg}

\index{fundamental!group|)}%

\index{van Kampen theorem|)}%
\index{theorem!van Kampen|)}%

\section{Whitehead's theorem and Whitehead's principle}
\label{sec:whitehead}

In classical homotopy theory, a map $f:A\to B$ which induces an isomorphism $\pi_n(A,a) \cong \pi_n(B,f(a))$ for all points $a$ in $A$ (and also an isomorphism $\pi_0(A)\cong\pi_0(B)$) is necessarily a homotopy equivalence, as long as the spaces $A$ and $B$ are well-behaved (e.g.\ have the homotopy types of CW-complexes).
\index{theorem!Whitehead's}%
\index{Whitehead's!theorem}%
This is known as \emph{Whitehead's theorem}.
In fact, the ``ill-behaved'' spaces for which Whitehead's theorem fails are invisible to type theory.
Roughly, the well-behaved topological spaces suffice to present $\infty$-groupoids,%
\index{.infinity-groupoid@$\infty$-groupoid}
and homotopy type theory deals with $\infty$-groupoids directly rather than actual topological spaces.
Thus, one might expect that Whitehead's theorem would be true in univalent foundations.

However, this is \emph{not} the case: Whitehead's theorem is not provable.
In fact, there are known models of type theory in which it fails to be true, although for entirely different reasons than its failure for ill-behaved topological spaces.
These models are ``non-hypercomplete $\infty$-toposes''
\index{.infinity1-topos@$(\infty,1)$-topos}%
\index{.infinity1-topos@$(\infty,1)$-topos!non-hypercomplete}%
(see~\cite{lurie:higher-topoi}); roughly speaking, they consist of sheaves of $\infty$-groupoids over $\infty$-dimensional base spaces.

\index{axiom!Whitehead's principle|(}%
\index{Whitehead's!principle|(}%

From a foundational point of view, therefore, we may speak of \emph{Whitehead's principle} as a ``classicality axiom'', akin to \LEM{} and \choice{}.
It may consistently be assumed, but it is not part of the computationally motivated type theory, nor does it hold in all natural models.
But when working from set-theoretic foundations, this principle is invisible: it cannot fail to be true in a world where $\infty$-groupoids are built up out of sets (using topological spaces, simplicial sets, or any other such model).

This may seem odd, but actually it should not be surprising.
Homotopy type theory is the \emph{abstract} theory of homotopy types, whereas the homotopy theory of topological spaces or simplicial sets in set theory is a \emph{concrete} model of this theory, in the same way that the integers are a concrete model of the abstract theory of rings.
It is to be expected that any concrete model will have special properties which are not intrinsic to the corresponding abstract theory, but which we might sometimes want to assume as additional axioms (e.g.\ the integers are a Principal Ideal Domain, but not all rings are).

It is beyond the scope of this book to describe any models of type theory, so we will not explain how Whitehead's principle might fail in some of them.
However, we can prove that it holds whenever the types involved are $n$-truncated for some finite $n$, by ``downward'' induction on $n$.
In addition to being of interest in its own right (for instance, it implies the essential uniqueness of Eilenberg--Mac Lane spaces), the proof of this result will hopefully provide some intuitive explanation for why we cannot hope to prove an analogous theorem without truncation hypotheses.

We begin with the following modification of \cref{thm:mono-surj-equiv}, which will eventually supply the induction step in the proof of the truncated Whitehead's principle.
It may be regarded as a type-theoretic, $\infty$-group\-oid\-al version of the classical statement that a fully faithful and essentially surjective functor is an equivalence of categories.

\begin{thm}\label{thm:whitehead0}
  Suppose $f:A\to B$ is a function such that
  \begin{enumerate}
  \item $\trunc0 f : \trunc0 A \to \trunc0 B$ is surjective, and\label{item:whitehead01}
  \item for any $x,y:A$, the function $\apfunc f : (\id[A]xy) \to (\id[B]{f(x)}{f(y)})$ is an equivalence.\label{item:whitehead02}
  \end{enumerate}
  Then $f$ is an equivalence.
\end{thm}
\begin{proof}
  Note that~\ref{item:whitehead02} is precisely the statement that $f$ is an embedding, c.f.~\cref{sec:mono-surj}.
  Thus, by \cref{thm:mono-surj-equiv}, it suffices to show that $f$ is surjective, i.e.\ that for any $b:B$ we have $\trunc{-1}{\hfib f b}$.
  Suppose given $b$; then since $\trunc0 f$ is surjective, there merely exists an $a:A$ such that $\trunc 0 f(\tproj0a) = \tproj0b$.
  And since our goal is a mere proposition, we may assume given such an $a$.
  Then we have $\tproj0{f(a)} = \trunc 0 f(\tproj0a) =\tproj0b$, hence $\trunc{-1}{f(a)=b}$.
  Again, since our goal is still a mere proposition, we may assume $f(a)=b$.
  Hence $\hfib f b$ is inhabited, and thus merely inhabited.
\end{proof}

Since homotopy groups are truncations of loop spaces\index{loop space}, rather than path spaces, we need to modify this theorem to speak about these instead.

\begin{cor}\label{thm:whitehead1}
  Suppose $f:A\to B$ is a function such that
  \begin{enumerate}
  \item $\trunc0 f : \trunc0 A \to \trunc0 B$ is a bijection, and
  \item for any $x:A$, the function $\apfunc f : \Omega(A,x) \to \Omega(B,f(x))$ is an equivalence.
  \end{enumerate}
  Then $f$ is an equivalence.
\end{cor}
\begin{proof}
  By \cref{thm:whitehead0}, it suffices to show that $\apfunc f : (\id[A]xy) \to (\id[B]{f(x)}{f(y)})$ is an equivalence for any $x,y:A$.
  And by \cref{thm:equiv-inhabcod}, we may assume $\id[B]{f(x)}{f(y)}$.
  In particular, $\tproj0{f(x)} = \tproj0{f(y)}$, so since $\trunc0 f$ is an equivalence, we have $\tproj0 x = \tproj0y$, hence $\tproj{-1}{x=y}$.
  Since we are trying to prove a mere proposition ($f$ being an equivalence), we may assume given $p:x=y$.
  But now the following square commutes up to homotopy:
  \begin{equation*}
  \vcenter{\xymatrix@C=3pc{
      \Omega(A,x)\ar[r]^-{\blank\ct p}\ar[d]_{\apfunc f} &
      (\id[A]xy) \ar[d]^{\apfunc f}\\
      \Omega(B,f(x))\ar[r]_-{\blank\ct f(p)} &
      (\id[B]{f(x)}{f(y)}).
      }}
  \end{equation*}
  The top and bottom maps are equivalences, and the left-hand map is so by assumption.
  Hence, by the 2-out-of-3 property, so is the right-hand map.
\end{proof}

Now we can prove the truncated Whitehead's principle.

\begin{thm}\label{thm:whiteheadn}
  Suppose $A$ and $B$ are $n$-types and $f:A\to B$ is such that
  \begin{enumerate}
  \item $\trunc0f:\trunc0A \to \trunc0B$ is an isomorphism, and\label{item:wh0}
  \item $\pi_k(f):\pi_k(A,x) \to \pi_k(B,f(x))$ is a bijection for all $k\ge 1$ and all $x:A$.\label{item:whk}
  \end{enumerate}
  Then $f$ is an equivalence.
\end{thm}

\noindent
Condition~\ref{item:wh0} is almost the case of~\ref{item:whk} when $k=0$, except that it makes no reference to any basepoint $x:A$.

\begin{proof}
  We proceed by induction on $n$.
  When $n=-2$, the statement is trivial.
  Thus, suppose it to be true for all functions between $n$-types, and let $A$ and $B$ be $(n+1)$-types and $f:A\to B$ as above.
  The first condition in \cref{thm:whitehead1} holds by assumption, so it will suffice to show that for any $x:A$, the function $\apfunc f: \Omega(A,x) \to \Omega(B,f(x))$ is an equivalence.
  However, $\Omega(A,x)$ and $\Omega(B,f(x))$ are $n$-types, and $\pi_k(\apfunc f) = \pi_{k+1}(f)$, so this follows from the inductive hypothesis.
\end{proof}

Note that if $A$ and $B$ are not $n$-types for any finite $n$, then there is no way for the induction to get started.

\begin{cor}\label{thm:whitehead-contr}
  If $A$ is a $0$-connected $n$-type and $\pi_k(A,a)=0$ for all $k$ and $a:A$, then $A$ is contractible.
\end{cor}
\begin{proof}
  Apply \cref{thm:whiteheadn} to the map $A\to\unit$.
\end{proof}

As an application, we can deduce the converse of \cref{thm:conn-pik}.

\begin{cor}\label{thm:pik-conn}
  For $n\ge 0$, a map $f:A\to B$ is $n$-connected if and only if the following all hold:
  \begin{enumerate}
  \item $\trunc0f:\trunc0A \to \trunc0B$ is an isomorphism.
  \item For any $a:A$ and $k\le n$, the map $\pi_k(f):\pi_k(A,a) \to \pi_k(B,f(a))$ is an isomorphism.
  \item For any $a:A$, the map $\pi_{n+1}(f):\pi_{n+1}(A,a) \to \pi_{n+1}(B,f(a))$ is surjective.
  \end{enumerate}
\end{cor}
\begin{proof}
  The ``only if'' direction is \cref{thm:conn-pik}.
  Conversely, by the long exact sequence of a fibration (\cref{thm:les}),
  \index{sequence!exact}%
  the hypotheses imply that $\pi_k(\hfib f {f(a)})=0$ for all $k\le n$ and $a:A$, and that $\trunc 0{\hfib f{f(a)}}$ is contractible.
  Since $\pi_k(\hfib f {f(a)}) = \pi_k(\trunc n{\hfib f{f(a)}})$ for $k\le n$, and $\trunc n{\hfib f{f(a)}}$ is $n$-connected, by \cref{thm:whitehead-contr} it is contractible for any $a$.

  It remains to show that $\trunc n{\hfib f{b}}$ is contractible for $b:B$ not necessarily of the form $f(a)$.
  However, by assumption, there is $x:\trunc0A$ with $\tproj 0b = \trunc0f(x)$.
  Since contractibility is a mere proposition, we may assume $x$ is of the form $\tproj0a$ for $a:A$, in which case $\tproj 0 b = \trunc0f(\tproj0a) = \tproj0{f(a)}$, and therefore $\trunc{-1}{b=f(a)}$.
  Again since contractibility is a mere proposition, we may assume $b=f(a)$, and the result follows.
\end{proof}

A map $f$ such that $\trunc0f$ is a bijection and $\pi_k(f)$ is a bijection for all $k$ is called \define{$\infty$-connected}%
\indexdef{function!.infinity-connected@$\infty$-connected}%
\indexdef{.infinity-connected function@$\infty$-connected function}
or a \define{weak equivalence}.%
\indexdef{equivalence!weak}%
\indexdef{weak equivalence!of types}
This is equivalent to asking that $f$ be $n$-connected for all $n$.
A type $Z$ is called \define{$\infty$-truncated}%
\indexdef{type!.infinity-truncated@$\infty$-truncated}%
\indexdef{.infinity-truncated type@$\infty$-truncated type}
or \define{hypercomplete}%
\indexdef{type!hypercomplete}%
\indexdef{hypercomplete type}
if the induced map
\[(\blank\circ f):(B\to Z) \to (A\to Z)\]
is an equivalence whenever $f$ is $\infty$-connected --- that is, if $Z$ thinks every $\infty$-connected map is an equivalence.
\indexdef{axiom!Whitehead's principle}%
Then if we want to assume Whitehead's principle as an axiom, we may use either of the following equivalent forms.
\begin{itemize}
\item Every $\infty$-connected function is an equivalence.
\item Every type is $\infty$-truncated.
\end{itemize}
In higher topos models,
\index{.infinity1-topos@$(\infty,1)$-topos}%
the $\infty$-truncated types form a reflective subuniverse in the sense of
\cref{sec:modalities} (the ``hypercompletion'' of an $(\infty,1)$-topos), but we do not know whether this is
true in general.

\index{axiom!Whitehead's principle|)}%
\index{Whitehead's!principle|)}%

It may not be obvious that there \emph{are} any types which are not $n$-types for any $n$, but in fact there are.
Indeed, in classical homotopy theory, $\Sn^n$ has this property for any $n\ge 2$.
We have not proven this fact in homotopy type theory yet, but there are other types which we can prove to have ``infinite truncation level''.

\begin{eg}
  Suppose we have $B:\nat\to\type$ such that for each $n$, the type $B(n)$ contains an $n$-loop\index{loop!n-@$n$-} which is not equal to $n$-fold reflexivity, say $p_n:\Omega^n(B(n),b_n)$ with $p_n \neq \refl{b_n}^n$.
  (For instance, we could define $B(n)\defeq \Sn^n$, with $p_n$ the image of $1:\Z$ under the isomorphism $\pi_n(\Sn^n)\cong \Z$.)
  Consider $C\defeq \prd{n:\nat} B(n)$, with the point $c:C$ defined by $c(n)\defeq b_n$.
  Since loop spaces commute with products, for any $m$ we have
  \[\eqvspaced{\Omega^m (C,c)}{\prd{n:\nat}\Omega^m(B(n),b_n)}.\]
  Under this equivalence, $\refl{c}^m$ corresponds to the function $(n\mapsto \refl{b_n}^m)$.
  Now define $q_m$ in the right-hand type by
  \[ q_m(n) \defeq
  \begin{cases}
    p_n &\quad m=n\\
    \refl{b_n}^m &\quad m\neq n.
  \end{cases}
  \]
  If we had $q_m = (n\mapsto \refl{b_n}^m)$, then we would have $p_n = \refl{b_n}^n$, which is not the case.
  Thus, $q_m \neq (n\mapsto \refl{b_n}^m)$, and so there is a point of $\Omega^m(C,c)$ which is unequal to $\refl{c}^m$.
  Hence $C$ is not an $m$-type, for any $m:\nat$.
\end{eg}

We expect it should also be possible to show that a universe $\UU$ itself is not an $n$-type for any $n$, using the fact that it contains higher inductive types such as $\Sn^n$ for all $n$.
However, this has not yet been done.

\section{A general statement of the encode-decode method}
\label{sec:general-encode-decode}

\indexdef{encode-decode method}

We have used the encode-decode method to characterize the path spaces
of various types, including coproducts (\cref{thm:path-coprod}), natural
numbers (\cref{thm:path-nat}), truncations (\cref{thm:path-truncation}),
the circle (\cref{{cor:omega-s1}}), suspensions (\cref{thm:freudenthal}), and pushouts
(\cref{thm: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(\Sn^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 \cref{thm:path-coprod,cor:omega-s1}) or
a whole path space (as in \cref{thm:path-nat}), to give a complete
characterization of a loop space (e.g.\ $\Omega^1(\Sn ^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 \cref{thm:path-coprod} and \cref{{cor:omega-s1}}.

\begin{lem}[Encode-decode for Loop Spaces]
  \index{loop space}%
Given a pointed type $(A,a_0)$ and a fibration
$\code : A \to \type$, if
\begin{enumerate}
\item $c_0 : \code(a_0)$,\label{item:ed1}
\item $\decode : \prd{x:A} \code(x) \to (\id{a_0}{x})$,\label{item:ed2}
\item for all $c : \code(a_0)$, \id{\transfib{\code}{\decode(c)}{c_0}}{c}, and\label{item:ed3}
\item $\id{\decode(c_0)}{\refl{}}$,\label{item:ed4}
\end{enumerate}
then $(\id{a_0}{a_0})$ is equivalent to $\code(a_0)$.
\end{lem}

\begin{proof}
Define
$\encode : \prd{x:A} (\id{a_0}{x}) \to \code(x)$ by
\[
\encode_x(\alpha) = \transfib{\code}{\alpha}{c_0}.
\]
We show that $\encode_{a_0}$ and $\decode_{a_0}$ are quasi-inverses.
The composition $\encode_{a_0} \circ \decode_{a_0}$ is immediate by
assumption~\ref{item:ed3}.  For the other composition, we show
\[
\prd{x:A}{p : \id{a_0}{x}} \id{\decode_{x} (\encode_{x} p)}{p}.
\]
By path induction, it suffices to show
$\id{{\decode_{{a_0}} (\encode_{{a_o}} \refl{})}}{\refl{}}$.
After reducing the $\mathsf{transport}$, it suffices to show
$\id{{\decode_{{a_0}} (c_0)}}{\refl{}}$, which is assumption~\ref{item:ed4}.
\end{proof}

If a fiberwise equivalence between $(\id{a_0}{\blank})$ and $\code$ is desired,
it suffices to strengthen condition (iii) to
\[
\prd{x:A}{c : \code(x)} \id{\encode_{x}(\decode_{x}(c))}{c}.a
\]
However, to calculate a loop space (e.g. $\Omega(\Sn ^1)$), this
stronger assumption is not necessary.

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

\begin{lem}[Encode-decode for Truncations of Loop Spaces]
Assume a pointed type $(A,a_0)$ and a fibration
$\code : A \to \type$, where for every $x$, $\code(x)$ is a $k$-type.
Define
\[
\encode : \prd{x:A} \trunc{k}{\id{a_0}{x}} \to \code(x).
\]
by truncation recursion (using the fact
that $\code(x)$ is a $k$-type), mapping $\alpha : \id{a_0}{x}$ to
\transfib{\code}{\alpha}{c_0}. Suppose:
\begin{enumerate}
\item $c_0 : \code(a_0)$,
\item $\decode : \prd{x:A} \code(x) \to \trunc{k}{\id{a_0}{x}}$,
\item \label{item:decode-encode-loop-iii}
  $\id{\encode_{a_0}(\decode_{a0}(c))}{c}$ for all $c : \code(a_0)$, and
\item \label{item:decode-encode-loop-iv}
  $\id{\decode(c_0)}{\tproj{}{\refl{}}}$.
\end{enumerate}
Then $\trunc{k}{\id{a_0}{a_0}}$ is equivalent to $\code(a_0)$.
\end{lem}

\begin{proof}
That $\decode \circ \encode$ is identity is immediate by \ref{item:decode-encode-loop-iii}.
%
To prove $\encode \circ \decode$, we first do a truncation induction, by
which it suffices to show
\[
\prd{x:A}{p : \id{a_0}{x}} \id{\decode_{x}(\encode_{x}(\tproj{k}{p}))}{\tproj{k}{p}}.
\]
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 \encode, use assumption~\ref{item:decode-encode-loop-iv}.
\end{proof}

\section{Additional Results}
\label{sec:moreresults}

Though we do not present the proofs in this chapter, following results have also been established in homotopy type theory.

\begin{thm}
\index{homotopy!group!of sphere}
There exists a $k$ such that for all $n \ge 3$, $\pi_{n+1}(\Sn ^n) =
\Z_k$.
\end{thm}

\begin{proof}[Notes on the proof.]
The proof consists of a calculation of $\pi_4(\Sn ^3)$, together with an
appeal to stability (\cref{cor:stability-spheres}).  In the classical
statement of this result, $k$ is $2$.  While we have not yet checked that
$k$ is in fact $2$, our calcluation of $\pi_4(\Sn ^3)$ is constructive,\index{mathematics!constructive}
like all the rest of the proofs in this chapter.
(More precisely, it doesn't use any additional axioms such as \LEM{} or \choice{}, making it as constructive as
univalence and higher inductive types are.)  Thus, given a
computational interpretation of homotopy type theory, we could run the
proof on a computer to verify that $k$ is $2$.  This example is quite
intriguing, because it is the first calculation of a homotopy group
for which we have not needed to know the answer in advance.
\end{proof}

% Recall from \cref{sec:colimits} that $X \sqcup^C Y$ denotes the
% (homotopy) pushout of $X$ and $Y$ along $C$.
\index{pushout}%

\begin{thm}[Blakers--Massey theorem]\label{Blakers-Massey}
  \indexdef{theorem!Blakers--Massey}%
  \indexsee{Blakers--Massey theorem}{theorem, Blakers--Massey}%
  Suppose we are given maps $f : C  \rightarrow X$, and $g : C \rightarrow Y$. Taking first the pushout $X \sqcup^C Y $ of $f$ and $g$ and then the pullback of its inclusions $\inl : X \rightarrow X \sqcup^C Y \leftarrow Y : \inr$, we have an induced map $C \to X \times_{(X \sqcup^C Y)} Y$.

  If $f$ is $i$-connected and $g$ is $j$-connected, then this induced map is $(i+j)$-connected. In other words, for any points $x:X$, $y:Y$, the corresponding fiber $C_{x,y}$ of $(f,g) : C \to X \times Y $ gives an approximation to the path space $\id[X \sqcup^C Y]{\inl(x)}{\inr(y)}$ in the pushout.
\end{thm}

It should be noted that in classical algebraic topology, the Blakers--Massey theorem is often stated in a somewhat different form, where the maps $f$ and $g$ are replaced by inclusions of subcomplexes of CW complexes, and the homotopy pushout and homotopy pullback by a union and intersection, respectively.
In order to express the theorem in homotopy type theory, we have to replace notions of this sort with ones that are homotopy-invariant.
We have seen another example of this in the van Kampen theorem (\cref{sec:van-kampen}), where we had to replace a union of open subsets by a homotopy pushout.

\begin{thm}[Eilenberg--Mac Lane Spaces]\label{Eilenberg-Mac-Lane-Spaces}
\index{Eilenberg--Mac Lane space}
For any abelian\index{group!abelian} group $G$ and positive integer $n$, there is an $n$-type
$K(G,n)$ such that $\pi_n(K(G,n)) = G$, and  $\pi_k(K(G,n)) = 0$
for $k\neq n$.
\end{thm}

\begin{thm}[Covering spaces]\label{thm:covering-spaces}
  \index{covering space}%
  For a connected space $A$, there is an equivalence between covering spaces over $A$ and sets with an action of $\pi_1(A)$.
\end{thm}


\sectionNotes

%% For the spheres,  two
%% different definitions of the $n$-sphere $\Sn ^n$ have been used: the first as the
%% suspension of $\Sn ^ {n-1}$ (\cref{sec:suspension}), and the second
%% as a higher inductive type with one base point and one loop in
%% $\Omega^n$ (\cref{sec:circle}); we list the status for both
%% definitions.  The equivalence of the two can be deduced from the remarks
%% at the end of \cref{sec:suspension}.

{
\newcommand{\humancheck}{\ding{52}}
\newcommand{\computercheck}{\ding{52}\kern-0.5em\ding{52}}
\begin{table}[htb]
  \centering
\begin{tabular}{lcc}
\toprule
Theorem         & Status \\
\midrule
$\pi_1(\Sn ^1)$                     & \computercheck \\
$\pi_{k<n}(\Sn ^n)$                  & \computercheck \\
%% $\pi_{k<n}(\Sn ^n)$ --- suspension  & \computercheck \\
%% $\pi_2(\Sn ^2)$ --- suspension      & \computercheck \\
long-exact-sequence of homotopy groups & \computercheck    \\
total space of Hopf fibration is $\Sn ^3$ & \humancheck    \\
$\pi_2(\Sn ^2)$                     & \computercheck \\
$\pi_3(\Sn ^2)$                     & \humancheck    \\
$\pi_n(\Sn ^n)$                     & \computercheck \\
%% $\pi_n(\Sn ^n)$ --- suspension      & \computercheck \\
$\pi_4(\Sn ^3)$                     & \humancheck    \\
Freudenthal suspension theorem      & \computercheck \\
Blakers--Massey theorem              & \computercheck \\
Eilenberg--Mac Lane spaces $K(G,n)$ & \computercheck \\
van Kampen theorem                & \computercheck \\
covering spaces                     & \computercheck \\
Whitehead's principle for $n$-types & \computercheck \\
\bottomrule
\end{tabular}
\caption{Theorems from homotopy theory proved by
  hand (\humancheck) and by computer (\computercheck).}
  \label{tab:theorems}
\end{table}
}

The theorems described in this chapter are standard results in classical
homotopy theory; many are described by \cite{hatcher02topology}.  In these
notes, we review the development of the new synthetic proofs of them in homotopy
type theory.  \cref{tab:theorems} lists the homotopy-theoretic
theorems that have been proven in homotopy type theory, and whether they
have been computer-checked.
Almost all of these results were developed during the spring term at IAS
in 2013, as part of a significant collaborative effort.  Many people
contributed to these results, for example by being the principal author
of a proof, by suggesting problems to work on, by participating in many
discussions and seminars about these problems, or by giving feedback on
results.  The following people were the principal authors of the first
homotopy type theory proofs of the above theorems. Unless indicated otherwise, for the
theorems that have been computer-checked, the principal authors were
also the first ones to formalize\index{mathematics!formalized} the proof using a computer proof
assistant.
\begin{itemize}
\item
Shulman gave the homotopy-theoretic calculation of $\pi_1(\Sn^1)$.  Licata later discovered the
encode-decode proof and the encode-decode method.

\item
Brunerie calculated $\pi_{k<n}(\Sn ^ n)$.
Licata later gave an encode-decode version.

\item Voevodsky constructed the long exact sequence of homotopy groups.

\item Lumsdaine constructed the Hopf fibration.
  Brunerie proved that its total space is $\Sn ^3$, thereby calculating $\pi_2(\Sn ^2)$ and
  $\pi_3(\Sn ^3)$.

\item Licata and Brunerie gave a direct calculation of
$\pi_n(\Sn ^n)$.

\item
  Lumsdaine proved the Freudenthal suspension theorem; Licata and
  Lumsdaine formalized this proof.
\item Lumsdaine, Finster, and Licata proved the Blakers--Massey theorem;
  Lumsdaine, Brunerie, Licata, and Hou formalized it.

\item
Licata gave an encode-decode calculation of $\pi_2(\Sn ^2)$, and a
calculation of $\pi_n(\Sn ^n)$ using the Freudenthal suspension theorem; using similar
techniques, he constructed $K(G,n)$.

\item
Shulman proved the van Kampen theorem; Hou formalized this proof.

\item
Licata proved Whitehead's theorem for $n$-types.

\item Brunerie calculated $\pi_4(\Sn ^3)$.

\item
Hou established the theory of covering spaces and formalized it.
\end{itemize}

The interplay between homotopy theory and type theory was crucial to the
development of these results.  For example, the first proof that
$\pi_1(\Sn ^1)=\mathbb{Z}$ was the one given in \cref{subsec:pi1s1-homotopy-theory}, which follows a classical homotopy theoretic one.  A
type-theoretic analysis of this proof resulted in the development of the
encode-decode method.  The first calculation of $\pi_2(\Sn ^2)$ also followed
classical methods, but this led quickly to an encode-decode proof of the
result.  The encode-decode calculation generalized to $\pi_n(\Sn ^n)$, which
in turn led to the proof of the Freudenthal suspension theorem, by
combining an encode-decode argument with classical homotopy-theoretic
reasoning about connectedness, which in turn led to the Blakers--Massey
theorem and Eilenberg--Mac Lane spaces.  The rapid development of this
series of results illustrates the promise of our new understanding of
the connections between these two subjects.

\sectionExercises

\begin{ex}\label{ex:homotopy-groups-resp-prod}
  Prove that homotopy groups respect products: $\eqv{\pi_n(A\times B)}{\pi_n(A)\times \pi_n(B)}$.
\end{ex}

\begin{ex}\label{ex:decidable-equality-susp}
  \index{decidable!equality}%
  Prove that if $A$ is a set with decidable equality (see \cref{defn:decidable-equality}), then its suspension $\susp A$ is a 1-type.
  (It is an open question\index{open!problem} whether this is provable without the assumption of decidable equality.)
\end{ex}

\begin{ex}\label{ex:contr-infinity-sphere-colim}
  Define $\Sn^\infty$ to be the colimit of the sequence $\Sn^0 \to \Sn^1 \to \Sn^2 \to\cdots$.
  Prove that $\Sn^\infty$ is contractible.
\end{ex}

\begin{ex}\label{ex:contr-infinity-sphere-susp}
  Define $\Sn^\infty$ to be the higher inductive type generated by
  \begin{itemize}
  \item Two points $\north:\Sn^\infty$ and $\south:\Sn^\infty$, and
  \item For each $x:\Sn^\infty$, a path $\merid(x):\north=\south$.
  \end{itemize}
  In other words, $\Sn^\infty$ is its own suspension.
  Prove that $\Sn^\infty$ is contractible.
\end{ex}

\begin{ex}\label{ex:unique-fiber}
  Suppose $f:X\to Y$ is a function and $Y$ is connected.
  Show that for any $y_1,y_2:Y$ we have $\brck{\eqv{\hfib f {y_1}}{\hfib f {y_2}}}$.
\end{ex}

\begin{ex}\label{ex:ap-path-inversion}
  For any pointed type $A$, let $i_A : \Omega A \to \Omega A$ denote inversion of loops, $i_A \defeq \lam{p} \rev{p}$.
  Show that $i_{\Omega A} : \Omega^2 A \to \Omega^2 A$ is equal to $\Omega(i_A)$.
\end{ex}

\begin{ex}\label{ex:pointed-equivalences}
  Define a \textbf{pointed equivalence} to be a pointed map whose underlying function is an equivalence.
  \begin{enumerate}
  \item Show that the type of pointed equivalences between pointed types $(X,x_0)$ and $(Y,y_0)$ is equivalent to $\id[\pointed\type]{(X,x_0)}{(Y,y_0)}$.
  \item Reformulate the notion of pointed equivalence in terms of a pointed quasi-inverse and pointed homotopies, in one of the coherent styles from \cref{cha:equivalences}.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:HopfJr}
  Following the example of the Hopf fibration in \cref{sec:hopf}, define the \define{junior Hopf fibration}
  \indexdef{Hopf!fibration!junior}%
as a fibration (that is, a type family) over $\Sn ^1$ whose fiber over the basepoint is $\Sn ^0$ and whose total space is $\Sn ^1$.  This is also called the ``twisted double cover'' of the circle $\Sn ^1$.
\end{ex}

\begin{ex}\label{ex:SuperHopf}
Again following the example of the Hopf fibration in \cref{sec:hopf}, define an analogous fibration over $\Sn ^4$ whose fiber over the basepoint is $\Sn ^3$ and whose total space is $\Sn ^7$.  This is an open problem\index{open!problem} in homotopy type theory (such a fibration is known to exist in classical homotopy theory).
\end{ex}

\begin{ex}\label{ex:vksusppt}
  Continuing from \cref{eg:suspension}, prove that if $A$ has a point $a:A$, then we can identify $\pi_1(\susp A)$ with the group presented by $\trunc0A$ as generators with the relation $\tproj0a = e$.
  Then show that if we assume excluded middle, this is also the free group on $\trunc0 A \setminus \{\tproj0 a \}$.
\end{ex}

\begin{ex}\label{ex:vksuspnopt}
  Again continuing from \cref{eg:suspension}, but this time without assuming $A$ to be pointed, show that we can identify $\pi_1(\susp A)$ with the group presented by generators $\trunc0A \times \trunc0A$ and relations
  \begin{equation*}
    (a,b) = \opp{(b,a)},
    \qquad
    (a,c) = (a,b)\cdot (b,c),
    \qquad\text{and}\qquad
    (a,a) = e.
  \end{equation*}
\end{ex}

\index{acceptance|)}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "hott-online"
%%% End: