8.5.2 The Hopf construction
Definition 8.5.1.
An Hspace consists of

•
a type $A$,

•
a base point $e:A$,

•
a binary operation^{} $\mu :A\times A\to A$, and

•
for every $a:A$, equalities $\mu (e,a)=a$ and $\mu (a,e)=a$.
Lemma 8.5.2.
Let $A$ be a connected Hspace. Then for every $a\mathrm{:}A$, the maps $\mu \mathit{}\mathrm{(}a\mathrm{,}\mathit{\text{\u2013}}\mathrm{)}\mathrm{:}A\mathrm{\to}A$ and $\mu \mathit{}\mathrm{(}\mathit{\text{\u2013}}\mathrm{,}a\mathrm{)}\mathrm{:}A\mathrm{\to}A$ are equivalences.
Proof.
Let us prove that for every $a:A$ the map $\mu (a,\text{\u2013})$ is an equivalence. The other statement is symmetric^{}. The statement that $\mu (a,\text{\u2013})$ is an equivalence corresponds to a type family $P:A\to \mathrm{\U0001d5af\U0001d5cb\U0001d5c8\U0001d5c9}$ and proving it corresponds to finding a section^{} of this type family.
The type $\mathrm{\U0001d5af\U0001d5cb\U0001d5c8\U0001d5c9}$ is a set (\autorefthm:hlevelnofhlevelSn) hence we can define a new type family ${P}^{\prime}:\parallel A{\parallel}_{0}\to \mathrm{\U0001d5af\U0001d5cb\U0001d5c8\U0001d5c9}$ by ${P}^{\prime}(a{}_{0}):\equiv P(a)$. But $A$ is connected by assumption^{}, hence ${\parallel A\parallel}_{0}$ is contractible. This implies that in order to find a section of ${P}^{\prime}$, it is enough to find a point in the fiber of ${P}^{\prime}$ over ${\lefte\right}_{0}$. But we have ${P}^{\prime}(e{}_{0})=P(e)$ which is inhabited because $\mu (e,\text{\u2013})$ is equal to the identity map^{} by definition of an Hspace, hence is an equivalence.
We have proved that for every $x:\parallel A{\parallel}_{0}$ the proposition^{} ${P}^{\prime}(x)$ is true, hence in particular for every $a:A$ the proposition $P(a)$ is true because $P(a)$ is ${P}^{\prime}(a{}_{0})$. ∎
Definition 8.5.3.
Let $A$ be a connected Hspace. We define a fibration over $\mathrm{\Sigma}\mathit{}A$ using \autoreflem:fibrationoverpushout.
Given that $\mathrm{\Sigma}\mathit{}A$ is the pushout $\mathrm{1}{\mathrm{\bigsqcup}}^{A}\mathrm{1}$, we can define a fibration over $\mathrm{\Sigma}\mathit{}A$ by specifying

•
two fibrations over $\mathrm{\U0001d7cf}$ (i.e. two types ${F}_{1}$ and ${F}_{2}$), and

•
a family $e:A\to ({F}_{1}\simeq {F}_{2})$ of equivalences between ${F}_{1}$ and ${F}_{2}$, one for every element of $A$.
We take $A$ for ${F}_{\mathrm{1}}$ and ${F}_{\mathrm{2}}$, and for $a\mathrm{:}A$ we take the equivalence $\mu \mathit{}\mathrm{(}a\mathrm{,}\mathit{\text{\u2013}}\mathrm{)}$ for $e\mathit{}\mathrm{(}a\mathrm{)}$.
According to \autoreflem:fibrationoverpushout, we have the following diagram:
$$\text{xymatrix}A\text{ar}\mathrm{@}\gg [d]\mathrm{\&}A\times A\text{ar}{[l]}_{}{\mathrm{\U0001d5c9\U0001d5cb}}_{2}\text{ar}\mathrm{@}{\gg}_{{\mathrm{\U0001d5c9\U0001d5cb}}_{1}}[d]\text{ar}{[r]}^{}\mu \mathrm{\&}A\text{ar}\mathrm{@}\gg [d]1\mathrm{\&}A\text{ar}[r]\text{ar}[l]\mathrm{\&}1$$ 
and the fibration we just constructed is a fibration over $\mathrm{\Sigma}A$ whose total space is the pushout of the top line.
Moreover, with $f(x,y):\equiv (\mu (x,y),y)$ we have the following diagram:
$$\text{xymatrix}A{\text{ar}}_{\mathrm{\U0001d5c2\U0001d5bd}}{}_{d}\mathrm{\&}A\times A\text{ar}{[l]}_{}{\mathrm{\U0001d5c9\U0001d5cb}}_{2}{\text{ar}}^{f}[d]\text{ar}{[r]}^{}\mu \mathrm{\&}A{\text{ar}}_{d}^{\mathrm{\U0001d5c2\U0001d5bd}}A\mathrm{\&}A\times A{\text{ar}}^{}{\mathrm{\U0001d5c9\U0001d5cb}}_{2}[l]{\text{ar}}_{}{\mathrm{\U0001d5c9\U0001d5cb}}_{1}[r]\mathrm{\&}A$$ 
The diagram commutes and the three vertical maps are equivalences, the inverse^{} of $f$ being the function $g$ defined by
$$g(u,v):\equiv (\mu {(\text{\u2013},v)}^{1}(u),v).$$ 
This shows that the two lines are equivalent^{} (hence equal) spans, so the total space of the fibration we constructed is equivalent to the pushout of the bottom line. And by definition, this latter pushout is the join of $A$ with itself (see \autorefsec:colimits). We have proven:
Lemma 8.5.4.
Given a connected Hspace $A$, there is a fibration, called the Hopf construction, over $\mathrm{\Sigma}\mathit{}A$ with fiber $A$ and total space $A\mathrm{*}A$.
Title  8.5.2 The Hopf construction 

\metatable 