≃$\simeq$ ≅$\cong$ ∈$\in$ ⁻- ᴹM ᴺN ≡$\equiv$ λ$\lambda$ ⊎$\uplus$ ∷$::$
ℓ$\ell$ ᵢi ⟨$\langle$ ⟩$\rangle$ α$\alpha$ β$\beta$ θ$\theta$ φ$\varphi$
ψ$\psi$ η$\eta$ ε$\varepsilon$ ι$\iota$ Σ$\Sigma$ σ$\sigma$ ∀$\forall$
ℕ$\mathbb{N}$ →$\to$ ⊎$\uplus$ ⋆$*$ ¬$\lnot$ Θ$\theta$ ᴸ← ᴿ→ ∧$\wedge$ ∨$\vee$
∼$\sim$ ≢$\nequiv$ Π$\Pi$ ℤ$\mathbb{Z}$ ∥$\parallel$ ∣$\mid$ ℚ$\mathbb{Q}$ ₊+
∗$\ast$ ₁1 ₂2 ⊥$\bot$ ∘$\circ$ ρ$\rho$ ↦$\mapsto$ ₀0 ∙$\boldsymbol{\cdot}$
Ω$\Omega$ §$\mathbb{S}$ 𝟙$\mathbb{1}$ ×$\times$ ♥Susp ₋${}_{-}\\!$
✪$\sigma\\!$ ♢$\sphere{2}$ ⋆* ®${}^{\text{\color[rgb]{0,0,0}{$3$}}}$ ℏ,
⌣$\smile$ ⋈* ▬2 𝕒$A$ 𝕓$B$ 𝕔$\star_{A}$ 𝕕$\star_{B}$ ∇$\nabla$ ⊓$A$ 𝕝$B$
𝕗$i^{\vee}$ 𝟙$\mathbbm{1}$ ⊗$\mathbb{S}^{{\color[rgb]{0,0,0}2}}$
⊕$\mathbb{S}^{{\color[rgb]{0,0,0}3}}$ ₃3 □$\mathsf{\square}$
α${\mathbb{T}^{2}}$ β${\mathbb{K}^{2}}$ γ${\mathbb{R}P^{2}}$ ◃ ▹ ◁Susp △ Susp
ℜinr 𝕃inl ⋁$\vee$ ✶$\star$ ₕh ϕ$\phi$ ζ3

# Formalizing $\pi_{4}(\mathbb{S}^{3})\cong\mathbb{Z}/2\mathbb{Z}$ and
Computing a Brunerie Number in Cubical Agda

Axel Ljungström and Anders Mörtberg  Department of Mathematics
Stockholm University
Email<EMAIL_ADDRESS>and<EMAIL_ADDRESS>
###### Abstract

Brunerie’s 2016 PhD thesis contains the first synthetic proof in Homotopy Type
Theory (HoTT) of the classical result that the fourth homotopy group of the
3-sphere is $\mathbb{Z}/2\mathbb{Z}$. The proof is one of the most impressive
pieces of synthetic homotopy theory to date and uses a lot of advanced
classical algebraic topology rephrased synthetically. Furthermore, the proof
is fully constructive and the main result can be reduced to the question of
whether a particular “Brunerie number” $\beta$ can be normalized to $\pm 2$.
The question of whether Brunerie’s proof could be formalized in a proof
assistant, either by computing this number or by formalizing the pen-and-paper
proof, has since remained open. In this paper, we present a complete
formalization in
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>We do this by modifying Brunerie’s proof so that a key technical result, whose
proof Brunerie only sketched in his thesis, can be avoided. We also present a
formalization of a new and much simpler proof that $\beta$ is $\pm 2$. This
formalization provides us with a sequence of simpler Brunerie numbers, one of
which normalizes very quickly to $-2$ in
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>resulting in a fully formalized computer-assisted proof that
$\pi_{4}(\mathbb{S}^{3})\cong\mathbb{Z}/2\mathbb{Z}$.

††publicationid: pubid: 979-8-3503-3587-3/23/$31.00 ©2023 IEEE

##  I Introduction

Homotopy theory originated in algebraic topology, but is by now a central tool
in many branches of modern mathematics, such as algebraic geometry and
category theory. One of the central notions in homotopy theory is that of the
_homotopy groups_ of a space $X$, denoted $\pi_{n}(X)$. These groups
constitute a topological invariant, making them a powerful tool for
establishing if two given spaces are homotopy equivalent. The first two such
groups of a space are easy to understand: $\pi_{0}(X)$ characterizes the
connected components of $X$ and $\pi_{1}(X)$ is the fundamental group, i.e.
the group of equivalence classes of loops in $X$ up to homotopy. This idea
generalizes to higher values of $n$, for which $\pi_{n}(X)$ consists of
$n$-dimensional loops up to homotopy. For many spaces, these groups are
increasingly esoteric and difficult to compute for large $n$. This is true
also for seemingly tame spaces like spheres where $\pi_{n}(\mathbb{S}^{m})$ in
general is highly irregular when $n>m\geq 2$.

This paper concerns the first computer formalization of the classical result
that $\pi_{4}(\mathbb{S}^{3})\cong\mathbb{Z}/2\mathbb{Z}$, a result which is
particularly interesting because it gives the whole first stable stem of
homotopy groups of spheres, i.e. $\pi_{n+1}(\mathbb{S}^{n})$ for $n\geq 3$.
The fact that $\pi_{4}(\mathbb{S}^{3})\cong\mathbb{Z}/2\mathbb{Z}$ was proved
already in the 1930’s by Pontryagin using cobordism theory, but we instead
follow the synthetic approach to homotopy theory developed in Homotopy Type
Theory (HoTT) and popularized by the HoTT Book [1]. In this new approach,
spaces up to homotopy are represented directly as higher inductive types
(HITs) and homotopy groups are computed using Voevodsky’s univalence axiom
[2]. This gives a logical approach suitable for computer formalization, where
the results are interpretable in any suitably structured $(\infty,1)$-topos
[3].

The basis for our formalization is the 2016 PhD thesis of Brunerie [4] which
contains the first synthetic proof in HoTT that
$\pi_{4}(\mathbb{S}^{3})\cong\mathbb{Z}/2\mathbb{Z}$. The proof is one of the
most impressive pieces of synthetic homotopy theory to date and uses advanced
machinery from classical algebraic topology developed synthetically, including
the symmetric monoidal structure of smash products, (integral) cohomology
rings, the Mayer-Vietoris and Gysin sequences, the Hopf invariant, Whitehead
products, etc. The formalization of Brunerie’s proof has since remained open,
primarily due to the highly technical nature of some of the details. In this
paper, we present such a formalization in
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>[5], a _cubical_ extension of
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>[6] with computational support for univalence and HITs.

In addition to being a very impressive proof in synthetic homotopy theory,
Brunerie’s proof is particularly interesting as it is fully constructive. The
proof consists of two parts, with the first one culminating at the end of
Chapter 3 with the definition of a number $\beta:\mathbb{Z}$ such that
$\pi_{4}(\mathbb{S}^{3})\cong\mathbb{Z}/\beta\mathbb{Z}$. Since then, this
$\beta$ has been commonly referred to as the _Brunerie number_. Brunerie
writes the following about it:

> _This result is quite remarkable in that even though it is a constructive
> proof, it is not at all obvious how to actually compute this [ $\beta$]. At
> the time of writing, we still haven’t managed to extract its value from its
> definition. [4, Page 85]_

In fact, [4, Appendix B] contains a complete and concise definition of $\beta$
as the image of $1$ under a sequence of $12$ maps:

${\mathbb{Z}}$${\Omega(\mathbb{S}^{1})}$${\Omega^{2}(\mathbb{S}^{2})}$${\Omega^{3}(\mathbb{S}^{3})}$${\Omega^{3}(\mathbb{S}^{1}*\mathbb{S}^{1})}$${\Omega^{3}(\mathbb{S}^{2})}$${\Omega^{3}(\mathbb{S}^{1}*\mathbb{S}^{1})}$${\Omega^{3}(\mathbb{S}^{3})}$${\Omega^{2}\|\mathbb{S}^{2}\|_{2}}$${\Omega\|\Omega(\mathbb{S}^{2})\|_{1}}$${\|\Omega^{2}(\mathbb{S}^{2})\|_{0}}$${\Omega(\mathbb{S}^{1})}$${\mathbb{Z}}$

By implementing this number in a proof assistant with computational support
for univalence and HITs, one should be able to normalize it using a computer
to establish that $\beta=\pm 2$ and hence that
$\pi_{4}(\mathbb{S}^{3})\cong\mathbb{Z}/2\mathbb{Z}$. In 2016, by the time
Brunerie was finishing his thesis, there were some experimental proof
assistants based on the cubical type theory of [7], but these were too slow to
perform such a complex computation. So, instead of relying on normalization,
Brunerie spends the second part of the thesis (Chapters 4–6) to prove, using a
lot of the advanced machinery mentioned above, that $|\beta|$ is
propositionally equal to $2$. However, if one were instead able to compute the
number automatically in a proof assistant, this equality would hold
definitionally—effectively reducing the complexity and length of the proof by
an order of magnitude.

The intriguing possibility of a computer-assisted formal proof made many
people interested and countless attempts to normalize it has been made using
increasingly powerful computers. However, to date, no one has succeeded and it
is still unclear if $\beta$ is normalizable in a reasonable amount of time. In
light of this, it is natural to wonder if it is possible to simplify it to be
able to compute it. For example, the original definition only involves 1-HITs,
as the status of higher HITs was still quite understudied at the time. With a
better understanding of higher HITs [8, 9, 10], one quickly sees that the
first $3$ maps can be combined into one sending $1$ to the 3-cell of
$\mathbb{S}^{3}$ defined as a 3-HIT instead of as an iterated suspension as in
[4]. Unfortunately, simple optimizations like this do not seem to be
sufficient and, after several unsuccessful attempts, we decided to formalize
the second half of Brunerie’s thesis instead. However, this is by no means
straightforward. The first issue appears already in Section 4.1 about smash
products. The main result, Proposition 4.1.2, says that the smash product is a
1-coherent symmetric monoidal product on pointed types. However, its proof is
just a sketch and Brunerie writes the following about it:

> _The following result is the main result of this section even though we
> essentially admit it.[4, Page 90]_

Unfortunately, this result is then used to construct integral cohomology
rings, $H^{*}(X)$, whose cup product, $\smile$, appears in the definition of
the so-called Hopf invariant which is crucially used to prove that $|\beta|$
is $2$. While one might be convinced that Brunerie’s informal proof sketch is
correct, it is not obvious how one convinces a proof assistant of this. A
complete formalization would either have to fill in the holes in the proof
sketch or find an alternative construction which avoids Proposition 4.1.2. In
fact, Brunerie tried very hard to fill these holes using
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>metaprogramming [11]. However, he never managed to typecheck his computer
generated proof of the pentagon identity. Hence, this approach also seems
infeasible with current proof assistant technology. Luckily, Brunerie,
Ljungström and Mörtberg [12] recently gave an alternative synthetic definition
of the cup product on $H^{*}(X)$ which completely avoids smash products. This
has allowed us to completely skip the problematic Chapter 4 and, in
particular, Proposition 4.1.2, while still following the proofs in Chapters 5
and 6. Having a strategy for a formal proof, we were then able to embark on
the ambitious project of formalizing Brunerie’s proof. Even though we do not
need smash products, there was still a lot left to formalize and our
formalization closely follows Brunerie’s proofs, except for various smaller
simplifications and adjustments which we discuss in the paper.

In addition to this, we have also formalized a new proof by Ljungström [13]
which completely circumvents Chapters 4–6. This major simplification builds on
manually calculating the image of the element $\eta:\pi_{3}(\mathbb{S}^{2})$,
corresponding to $\beta$ under the isomorphism
$\pi_{3}(\mathbb{S}^{2})\cong\mathbb{Z}$, by dividing this isomorphism into
several maps, tracing $\eta$ in each step. In particular, the new proof is
completely elementary and does not rely on advanced tools such as cohomology.
The elements that one obtains while tracing $\eta$ are all new “Brunerie
numbers” that should normalize to $\pm 2$. In fact, one of these normalizes to
$-2$ in
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>in just under $4$ seconds on a regular laptop at the time of writing. So,
despite still not being able to compute the original $\beta$, this work can be
seen as an alternative solution to Brunerie’s conjecture about obtaining a
computational proof that $\pi_{4}(\mathbb{S}^{3})\cong\mathbb{Z}/2\mathbb{Z}$
which relies on simplifying the Brunerie number until it becomes effectively
computable.

Outline. The paper closely follows the structure of Brunerie’s proof. In
Section II, we discuss key results from HoTT that we will need and their
formalization in
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>Section III, which roughly corresponds to Chapter 2 of Brunerie’s thesis,
contains some first results on homotopy groups of spheres—e.g. the computation
of $\pi_{n}(\mathbb{S}^{m})$ for $n\leq m$. We then give Brunerie’s definition
of $\beta$ and prove that
$\pi_{4}(\mathbb{S}^{3})\cong\mathbb{Z}/\beta\mathbb{Z}$, the formalization of
which involves the James construction and Whitehead products. The remainder of
the paper is then devoted to the formalization of the different proofs that
$\beta=\pm 2$. We first discuss the formalization of Chapters 4–6 of
Brunerie’s proof in Section V. This involves a lot of technical machinery like
cohomology, the Hopf invariant, etc. We then, in Section VI, turn our
attention to the new elementary proof that $\beta=\pm 2$ and the new Brunerie
number which quickly normalizes to $-2$ in
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>We conclude in Section VII with a discussion and comparison of the different
formal proofs, as well as some directions for future work.

Formalization. All results in the paper have been formalized in
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>and is part of the
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>library (https://github.com/agda/cubical/). The code in the paper is mainly
literal
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>code taken verbatim from the library, but we have taken some liberties when
typesetting, e.g. shortening notations and omitting some universe levels. A
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>summary file linking the formalization and paper can be found here. The
development typechecks with
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>\--safe flag, which ensures that there are no admitted goals or postulates.

##  II Homotopy type theory in
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>
In this section, we concisely summarize the key HoTT concepts needed for the
proofs and their formalization in
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>This roughly corresponds to [4, Chap. 1]. For a more in depth introduction see
[1], which also serves as a reference for the formal language “Book HoTT”. In
this paper, we mainly use cubical notations, but almost all of the results
hold with minor changes in Book HoTT where paths are represented using Martin-
Löf’s inductive Id-types [14] instead of cubical path types. In Section VII we
discuss in more detail which proofs crucially rely on cubical features.

All of the results presented in this section were already part of the
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>library before we began our formalization and, while useful as a resource for
our notations, experts on HoTT and
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>can safely skim this section.

###  II-A Elementary HoTT notions and
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>notations

We write $(x:A)\to B\,x$ for dependent function types and denote the identity
function by
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{id}}}_{A}:A\to
A$. We write $\Sigma_{x:A}(B\,x)$ for dependent pair types and
$\mathsf{fst}$/$\mathsf{snd}$ for its projections. We write Bool for the type
of booleans and $\mathbbm{1}$ for the unit/singleton type with a single point
$\mathsf{\star_{1}}$.

Cubically, paths correspond to functions out of the unit interval, just like
in traditional topology. In
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>there is a primitive interval (pre-)type I with endpoints $\mathsf{i0}$ and
$\mathsf{i1}$. A path of type
${x}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{y}$
between two points $x,y:A$ is a function
$p:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{I}}\to
A$ such that
$p\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{i0}$}}}=x$
and
$p\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{i1}$}}}=y$.
As an example, the constant path at $x$ is defined by:
[agda/latex/Section2.tex]refl Note that we use “$=$” for
definitional/judgmental equality and “ ≡ ” for
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>path-equality. This can be contrasted with [1] which uses the opposite
convention where “$=$” is propositional/typal equality. This type of
notational conventions is not the only difference between
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>and Book HoTT. Many proofs by path induction in Book HoTT can instead be
replaced by direct proofs involving cubical path types. For example, cong (ap
in Book HoTT), which applies a function to a path, can be proved as:
[agda/latex/Section2.tex]cong Two other interesting applications of cubical
path types are the direct proofs of function extensionality and its inverse
funExt⁻ which are both one-liners [5, Sect. 2.1]. Although the treatment of
paths in
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>differs somewhat from Book HoTT, we may still prove _path induction_ : for any
dependent type
$B:(y:A)\,(p:{x}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{y})\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{Type}}$,
all dependent functions
$f:(y:A)\,(p:{x}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{y})\to
B\,x\,p$ are uniquely determined by
$f\,x\,({\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{refl}}\,x)$.
In Book HoTT, this can be used, among other things, to define the notion of a
_dependent_ path, which formalizes the situation when two points $a:A$ and
$b:B$ are equal up to a path
$p:{A}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{B}$.
In
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>however, the type of dependent paths is primitive:
[agda/latex/Section2.tex]PathP In fact,
${{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{\\_}}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{\\_}$
is just the special case of PathP where the line of paths
$A:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{I}}\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{Type}}$
is constant.

Following [1], a _pointed type_ is a dependent pair $(A,\star_{A})$ consisting
of a type $A$ and a fixed basepoint $\star_{A}:A$. We often omit the basepoint
and simply write $A$ for the pointed type $(A,\star_{A})$. Given pointed types
$A$ and $B$, the type of _pointed functions_ $A\to_{\star}B$ consists of pairs
$(f,\star_{f})$ where $f:A\to B$ and
$\star_{f}:{f\,\star_{A}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{\star_{B}}$.
Again, we often simply write $f:A\to_{\star}B$ and take $\star_{f}$ implicit.

A defining feature of HoTT, as opposed to Martin-Löf type theory [15], is the
existence of _higher inductive types_ (HITs). This is a generalization of
inductive types where we are not only allowed to specify the generating points
of the type in question, but also identifications between these points (and
possibly identifications of these identifications, and so on). This is useful
for defining quotient types, but also for defining spaces when working in the
_types-as-spaces_ interpretation of HoTT [1, Table 1].
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>natively supports HITs and a type representing the circle can be defined as
follows: [agda/latex/background.tex]s1 This captures precisely the
representation of the circle as a cell complex with one $0$-cell
($\mathsf{base}$) and one $1$-cell ($\mathsf{loop}$). We always take
$\sphere{1}$ to be pointed by $\mathsf{base}$. A dependent function
$f:(x:\sphere{1})\textrightarrow B\,x$ is determined by a point
$b:B\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{base}$}}}$
and a loop
$\ell:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{PathP}}(\lambda
i\to
B({{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{loop}$}}}\,i))\,b\,b$.
In
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>this would be written using pattern matching, as in the left-most definition
below, which is introduced side-by-side with the way it would commonly be
written in informal HoTT (e.g. as in Brunerie’s thesis):
[agda/latex/Background.tex]s1-fun $\displaystyle
f({{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{base}$}}})=b$
$\displaystyle\mathsf{ap}_{f}({{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{loop}$}}})=\ell$

###  II-B More higher inductive types

Let us now introduce the remaining HITs used in [4]. These come equipped with
induction principles analogous to that of $\sphere{1}$. To define higher
spheres, we need suspensions: [agda/latex/background.tex]susp We always take
suspensions to be pointed by $\mathsf{north}$. We may now define the
$n$-sphere, for $n\geq 1$, by
$\sphere{n}=\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Susp}}${}^{n-1}$}{\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\mathbb{S}^{1}$}}}$
where Suspn-1 denotes $(n-1)$-fold suspension. We also define
$\sphere{-1}={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\bot$}}$
(the empty type) and
$\sphere{0}={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{\text{Bool}}}$.
We remark that we could equivalently have defined $\sphere{1}$ as the
suspension of $\sphere{0}$ as is done in [4]. Our reason for not doing so is
that certain functions using $\sphere{1}$ appear to compute better with the
${{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{base}$}}}/{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{loop}$}}}$
definition. Furthermore, this is the definition used in already existing code
in the
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>library.

We may also capture the (homotopy) pushout of a span
$B\xleftarrow{f}A\xrightarrow{g}C$ by the following HIT:
[agda/latex/background.tex]pushout We use pushouts to define the wedge sum of
two pointed types, denoted
${A\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\vee$}}\,B}$,
the join of two types, denoted
${A\,}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{\text{\textasteriskcentered}}}\,{B}$,
and the cofiber of a map $f:A\to B$, denoted
${\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{cofib}}}}\,{f}$:

$\mathbbm{1}$${B}$${{A\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\times$}}\,B}}$${B}$${A}$${B}$${A}$${{A\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\vee$}}\,B}}$${A}$${{{A}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{\text{\textasteriskcentered}}}{B}}}$$\mathbbm{1}$${{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{cofib}}}}\,{f}}$$\scriptstyle\mathsf{fst}$$\scriptstyle\mathsf{snd}$$\scriptstyle{f}$$\scriptstyle{\lrcorner}$$\scriptstyle{\lrcorner}$$\scriptstyle{\lrcorner}$

Two particularly important functions out of wedge sums are:
[agda/latex/background.tex]nabla [agda/latex/background.tex]totimes

###  II-C Truncation levels and $n$-truncations

An important concept in HoTT is that of Voevodsky’s _h-levels_ [16], which
gives rise to the notion of an _n-type_. Since types in HoTT are interpreted
as spaces (or rather, as homotopy types), they are not only determined by
their points but also by which higher paths they may contain. We say that a
type $A$ is an $n$-type if all $(n+1)$-dimensional structure of $A$ is
trivial. Formally, this is captured by an inductive definition. We say that
$A$ is a $(-2)$-type if it is contractible, i.e. consisting of a single point,
as captured by
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{isContr}}\,A=\Sigma_{a_{0}:A}((a:A)\to{a_{0}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{a})$.
We inductively say that $A$ is an $(n+1)$-type if for any $x,y:A$, the type
${x}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{y}$
is an $n$-type. We call $(-1)$-types _propositions_ and $0$-types _sets_.

We can turn any type $A$ into an $n$-type by $n$-_truncation_ , denoted
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,A\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{n}$.
We often use the direct definitions of $(-1)$\- and $0$-truncation in our
formalization, and similar constructions work for any fixed value of $n$, but
not when $n$ is arbitrary. For higher $n$ we rely on the hub-and-spoke
construction [1, Sect. 7.3]. One caveat with truncations is that a map $f:A\to
B$ does _not_ , in general, induce a map
$f:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,A\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{n}\to
B$. This is, however, the case when $B$ is an $n$-type. In particular, $f$
always induces a function
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,f\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{n}:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,A\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{n}\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,B\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{n}$.

###  II-D Univalence, loop spaces, and h-spaces

In order to introduce Voevodsky’s univalence principle [2], we need to define
the (homotopy) fiber of a function. Given a function $f:A\to B$ and a point
$b:B$, we define the fiber of $f$ over $b$ by
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{fib}}}\,{f}\,b=\Sigma_{x:A}{({f\,a}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{b}})$.
We say that $f:A\to B$ is an equivalence, written
$f:{A}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{B}$,
if
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{fib}}}\,{f}\,b$
is contractible for all $b:B$. In order to prove that a function $f:A\to B$ is
an equivalence, it suffices to provide an inverse $f^{-}:B\to A$ and two paths
${f\circ
f^{-}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{id}}}_{B}}$
and ${f^{-}\circ
f}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{id}}}_{A}}$.
If $f$ is also pointed, we write
$f:A\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\simeq_{\star}$}}\,B$.

Univalence states that the canonical map
${A}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{B}\to{A}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{B}$,
defined by path induction, is an equivalence. In particular, we get a map
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ua}}:{A}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{B}\to{A}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{B}$
promoting equivalences to paths. This provides us with a useful method for
transferring proofs between equivalent types.

Transferring proofs is, however, not the only use case of univalence in HoTT.
It can also be used to characterize _loop spaces_ of HITs. This is often done
using the _encode-decode method_ [1, Sect. 8.1.4], a type theoretic analogue
of proofs by contractibilty of total spaces of fibrations. In HoTT, we define
the loop space of a pointed type $A$, by
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{A}=({\star_{A}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{\star_{A}})$.
This is again pointed by
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{refl}}\,\star_{A}$,
so we may iterate this definition to get the $n$th loop space of $A$, denoted
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}^{n}\,{A}$.
Loop spaces belong to a particularly important class of types called h-spaces.
These consist of a pointed type $B$ equipped with a magma structure

$\displaystyle\mu:B\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\times$}}B\to
B$
$\displaystyle\mu_{l}:(b:B)\to{\mu(\star_{B},b)}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{b}$
$\displaystyle\mu_{r}:(b:B)\to{\mu(b,\star_{B})}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{b}$

satisfying
${\mu_{l}\,\star_{B}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{\mu_{r}\,\star_{B}}$.
Another particularly important h-space for our purposes is $\sphere{1}$, for
which we will use $+$ to denote its binary operation. $\sphere{1}$ also comes
equipped with a notion of inversion which we will denote by $-$. In fact,
$\sphere{1}$ is a commutative and associative h-space.

##  III First results on homotopy groups of spheres

In this section, we cover [4, Chap. 2], which introduces some elementary
results on the homotopy groups of spheres. All of these results can also be
found in [1]. Before even stating them, we need homotopy groups:

######  Definition 1 (Homotopy groups).

For $n:\mathbb{N}$, we define the $n$th _homotopy group_ of a pointed type $A$
by:

${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}(A)={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\sphere{n}\to_{\star}A\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{0}$

The name homotopy _group_ should be taken with a grain of salt: it, in
general, only has a group structure when $n\geq 1$ (abelian when $n\geq 2$).
The structure may be defined, much like in [17, Section 5], by considering the
equivalence
${(\sphere{n}\to_{\star}A)}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{(\sphere{n-1}\to_{\star}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{A})}$,
where the latter type has a multiplication given by pointwise path
composition. An alternative definition of
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}(A)$
is via loop spaces. There is an equivalence
$\omega_{n}:{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}^{n}\,{A}}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{(\sphere{n}\to_{\star}A)}$
and, hence, we could equivalently have defined
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}(A)$
by setting
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}(A)={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}^{n}\,{A}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{0}$.
This makes the group structure on
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}(A)$
more transparent: it is simply path composition. This is the definition used
in [1]. Brunerie uses both definitions and often passes between the two
without comment.

An elementary but crucial result for the computation of homotopy groups is the
existence of the _long exact sequence of homotopy groups_. Its proof is
usually phrased using the loop space definition of homotopy groups [1, Theorem
8.4.6]. For ease of notation, let us simply write
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{fib}}}\,{f}$
for the fiber of a pointed function $f:A\to_{\star}B$ over the basepoint of
$B$.

######  Proposition 2 (LES of homotopy groups).

For any pointed map $f:A\to_{\star}B$, there is a long exact sequence

${\dots}$${{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n+1}(B)}}$
${{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}(\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{fib}}}\,{f})}}$${{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}(A)}}$${{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}(B)}}$
${{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n-1}(\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{fib}}}\,{f})}}$${\dots}$

Above, we have implicitly taken the kernel and image of a group homomorphism
$\phi:G\to H$ to be defined by

$\displaystyle{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ker}}\,\phi\,$
$\displaystyle={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{fib}}\,\phi\,0_{H}$
$\displaystyle{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{im}}\,\phi$
$\displaystyle=\Sigma_{h:H}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\Sigma_{g:G}(\phi(g)\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\equiv$}}\,h)\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{-1}$

When analyzing loop spaces and homotopy groups of suspensions, the following
function is of great importance. It will be used in many constructions to
come.

######  Definition 3 (The suspension map).

Given a pointed type $A$, there is a canonical map
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\sigma$}}:A\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{(}\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Susp}}{$\,A$}})$
given by

${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\sigma$}}\,x={{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{merid}$}}}\;{x}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cdot$}}\,{({{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{merid}$}}}\;{\star_{A}})}^{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$-1$}}}$

This induces a homomorphism on homotopy groups by post-composition:

${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}(A)\xrightarrow{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\sigma$}}_{*}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}({\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{(\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Susp}}{$\,A$}})})\xrightarrow{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n+1}(\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Susp}}{$\,A$}})$

We will often, with some abuse of notation, simply write
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\sigma$}}_{*}$
for this composition. We also define
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\sigma$}}_{n}:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,A\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{n}\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{({\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Susp}}{$\,A$}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{n+1})}$
by

${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\sigma$}}_{n}{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,x\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{cong}}\;{{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{\\!\\_\\!}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}}\;{({\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\sigma$}}\,x)}$

We will soon see the suspension map in action, but first we need the following
elementary result.

######  Proposition 4 (Join of spheres).

${{\sphere{n}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{\text{\textasteriskcentered}}}\,{\,\sphere{m}}}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{\sphere{n+m+1}}$.

###### Proof:

The statement is easily proved by induction, using
${\sphere{n+1}}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Susp}}{$\,\sphere{n}$}}}$
and
${{(\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Susp}}{$\,A$}})\,}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{\text{\textasteriskcentered}}}\,{B}}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Susp}}{$\,({A\,}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{\text{\textasteriskcentered}}}\,{B})$}}}$.
∎

In particular, Proposition 4 gives us an equivalence
${{\sphere{1}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{\text{\textasteriskcentered}}}\,{\sphere{1}}}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{\sphere{3}}$.
Using this fact, we define the following map, which will play a crucial role
in the analysis of
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{4}(\sphere{3})$.

######  Definition 5 (Hopf map).

We define
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{hopf}}}:\sphere{3}\to\sphere{2}$
by the composition
$\sphere{3}\xrightarrow{\sim}{\sphere{1}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{\text{\textasteriskcentered}}}\,{\sphere{1}}\xrightarrow{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{h}}}}\sphere{2}$
where h is given by  [agda/latex/BruneriesProof.tex]hopf where y - x is
defined using the h-space and inversion structure on $\sphere{1}$.

It turns out that the following is true.

######  Proposition 6 ([1, Theorem 8.5.1]).

The fiber of hopf is equivalent to $\sphere{1}$, i.e.
${\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{fib}}}\,{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{hopf}}}}}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{\sphere{1}}$.

This gives us a fibration sequence $\sphere{1}\to\sphere{3}\to\sphere{2}$
which, in particular, will allow us to connect homotopy groups of $\sphere{2}$
with those of $\sphere{3}$ and $\sphere{1}$. For this, we need to introduce
the notion of _connectedness_. We say that a type $A$ is $n$-connected if
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,A\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{n}$
is contractible. Similarly, we say that a function $f:A\to B$ is $n$-connected
if all of its fibers are $n$-connected. This means, in particular, that the
induced function
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,f\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{n}:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,A\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{n}\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,B\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{n}$
is an equivalence. The following is an immediate consequence of the definition
of $n$-truncations.

######  Lemma 7 (Connectedness of spheres).

For $n\geq-1$, $\sphere{n}$ is $(n-1)$-connected.

Using Lemma 7, we can easily prove the following:

######  Proposition 8 ([4, Prop. 2.4.1]).

For $n<m$, the group
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}(\sphere{m})$
is trivial.

For the sake of completeness, let us take the liberty of mentioning some
results from [4, Chap. 3] already here, since they also concern low-
dimensional homotopy groups of spheres. A crucial result is [1, Theorem
8.6.4]:

######  Theorem 9 (Freudenthal suspension theorem).

Given an $n$-connected and pointed type $A$, the map
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\sigma$}}:A\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{(}\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Susp}}{$\,A$}})$
is $2n$-connected.

On can easily deduce from Theorem 9 that, in particular,
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\sigma$}}_{n}:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,A\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{n}\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{(}\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Susp}}{$\,A$}})\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{n}$
is an equivalence. This allows us to prove the following result:

######  Corollary 10.

For $n\geq 1$, we have
${{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}(\sphere{n})}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}}$.
Furthermore,
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}(\sphere{n})$
is generated by
$i_{n}={{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{id}}}_{\sphere{n}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}$.

###### Proof:

The synthetic proof of the classical result that
${{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{1}(\sphere{1})}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}}$
is due to Licata and Shulman [18]. The fact that
${{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{2}(\sphere{2})}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{1}(\sphere{1})}$
is given by the LES associated to the Hopf fibration combined with Proposition
8. The fact that
${{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n+1}(\sphere{n+1})}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}(\sphere{n})}$
is an immediate consequence of Theorem 9. The second statement follows by
induction on $n$. ∎

We have now analyzed all homotopy groups
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}(\sphere{m})$
with $n\leq m$. This yields the following:

######  Proposition 11.

Post-composition by hopf induces an isomorphism
${{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{3})}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{2})}$.

###### Proof:

By Propositions 2 and 6, we get an exact sequence

${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{1})\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{3})\xrightarrow{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{hopf}}}_{*}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{2})\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{2}(\sphere{1})$

as
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}(\sphere{1})$
vanishes for $n>1$,
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{hopf}}}_{*}$
is an isomorphism. ∎

######  Corollary 12.

There is an isomorphism
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\psi$}}:{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{2})}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}}$.
Furthermore,
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{2})$
is generated by hopf.

###### Proof:

By Corollary 10 we know that
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{3})$
is generated by the identity function on $\sphere{3}$. We know that the
isomorphism
${{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{3})}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{2})}$
is given by post-composition by hopf and thus the generator of
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{3})$
is mapped to hopf. ∎

###  III-A Formalization of Brunerie’s Chapter 2

Most of these results have already been added to
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>by Mörtberg & Pujet [19], Ljungström [20], and Brunerie, Ljungström & Mörtberg
[12]. The Freudenthal suspension theorem was formalized in
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>by Cavallo [21], using a direct cubical proof following [1, Thm. 8.6.4].
Corollary 10 was given a direct proof, following the computation of cohomology
groups of spheres in [12].

There were some technical difficulties related to the equivalence
$\omega_{n}:{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}^{n}\,{A}}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{(\sphere{n}\to_{\star}A)}$,
which is used to show that the two different definitions of homotopy groups
are equivalent. In several proofs, it is more natural to work on the left-
hand-side of $\omega_{n}$. At the same time, working on the right-hand-side
often makes constructing elements easier (compare, for instance, an explicit
description of the generator of
$i_{3}:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{3})$
described as a $3$-loop in $\sphere{3}$ to the very compact definition
$i_{3}={{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{id}}}_{\sphere{3}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}$).
This means that we often have to translate between the two definitions. One
particularly important example is the LES of homotopy groups associated to a
function $A\to_{\star}B$. On each level, the maps are given as follows:

$\displaystyle{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}^{n}\,{(\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{fib}}}\,{f})}\xrightarrow{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}^{n}\,{\mathsf{fst}}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}^{n}\,{A}\xrightarrow{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}^{n}\,{f}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}^{n}\,{B}$

This is then transported to the definition of homotopy groups as maps from
spheres via $\omega_{n}$. For the proof of e.g. Corollary 12, we need to know
that the maps in the sequence are given as follows:

$\displaystyle{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}{(\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{fib}}}\,{f})}\xrightarrow{{{\color[rgb]{0.93359375,0.0703125,0.5390625}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.0703125,0.5390625}\textsf{$\mathsf{fst}$}}}_{*}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}{(A)}\xrightarrow{f_{*}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{n}{(B)}$

What we need is then more than just an equivalence
$\omega_{n}:{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}^{n}\,{A}}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{(\sphere{n}\to_{\star}A)}$
– we need to show that this equivalence is functorial. This is implicitly
assumed in Brunerie’s thesis, but, in
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>we need to make it precise. Formalizing this fact is not entirely trivial.
First, we need a tractable definition of the equivalence in question. It can
be described inductively with base case
$\omega_{1}:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{A}\to(\sphere{1}\to_{\star}A)$
given by:

$\displaystyle\omega_{1}\,p\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{base}$}}}$
$\displaystyle=\star_{A}$
$\displaystyle\omega_{1}\,p\,({{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{loop}$}}}\,i)$
$\displaystyle=p\,i$

which we take to be pointed by refl. It is easy to verify that this is an
equivalence. We define $\omega_{n+1}$ by the composition:

$\displaystyle{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}^{n+1}\,{A}={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{({\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}^{n}\,{A})}$
$\displaystyle\xrightarrow{~{}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{\omega_{n}}~{}~{}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{(\sphere{n}\to_{\star}A)}$
$\displaystyle\xrightarrow{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{funExt${}^{-}_{\star}$}}}(\sphere{n}\to_{\star}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{A})$
$\displaystyle\xrightarrow{~{}~{}~{}~{}~{}~{}~{}~{}}(\sphere{n+1}\to_{\star}A)$

where the last arrow comes from the adjunction
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{Susp}}\dashv{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{}$.
This is a composition of equivalences, and hence an equivalence. We then need
to verify that the following commutes

${{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}^{n}\,{A}}}$${{(\sphere{n}\to_{\star}A)}}$${{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}^{n}\,{B}}}$${{(\sphere{n}\to_{\star}B)}}$$\scriptstyle{\omega_{n}}$$\scriptstyle{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\scriptstyle\Omega$}}^{n}\,{\\!f}}$$\scriptstyle{\omega_{n}}$$\scriptstyle{f_{*}}$

This can be proved inductively. The base case is easy and the inductive step
is given by the following diagram

${{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{(}\sphere{n}\to_{\star}A)}}$${{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}^{n+1}\,{A}}}$${{(\sphere{n+1}\to_{\star}A)}}$${{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}^{n+1}\,{B}}}$${{(\sphere{n+1}\to_{\star}B)}}$${{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{(}\sphere{n}\to_{\star}B)}}$$\scriptstyle{\omega_{n+1}}$$\scriptstyle{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\scriptstyle\Omega$}}^{n+1}\,{f}}$$\scriptstyle{\omega_{n+1}}$$\scriptstyle{f_{*}}$
≃
$\scriptstyle{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\scriptstyle\Omega$}}\,{f_{*}}}$
≃
$\scriptstyle{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\scriptstyle\Omega$}}\,{\omega_{n}}}$$\scriptstyle{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\scriptstyle\Omega$}}\,{\omega_{n}}}$

where the commutativity of the outer square comes from the base case paired
with the inductive hypothesis, the triangles from the definition of
$\omega_{n+1}$ and the right-most square from a straightforward argument.

##  IV The Brunerie number

Here we give an overview of the first half of Brunerie’s proof. This
corresponds to [4, Chap. 3] and culminates in the isomorphism
${{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{4}(\sphere{3})}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}/{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\beta$}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}}$
for an at this point unknown “Brunerie number”
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\beta$}}:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}$.
We also discuss the formalization of this part of the proof and various
simplifications found during the formalization.

###  IV-A The James construction

To define $\beta$, Brunerie uses the _James construction_ [22], which he
introduced in HoTT and partially formalized in [23].

######  Proposition 13 (James construction).

Let $A$ be a pointed $(k\geq 0)$-connected type. There are types
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{n}{\,A}$
with inclusions

$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{0}{\,A}\lhook\joinrel\xrightarrow{j_{0}}\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{1}{\,A}\lhook\joinrel\xrightarrow{j_{1}}\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,A}\lhook\joinrel\xrightarrow{j_{2}}\cdots$

such that its sequential colimit
${\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{\infty}{\,A}}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{(\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Susp}}{$\,A$}})}}$.
Furthermore,
$j_{n}:\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{n}{\,A}\hookrightarrow\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{n+1}{\,A}$
is $(n(k+1)+(k-1))$-connected.

A consequence of Proposition 13 is the following fact

######  Proposition 14.

Given a $(k\geq 0)$-connected type $A$, there is a $(3k+1)$-connected map
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,A}\xrightarrow{}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{(\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Susp}}{$\,A$}})}$.

The proof of Proposition 14 uses that
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{\infty}{\,A}$,
the sequential colimit of the sequence in Proposition 13, can be shown to be
equivalent to
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{(\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Susp}}{$\,A$}})}$.
This, paired with some results on the connectivity of sequential colimits,
gives the statement.

######  Theorem 15.

${{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{4}(\sphere{3})}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,\sphere{2}})}$

###### Proof:

Because $\sphere{2}$ is $1$-connected, Proposition 14 tells us that there is a
$4$-connected map

$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,\sphere{2}}\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{(}\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Susp}}{$\,\sphere{2}$}})={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{(}\sphere{3})$

In particular, it is $3$-connected and induces an equivalence
${{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,\sphere{2}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{3}}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{\sphere{3}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{3}}$.
We get

${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{4}(\sphere{3})\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}({\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{\sphere{3}})\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,\sphere{2}})$

as desired. ∎

###  IV-B Formalization of the James construction

This is a particularly technical part of Brunerie’s thesis, primarily due to
the high number of higher coherences which need to be verified in the proof of
Proposition 13. While this has, subsequent to our efforts, been formalized in
its entirety by Kang [24], we have taken a shortcut by giving a direct proof
of Theorem 15, which means we do not in fact need the full James construction.
Consequently, we instead give direct definitions of
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{n}{\,A}$
for $n\leq 2$ for a pointed type $A$.

######  Definition 16 (Low dimensional James construction).

We define
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{0}{\,A}={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\mathbbm{1}$}}$
and
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{1}{\,A}=A$.
The type
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,A}$
is defined as the pushout of the span $A\times
A\xleftarrow{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$i^{\vee}$}}}A\vee
A\xrightarrow{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\nabla$}}}A$.

We remark that the construction in Definition 16 is not definitionally the
same as Brunerie’s; in his thesis, these constructions are theorems rather
than definitions. Here we take them as definitions. With
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{n}{\,A}$
defined this way, the map
$j_{0}:\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{0}{\,A}\to\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{1}{\,A}$
is just the constant pointed map and
$j_{1}:\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{1}{\,A}\to\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,A}$
is $\mathsf{inr}$.

Before we continue, let us temporarily redefine $\sphere{2}$ to be the
following equivalent HIT. This will make some of the following constructions
more compact. [agda/latex/background.tex]s2

The next lemma will be crucial. It is a special case of the _Wedge
Connectivity Lemma_ [1, Lemma 8.6.2], of which we have formalized a version of
the proof of the sphere case in [12, Lemma 8]. From the point of view of
formalization, this proof is easier to work with since it gives more useful
definitional equalities.

######  Lemma 17 (Wedge connectivity for $\sphere{2}$).

Let
$P:\sphere{2}\times\sphere{2}\to\textnormal{${2}$-{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Type}}}$.
Any function
$f:(x:\sphere{2}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\times$}}\sphere{2})\to
P\,x$ is induced by the following data:

$\displaystyle f_{l}$ $\displaystyle:(x:\sphere{2})\to
P(x\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{base}$}}})$
$\displaystyle f_{r}$ $\displaystyle:(y:\sphere{2})\to
P({{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{base}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,y)$
$\displaystyle f_{lr}$
$\displaystyle:{f_{l}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{base}$}}}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{f_{r}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{base}$}}}}$

Before we discuss the formalization of Theorem 15 stated with the low
dimensional James construction, we first construct a family of equivalences
$f_{x}:{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,\sphere{2}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{3}}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,\sphere{2}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{3}}$
over $x:\sphere{2}$. We do this by truncation elimination and pattern matching
on $x$, starting with the $\mathsf{base}$ case:

$\displaystyle
f_{{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{base}$}}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{inl}$}}}\,{(}x,y)\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}$
$\displaystyle={{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{inl}$}}}\,{(}x\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,y)\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}$
$\displaystyle
f_{{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{base}$}}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{inr}$}}}\,{z}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}$
$\displaystyle={{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{inl}$}}}\,{(}{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{base}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,z)\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}$

We omit the path constructors, which are all easy coherences which are omitted
due to space constraints. It is an easy lemma that
$f_{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{base}$}}}$
is equal to the identity on
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,\sphere{2}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{3}$.
To complete the definition of $f_{x}$, we need to consider the case when
$x={{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{surf}$}}}\,i\,j$.
This amounts to providing a dependent function:

$f_{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{surf}$}}}:(x:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,\sphere{2}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{3})\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}^{2}\,{({\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,\sphere{2}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{3}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,f_{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{base}$}}}\,x)}$

To do this, we will, in particular, need to provide a family of fillers
$Q_{(x\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,y)}:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{refl}}\,{{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{inl}$}}}\,{(}x\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,y)\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\equiv$}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{refl}}\,{{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{inl}$}}}\,{(}x\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,y)\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}}$.
This is a $1$-type, and thus Lemma 17 applies. We define:

$\displaystyle
Q_{({{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{base}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,y)}\,i\,j$
$\displaystyle={{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{inl}$}}}\,{(}{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{surf}$}}}\,i\,j\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,y)\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}$
$\displaystyle
Q_{(x\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{base}$}}})}\,i\,j$
$\displaystyle={{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{inl}$}}}\,{(}x\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{surf}$}}}\,i\,j)\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}$

The fact that these two constructions agree when both $x$ and $y$ are
$\mathsf{base}$ is a technical, but relatively straightforward lemma. Thereby,
$Q_{(x\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,y)}$
is defined. We may now define
$f_{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{surf}$}}}$:

$\displaystyle
f_{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{surf}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{inl}$}}}\,{(}x\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,y)\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}$
$\displaystyle=Q_{(x\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,y)}$
$\displaystyle
f_{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{surf}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{inr}$}}}\,{z}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}$
$\displaystyle=Q_{({{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{base}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,z)}$

The higher cases are easy due to the fact that the goal becomes $0$-truncated,
making it sufficient to define them for
${{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{base}$}}}:\sphere{2}$.
Thus, $f_{x}$ is defined for all $x:\sphere{2}$.

######  Lemma 18.

For $x:\sphere{2}$, $f_{x}$ is an automorphism on
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,\sphere{2}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{3}$.

This can be proved by explicitly constructing an inverse to $f_{x}$ which
makes later proofs easier. As the construction is completely analogous to that
of $f_{x}$ we have omitted it due to space constraints.

We are now ready to prove the following statement, which is a rephrasing of
Theorem 15.

######  Proposition 19.

${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\sphere{3}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{4}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\simeq$}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,\sphere{2}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{3}$

###### Proof:

We take
$\sphere{3}=\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Susp}}{$\,\sphere{2}$}}$,
where $\sphere{2}$ is defined using $\mathsf{base}$/$\mathsf{surf}$ as above.
We employ the encode-decode method and define
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{Code}}:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\sphere{3}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{4}\to\textsf{$3${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{-Type}}}$.
Since the universe of $3$-types is a $4$-type, we may do so by truncation
elimination, letting
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{Code}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{north}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{Code}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{south}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,\sphere{2}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{3}$
and
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{Code}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{merid}$}}}\;{x}\,i\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ua}}\,f_{x}\,i$.
We now need to define a family of functions
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{decode}}}_{x}:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{Code}}\,x\to{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{north}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\equiv$}}\,x$
over
$x:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\sphere{3}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{4}$.
The key step is defining
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{decode}}}_{{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{north}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}}:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,\sphere{2}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{3}\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\sphere{3}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{4}}$.
On point constructors, it is given by:

$\displaystyle\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{decode}}}_{{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{north}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}}\,({{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{inl}$}}}\,{(x\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,y)})$
$\displaystyle={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\sigma$}}\,x\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cdot$}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\sigma$}}\,y$
$\displaystyle\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{decode}}}_{{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{north}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}}\,({{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{inr}$}}}\,{z})$
$\displaystyle={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\sigma$}}\,z$

which is easily verified to be coherent with the higher constructors. At this
point, we may follow the usual encode-decode heuristic [1, Section 8.9] to
prove that
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{decode}}}_{{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{north}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{∣}$}}}}$
is an equivalence in a technical, but direct manner. ∎

We get Theorem 15 as an immediate corollary of Proposition 19 via the same
sequence of isomorphisms as in the proof of Theorem 15.

###  IV-C Definition of the Brunerie number

Brunerie’s goal is now to analyze
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,\sphere{2}})$.
The first result needed is the following:

######  Definition 20 (Whitehead map).

Given two pointed types $A$ and $B$, there is a map:
[agda/latex/background.tex]whitehead

For our purposes, we only need the case when $A=B=\sphere{1}$ (although all of
the following results appear in full generality in Brunerie’s thesis). We get
a composite map:

$\sphere{3}\xrightarrow{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\simeq$}}}{{\sphere{1}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{\text{\textasteriskcentered}}}\,{\sphere{1}}}\xrightarrow{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{W}}}\sphere{2}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\vee$}}\,\sphere{2}$

This induces, via pre-composition, a map

${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\sphere{2}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\vee$}}\,\sphere{2}\to_{\star}\sphere{2}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{0}\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{2})$

which via the obvious map

${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{2}(\sphere{2})\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\times$}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{2}(\sphere{2})\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\sphere{2}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\vee$}}\,\sphere{2}\to_{\star}\sphere{2}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{0}$

defines a _Whitehead product_ :

$[-,-]:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{2}(\sphere{2})\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\times$}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{2}(\sphere{2})\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{2})$

Recall that we denote by $i_{2}$ the generator of
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{2}(\sphere{2})$.
Brunerie shows, in particular, the following about its relation to the
Whitehead product.

######  Theorem 21.

The kernel of the suspension map
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\sigma$}}_{*}:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{2})\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{4}(\sphere{3})$
is generated by $[i_{2},i_{2}]$.

The key technical component in the proof is the _Blakers-Massey Theorem_ ,
first formalized in HoTT by Favonia, Finster, Licata & Lumsdaine in [25] and
later generalized by Anel, Biedermann, Finster & Joyal [26]:

######  Theorem 22 (Blakers-Massey).

Consider the diagram

${A}$${P}$${C}$${B}$${{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{{Pushout}}}\,f\,g}}$$\scriptstyle\mathsf{inl}$
$\scriptstyle\mathsf{inr}$
$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{f\sqcup
g}$$\scriptstyle{\lrcorner}$$\scriptstyle{\lrcorner}$

where $P$ is the pullback along $\mathsf{inl}$ and $\mathsf{inr}$, i.e.
$P=\Sigma_{(b,c):B\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\times$}}\,C}({{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{inl}$}}}\,{b}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{inr}$}}}\,{c}})$,
and $f\sqcup g$ is defined by

$(f\sqcup
g)\,a=(f\,a\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,g\,a\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{,}$}}}\,{{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{push}$}}}\,{a})$

If $f$ and $g$ are $n$\- respectively $m$-connected, then $f\sqcup g$ is
$(n+m)$-connected.

Theorem 21 is proved by considering the following diagram

${\sphere{3}}$${P}$${\sphere{2}}$$\mathbbm{1}$${{J_{2}\sphere{2}}}$$\scriptstyle{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\scriptstyle\nabla$}}\circ\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{W}}}$$\scriptstyle{\lrcorner}$$\scriptstyle{\lrcorner}$

Verifying that the outer square is a pushout square is technical and we omit
the proof here. Above, $P$ is simply the fiber of
${{\color[rgb]{0,0.546875,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.546875,0}\textsf{$\mathsf{inr}$}}}\,{}:\sphere{2}\to\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,\sphere{2}}$.
The leftmost map is $2$-connected since $\sphere{3}$ is $2$-connected and the
top map is $0$-connected since $\sphere{3}$ and $\sphere{2}$ are both
$1$-connected. Consequently, by Theorem 22, we get that the map $\sphere{3}\to
P$ is $2$-connected and thus induces a surjection after application of
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}$.
This gives the diagram:

${{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(P)}}$${{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{2})}}$${{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,\sphere{2}})}}$${{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{3})}}$${{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{4}(\sphere{3})}$$\scriptstyle\cong$$\scriptstyle{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\scriptstyle\sigma$}}_{*}}$

where the sequence on the top comes from the LES of homotopy groups associated
to $P$. The dashed map sends the generator
$i_{3}:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{3})$
to
$[i_{2},i_{2}]:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{2})$
by definition.

Theorem 21 motivates the following definition. Recall that we denote by $\psi$
the isomorphism
${{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{2})}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}}$.

######  Definition 23 (Brunerie number).

We define the Brunerie number
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\beta$}}:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}$
by
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\beta$}}={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\psi$}}\,[i_{2},i_{2}]$.

We may now state the main result of [4, Chap. 3].

######  Corollary 24.

${{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{4}(\sphere{3})}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}/{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\beta$}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}}$.

###### Proof:

The statement follows immediately from Theorem 21 and the fact that
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\sigma$}}_{*}:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{3}(\sphere{2})\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\pi$}}_{4}(\sphere{3})$
is surjective, which is a consequence of Theorem 9. ∎

###  IV-D Formalization of the Brunerie number

The formalization of this part was straightforward. Arguably the most
technical result, the Blakers-Massey theorem, was already available in the
library thanks to Kang [27]. Most of the remaining results were essentially
just diagram chases which, in a proof assistant, can be somewhat technical.
Most work went into verifying that
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{J}}}{}_{2}{\,\sphere{2}}$
is the cofiber of
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\nabla$}}\circ{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{W}}$,
the proof of which followed Brunerie’s closely.

In this section we found the only obvious mistake in Brunerie’s thesis on page
82. In his definition of the $\mathsf{push}$ -case for W, the path component
in the middle was not inverted, making the term ill-typed. Naturally, this was
of no mathematical significance and something Brunerie immediately would have
noticed if he would have attempted to provide a computer formalization of this
construction.

##  V Brunerie’s proof that
${\left|{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\beta$}}}\right|}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{2}$

This section concerns the final three Chapters (4–6) of Brunerie’s thesis. The
main goal here is proving that
${\left|{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\beta$}}}\right|}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{2}$.

We will not discuss Chapter 4 in much detail. Chapter 4 is devoted to smash
products and, in particular, their symmetric monoidal structure. Brunerie used
this in subsequent chapters to define and prove properties about the _cup
product_ , a graded multiplicative operation on cohomology groups which will
be used to show that
${\left|{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\beta$}}}\right|}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{2}$.
This chapter has turned out to be incredibly difficult to formalize due to the
large number of higher coherences involved in the proofs [11].

Luckily, it turns out that Chapter 4 can be avoided altogether and that this
in fact makes some difficult proofs later on very direct. For this reason, the
results in Chapter 4 were omitted completely from our formalization. The
reason for this is that all results regarding smash products in Brunerie’s
thesis concern, in some way, pointed maps out of smash products. In this case,
we may exploit the adjunction of maps out of smash products and bi-pointed
maps:

${(A\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∧}}\,B\to_{\star}C)}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{(A\to_{\star}(B\to_{\star}C))}$

Here, $B\to_{\star}C$ is taken to be pointed by the constant map. As shown in
[12], it is arguably easier to define the cup product on the right-hand side
of the adjunction, which effectively means that we never have to work with
smash products when formalizing cohomology theory.

###  V-A Cohomology and the Hopf invariant

[4, Chap. 5] introduces integral cohomology groups and rings, and gives a
construction of the Mayer-Vietoris sequence. In more detail, Brunerie defines
the integral Eilenberg-MacLane spaces by
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{K}}}_{0}={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}$
and
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{K}}}_{n}={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,\sphere{n}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{n}$
for $n\geq 1$. This allows for a definition of the (integral) cohomology of
$X$:

$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{n}\\!\left({X}\right)={\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}\,X\to\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{K}}}_{n}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{∥}}_{0}$

The fact that
${{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{K}}}_{n+1}}}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{K}}}_{n}}$
follows by a proof completely analogous to that of Corollary 10. Brunerie uses
this equivalence to carry over the (commutative) h-space structure on
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\Omega$}}\,{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{K}}}_{n+1}}$
to that of
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{K}}}_{n}$.
This provides a notion of addition
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{+${}_{k}$}}:\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{K}}}_{n}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\times$}}\,\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{K}}}_{n}\to\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{K}}}_{n}$
which lifts to
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{n}\\!\left({X}\right)$
by post-composition, thereby endowing
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{n}\\!\left({X}\right)$
with a group structure. Brunerie also defines a notion of multiplication
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\smile_{k}$}}:\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{K}}}_{n}\to\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{K}}}_{m}\to\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{K}}}_{n+m}$
which induces the graded-commutative multiplication
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\smile$}}:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{H}}^{n}(X)\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{H}}^{m}(X)\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{H}}^{n+m}(X)$
called the cup product. This construction is far less direct in Brunerie’s
thesis, and due to space constraints we cannot discuss it in more detail here.
For a more direct construction (which is also the one we have used in our
formalization), we refer to [12, Section 4.1].

The synthetic construction of the Mayer-Vietoris sequence concerns the long
exact sequence

${{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{0}\\!\left({D}\right)}}$${{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{0}\\!\left({B}\right)\times\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{0}\\!\left({C}\right)}}$${{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{0}\\!\left({A}\right)}}$
${{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{1}\\!\left({D}\right)}}$${\dots}$

where $D$ denotes the pushout of a span $B\xleftarrow{f}A\xrightarrow{g}C$. A
direct application gives us, for $n\geq 1$, that
${\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{n}\\!\left({\sphere{m}}\right)}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}}$
if $n=m$ and
${\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{n}\\!\left({\sphere{m}}\right)}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\mathbbm{1}$}}}$
otherwise. This gives, by another application of the sequence, the following
result:

######  Lemma 25.

For any $f:\sphere{3}\to\sphere{2}$ we have

$\displaystyle\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{n}\\!\left({{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{cofib}}}}\,{f}}\right)\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,\begin{cases}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}&n\in\\{0,2,4\\}\\\
{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\mathbbm{1}$}}&\text{otherwise}\end{cases}$

Let us briefly fix $f:\sphere{3}\to\sphere{2}$. Denote by $\gamma_{2}$ and
$\gamma_{4}$ the generators of
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{2}\\!\left({{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{cofib}}}}\,{f}}\right)$
and
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{4}\\!\left({{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{cofib}}}}\,{f}}\right)$
respectively given by the image of
$1:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}$
under the isomorphism in Lemma 25. These generators may be used to define an
invariant on $\sphere{3}\to\sphere{2}$ called the _Hopf Invariant_. This is
done as follows:

######  Definition 26 (Hopf invariant).

The _Hopf invariant_ of $f$ is the unique integer
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{HI}}}\,f:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}$
such that
${{\gamma_{2}}\;{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\smile$}}\;{\gamma_{2}}}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{HI}}}\,f}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cdot$}}\,\gamma_{4}$.

We remark that the above definition is given for the more general class of
maps $\sphere{2n-1}\to\sphere{n}$ in Brunerie’s thesis. For our purposes, the
above special case suffices. In particular, we may see HI as a function
$\pi_{3}(\sphere{2})\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}$.
The following turns out to be true:

######  Proposition 27.

HI is a homomorphism
$\pi_{3}(\sphere{2})\to{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}$.

###### Proof:

We first rephrase
$f\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{+}}\,g:\pi_{3}(\sphere{2})$
as a composition

$\sphere{3}\xrightarrow{}\sphere{3}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\vee$}}\,\sphere{3}\xrightarrow{f\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\vee$}}\,g}\sphere{2}$

By analyzing the cohomology of
${\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{cofib}}}}\,{(f\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\vee$}}\,g)}$
and the action on generators of the obvious maps from
${\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{cofib}}}}\,{(f\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\vee$}}\,g)}$,
${\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{cofib}}}}\,{f}$
and
${\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{cofib}}}}\,{g}$
into
${\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{cofib}}}}\,{(f\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{+}}\,g)}$,
one arrives at the result with some elementary algebra. ∎

Finally, the Hopf invariant of our element of interest $[i_{2},i_{2}]$ is
computed (up to a sign), using an argument similar to that of the proof of
Proposition 27.

######  Proposition 28.

${\left|{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{HI}}}\,[i_{2},i_{2}]}\right|}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{2}$

We are now almost done: if there is an element $f:\pi_{3}(\sphere{2})$ such
that
${\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{HI}}}\,f}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{1}$,
then HI is an isomorphism
${\pi_{3}(\sphere{2})}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}}$.
Since isomorphisms of this type are unique up to a sign, Proposition 28 tells
us that also for the standard isomorphism
${\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\psi$}}:{\pi_{3}(\sphere{2})}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\cong$}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{ℤ}}}$,
we must have
${\left|{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\psi$}}[i_{2},i_{2}]}\right|}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{2}$,
i.e.
${\left|{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\beta$}}}\right|}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{2}$.
Hence, we have so far shown the following:

######  Lemma 29.

If there is $f:\pi_{3}(\sphere{2})$ with
${\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{HI}}}\,f}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{1}$,
then
${\left|{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\beta$}}}\right|}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{2}$.

The final chapter of Brunerie’s thesis is devoted to proving the antecedent of
Lemma 29.

###  V-B Formalization of cohomology and the Hopf invariant

This section was largely covered by Brunerie, Ljungström and Mörtberg in [12]
and thus also available in
$\mathtt{\color[rgb]{.25,.25,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.25,.25,.25}\pgfsys@color@gray@stroke{.25}\pgfsys@color<EMAIL_ADDRESS>Hence, what remained to be formalized in Chapter 5 was the Hopf invariant and
Propositions 27 and 28. The formalization of these propositions was
straightforward and we were able to translate Brunerie’s proofs in a direct
manner. This is not surprising as the proofs are very algebraic.

For simplicity, we only formalized these propositions as they stand here and
not their generalizations to higher spheres (i.e. as in [4, Prop. 5.4.3 &
5.4.4]). We remark, however, that the formalized proofs easily should be
rephrasable for the general Hopf invariant of maps
$\sphere{2n-1}\to\sphere{n}$.

###  V-C The Gysin sequence

This section corresponds to [4, Chap. 6]. In order to be able to apply Lemma
29, this chapter is devoted to proving that
${\left|{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{HI}}}\,\,\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{hopf}}}}\right|}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{1}$,
where, recall,
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{hopf}}}:\sphere{3}\to\sphere{2}$
is the Hopf map—the generator of $\pi_{3}(\sphere{2})$ from Definition 5. This
amounts to analyzing the cup product on the cohomology of cofib hopf. It is
well-known that cofib hopf gives a model of the complex projective plane
$\mathbb{C}P^{2}$ (see e.g. [28, Example 4.45]), so let us simply write
$\mathbb{C}P^{2}$ from now on. In order to show that
${\left|{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{HI}}}\,\,\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{hopf}}}}\right|}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{1}$,
it suffices to show that
${-}\;{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\smile$}}\;{\gamma_{2}}:\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{2}\\!\left({{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\mathbb{C}P^{2}$}}}\right)\to\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{4}\\!\left({{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\mathbb{C}P^{2}$}}}\right)$
is an isomorphism for
$\gamma_{2}:\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{2}\\!\left({{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\mathbb{C}P^{2}$}}}\right)$
a generator. Brunerie does this by constructing the Gysin sequence
synthetically.

######  Proposition 30 (Gysin sequence).

Let $B$ be a pointed and $0$-connected type and
$P:B\to\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Type}}}$
be a fibration with
$P\,\star_{B}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\simeq_{\star}$}}\,\sphere{n-1}$.
Let $E=\Sigma_{b:B}(P\,b)$ be the total space of $P$. If there is a family of
maps
$c:(b:B)\to(\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Susp}}{$\,(P\,b)$}}\to_{\star}\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{K}}}_{n})$
with $c_{\star_{B}}$ a generator of
$\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{n}\\!\left({\sphere{m}}\right)$,
then there is an element
$e_{n}:\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{n}\\!\left({B}\right)$
and a long exact sequence

${\dots}$${\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{i-1}\\!\left({B}\right)}$${{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{i-1}\\!\left({E}\right)}}$${{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{i-n}\\!\left({B}\right)}}$${{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{i}\\!\left({B}\right)}}$${{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{i}\\!\left({E}\right)}}$${\dots}$$\scriptstyle{{-}\;{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\scriptstyle\smile$}}\;{e_{n}}}$

Moreover, $c$ (and also $e_{n}$) exists when $B$ is $1$-connected.

In order to make use of this, we need the following result.

######  Proposition 31.

There is a fibration
$P:{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\mathbb{C}P^{2}$}}\to\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Type}}}$
with
$P\,\star_{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\mathbb{C}P^{2}$}}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\simeq_{\star}$}}\,\sphere{1}$
and total space $\sphere{5}$.

Proposition 31 is a special case of the following result.

######  Proposition 32 (Iterated Hopf construction).

Given an associative h-space $A$, let
$h_{A}:{A}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{\text{\textasteriskcentered}}}\,{A}\to\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Susp}}{$\,A$}}$
denote the associated Hopf map. There is a fibration
${\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{cofib}}}}\,{h_{A}}\to\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{Type}}}$
with fiber $A$ and total space
${A\,}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{\text{\textasteriskcentered}}}\,{{A\,}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{\text{\textasteriskcentered}}}\,{A}}$.

We consider the particular case when $A=\sphere{1}$ in Proposition 32. In this
case, the map
$h_{\sphere{1}}:{\sphere{1}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{\text{\textasteriskcentered}}}\,{\sphere{1}}\to\sphere{2}$
corresponds to the usual Hopf map under the equivalence
${{\sphere{1}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{\text{\textasteriskcentered}}}\,{\sphere{1}}}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{\sphere{3}}$
and hence
${{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{cofib}}}}\,{h_{\sphere{1}}}}\,\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≃}}\,\,{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\mathbb{C}P^{2}$}}}$.
The total space of this is
${{\sphere{1}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{\text{\textasteriskcentered}}}\,{\sphere{1}}}{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{\text{\textasteriskcentered}}}\,{\sphere{1}}$
which is equivalent to $\sphere{5}$ by Proposition 4 and thus we have proved
Proposition 31. The associated Gysin sequence gives us the main result of this
section:

######  Proposition 33.

${\left|{\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{HI}}}\,h}\right|}\,{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{≡}}\,{1}$

###### Proof:

Since $\mathbb{C}P^{2}$ is $1$-connected, Proposition 30 combined with
Proposition 31 gives us an element
$e_{2}:\textnormal{{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}{H}}}^{2}\\!\left({{\color[rgb]{0,0,0.8046875}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.8046875}\textsf{$\mathbb{C}P^{2}$}}}\right)$
and a sequence