exercise_solutions.tex

% This is the exercise solution document for the homotopy type theory book.

% This file supports two book sizes:
% - Letter size (8.5" x 11")
% - US Trade size (6" x 9")
%
% To activate one or the other, uncomment the appropriate font size in
% the documentclass below, and then one of the two page geometry incantations
%
% NOTE: The 6" x 9" format is only experimental. It will break the
% title page, for example.

\PassOptionsToPackage{table}{xcolor}

% DOCUMENT CLASS
\documentclass[
%
%10pt % for US Trade 6" x 9" book
%
11pt % for Letter size book
]{article}
\usepackage{etex} % We're running out of registers and dimensions, or some such

\newcounter{chapter}            % So that macros.tex doesn't choke

% PAGE GEOMETRY
%
% Uncomment one of these

% We make the page 40pt taller than the standard LaTeX book.

% OPTION 1: Letter
\usepackage[papersize={8.5in,11in},
            twoside,
            includehead,
            top=1in,
            bottom=1in,
            inner=0.75in,
            outer=1.0in,
            bindingoffset=0.35in]{geometry}

% OPTION 2: US Trade
% \usepackage[papersize={6in,9in},
%             twoside,
%             includehead,
%             top=0.75in,
%             bottom=0.75in,
%             inner=0.5in,
%             outer=0.75in,
%             bindingoffset=0.35in]{geometry}

% HYPERLINKING AND PDF METADATA

\usepackage[pagebackref,
            colorlinks,
            citecolor=darkgreen,
            linkcolor=darkgreen,
            unicode,
            pdfauthor={Univalent Foundations Program},
            pdftitle={Homotopy Type Theory: Univalent Foundations of Mathematics},
            pdfsubject={Mathematics},
            pdfkeywords={type theory, homotopy theory, univalence axiom}]{hyperref}

% OTHER PACKAGES

% Use this package and stick \layout somewhere in the text to see
% page margins, text size and width etc. Useful for debugging page format.
%\usepackage{layout}

%%% Because Germans have umlauts and Slavs have even stranger ways of mangling letters
\usepackage[utf8]{inputenc}

%%% For table {tab:theorems}
\usepackage{pifont}

%%% Multi-Columns for long lists of names
\usepackage{multicol}

%%% Set the fonts
\usepackage{mathpazo}
\usepackage[scaled=0.95]{helvet}
\usepackage{courier}
\linespread{1.05} % Palatino looks better with this

\usepackage{graphicx}
\DeclareGraphicsExtensions{.png}
\input{bmpsize-hack} % for bounding boxes in dvi mode
\usepackage{comment}

\usepackage{wallpaper} % For the background image on the cover page

\usepackage{fancyhdr} % To set headers and footers

\usepackage{nextpage} % So we can jump to odd-numbered pages

\usepackage{amssymb,amsmath,amsthm,stmaryrd,mathrsfs,wasysym}
\usepackage{enumitem,mathtools,xspace}
\usepackage{xcolor} % For colored cells in tables we need \cellcolor
\usepackage{booktabs} % For nice tables
\usepackage{array} % For nice tables
\usepackage{supertabular} % For index of symbols
\definecolor{darkgreen}{rgb}{0,0.45,0}
\usepackage{aliascnt}
\usepackage[capitalize]{cleveref}
\usepackage[all,2cell]{xy}
\UseAllTwocells
\usepackage{braket} % used for \setof{ ... } macro
\usepackage{tikz}
\usetikzlibrary{decorations.pathmorphing}

\usepackage{etoolbox}           % hacking commands for TOC

\usepackage{mathpartir}         % for formal.tex appendix, section 3

\usepackage[numbered]{bookmark} % add chapter/section numbers to the toc in the pdf metadata

\input{macros}

%%%% Indexing
\usepackage{makeidx}
\makeindex

%%%% Header and footers
\pagestyle{fancyplain}
\setlength{\headheight}{15pt}
\renewcommand{\sectionmark}[1]{\markright{\textsc{\thesection\ #1}}}
\newcommand{\transfun}[3]{\mathcal{I}_{#1}(#2, #3)}
\newcommand{\nathom}[2]{\mathsf{nat}_{#1}(#2)}
\newcommand{\Tgh}[2]{\mathcal{T}_1(#1,#2)}
\newcommand{\T}[2]{\mathcal{T}_2(#1,#2)}
\newcommand{\TT}[2]{\mathcal{T}_3(#1,#2)}
\newcommand{\I}{\mathcal{I}_1}
\newcommand{\II}{\mathcal{I}_2}
\newcommand{\hapfuneq}{\mathsf{happly}\mbox{-}\mathsf{funext}\mbox{-}\mathsf{inv}}

\lhead[\fancyplain{}{{\thepage}}]%
      {\fancyplain{}{\nouppercase{\rightmark}}}
\rhead[\fancyplain{}{\nouppercase{\leftmark}}]%
      {\fancyplain{}{\thepage}}
\cfoot{\textsc{\scriptsize \textcolor{gray}{[Draft of \today]}}}
\lfoot[]{}
\rfoot[]{}

%%%% Chapter & part style
\usepackage{titlesec}
\titleformat{\part}[display]{\fontsize{40}{40}\fontseries{m}\fontshape{sc}\selectfont}{\hfil\partname\ \Roman{part}}{20pt}{\fontsize{60}{60}\fontseries{b}\fontshape{sc}\selectfont\hfil}
\titleformat{\chapter}[display]{\fontsize{23}{25}\fontseries{m}\fontshape{it}\selectfont}{\chaptertitlename\ \thechapter}{20pt}{\fontsize{35}{35}\fontseries{b}\fontshape{n}\selectfont}

\input{main.labels}

\title{Solutions to selected exercises}

\begin{document}
\maketitle

\section*{Exercises from \cref{cha:typetheory}}

\subsection*{Solution to \cref{ex:composition}}

We of course know what composition of functions $f : A \to B$ and $g : B \to C$ should be, but let us see how we might derive it by considering available forms of construction. We want a term
\[ g \circ f \defeq (\Box : A \to C), \]
where $\Box : A \to C$ indicates that in place of $\Box$ we would like to put something of type $A \to C$.
Since we are defining a function whose domain is $A$, we expect it to be of the form
\[ g \circ f \defeq \lam{x:A} (\Box : C), \]
so now we are looking for something of type $C$, with $x$, $f$ and $g$ available. Of these $g$ looks most promising as it lands in $C$:
\[ g \circ f \defeq \lam{x:A} g (\Box : B). \]
Now we repeat the same trick with $f$ to get
\[ g \circ f \defeq \lam{x:A} g(f(\Box : A)). \]
Inside the abstraction $x$ is available and has the type we need, so we define
\begin{equation}
  \label{eq:composdef}
   g \circ f \defeq \lam{x:A} g(f(x)) : C
\end{equation}
%
This baby example demonstrates how one often works with a proof assistant: look at what
you need and what is available, and try to make some progress.

Now, suppose given also $h : C \to D$. We have, according to \cref{eq:composdef},
%
\begin{align*}
  h \circ (g \circ f) &\jdeq \lamu{x:A} h ((\lam{y:A} g(f(y))) x)\\
                      &\jdeq \lamu{x:A} h(g(f(x))),
\end{align*}
%
and
%
\begin{align*}
  (h \circ  g) \circ f & \jdeq \lamu{x:A} (\lam{y:A} h(g(y))) (f(x))\\
                       & \jdeq \lamu{x:A} h(g(f(x))).
\end{align*}
%
They are equal, which establishes associativity of composition.

\subsection*{Solution to \cref{ex:pr-to-rec}}

If we suppose given only $\fst : A \times B \to A$ and $\snd : A \times B \to B$ satisfying $\fst(\tup{a}{b}) \jdeq a$ and $\snd(\tup{a}{b})\jdeq b$, we can define $\rec{A\times B}'$ by
\[ \rec{A\times B}'(C,g,x) \defeq g (\fst x) (\snd x). \]
We can now verify, given $C:\UU$, $g:A\to B \to C$ and $(a,b):A\times B$,
\begin{align*}
  \rec{A\times B}'(C,g,(a,b)) &\jdeq g (\fst (a,b)) (\snd (a,b))\\
                              &\jdeq g (a) (b).
\end{align*}
%
For $\Sigma$-types we replace $A \times B$ above with $\sm{a:A} B(a)$, but otherwise
everything else stays the same:
\[ \rec{\sm{x:A} B(x)}'(C,g,x) \defeq g (\fst x) (\snd x). \]

\subsection*{Solution to \cref{ex:pr-to-ind}}

Quite naturally, we form
\[ \ind{A\times B}''(C,g,x) \defeq g (\fst x) (\snd x),\]
of type
\[ \prd{C:A\times B \to \UU}\Parens{\prd{y:A}\prd{z:B} C(\tup yz)} \to
   \prd{x : A \times B} C (\tup{\fst x}{\snd x}). \]
This is not quite what we need because $\ind{A\times B}$ has the type
\[ \prd{C:A\times B \to \UU}\Parens{\prd{y:A}\prd{z:B} C(\tup{y}{z})} \to
   \prd{x : A \times B} C (x). \]
%
Recall that we have the propositional uniqueness principle
%
\[ \uniq{A\times B}: \prd{x : A \times B} (\id[A\times B]{\tup{\fst x}{\snd x}}{x}), \]
%
satisfying $\id{\uniq{A\times B}(\tup{a}{b})}{\refl{(a,b)}}$.
We can transport along $\uniq{A\times B}(x)$ to get from $C(\tup{\fst x}{\snd x})$ to $C(x)$:
%
\[ \ind{A\times B}'(C,g,x) \defeq
    \transfib{C}{\uniq{A\times B}(x)}{\ind{A \times B}''(C, g, x)}.
\]
%
It remains to verify that $\ind{A \times B}'(C, g, x)$ behaves as expected:
%
\begin{align*}
  \ind{A \times B}'(C,g,(a,b))
  &\jdeq \transfib{C}{\uniq{A\times B}(\tup{a}{b})}{g(\fst \tup{a}{b})(\snd\tup{a}{b})} \\
  &\jdeq \transfib{C}{\uniq{A\times B}(\tup{a}{b})}{g(a)(b)} \\
  &\jdeq \transfib{C}{\refl{\tup ab}}{g(a)(b)} \\
  &\jdeq g(a)(b).
\end{align*}
%
Now for $\Sigma$-types the exact same expressions work as well, except that the types change.

\section*{Exercises from \cref{cha:basics}}

\subsection*{Solution to \cref{ex:npaths}}

In general, when defining an ``$n$-foo'', one should ensure that a ``$1$-foo''
is just a ``foo'' (e.g.\ a 1-category is just a category). In this case, a
$1$-path in some type $A$ should just be a path, that is, an equality $\id[A]
xy$ between some elements $x,y:A$. Then a 0-path should probably be an
element of $A$. We also know that a $2$-path, or homotopy, is a pair of
$1$-paths and an equality between them. Our definition should extrapolate from
this pattern. 

Define $C\defeq \lam{n}\type\to\type$. By the induction principle for $\nat$, it
suffices to give terms
\begin{gather*}
  c_0 : \type\to\type \\
  c_s : \prd{n:\nat}\prd{f:\type\to\type}\type\to\type
\end{gather*}
Define these by
\begin{align*}
  c_0 &\defeq \idfunc[\type] \\
  c_s(n,f,A) &\defeq \sm{x,y:f(A)}\id[]xy
\end{align*}
That is to say, an $(n+1)$-dimensional path should be a pair of $n$-dimensional
paths, together with a path between them. More concisely:
\begin{gather*}
  \operatorname{npath} : \nat\to\type\to\type \\
  \operatorname{npath} \defeq \ind{\nat}\Parens{\lam{n}\type\to\type, \idfunc[\type], \lam{n}\lam{f}\lam{A}\Parens{\sm{x,y:f(A)}\id[]xy}}
\end{gather*}

What should the boundary of an $n$-path be? The boundary of a $1$-path is
a pair of points. The boundary of a $2$-path (that is, a homotopy) is a pair of
$1$-paths. Perhaps the boundary of an $(n+1)$-path should be a pair of
$n$-paths. We can get these by using the appropriate projections:
\begin{gather*}
  \operatorname{nboundary} :
  \prd{n:\nat}\prd{A:\type}\operatorname{npath}(\suc(n),A)\to
  \operatorname{npath}(n,A)\times \operatorname{npath}(n,A) \\
  \operatorname{nboundary}(p)\defeq (\proj{1}(p),\proj{1}(\proj{2}(p)))
\end{gather*}

\section*{Exercises from \cref{cha:logic}}

\subsection*{Solution to \cref{ex:equiv-functor-set}}

% Prove that if $\eqv A B$ and $A$ is a set, then so is $B$.

Generally, we can use univalence to transform equivalences to equalities
(paths), and use the principle indiscernability of identicals (transport) to
show that any statement (family) that holds for one type holds for any type it
is equivalent to. 

Let $A,B:\type$, $s:\isset(A)$, and $\eqv A B$. By univalence, there is
a path $p:A=_{\type}B$. We can transport $s$ across this path to obtain the
desired result:
\begin{equation*}
	\transfib{X\mapsto \isset(X)}{p}{s} : \isset(B)
\end{equation*}

\subsection*{Solution to \cref{ex:isset-coprod}}

Let $A,B:\type$, and assume that $A$ and $B$ are sets. To show $\isset(A+B)$, we
must show that there is at most one path between elements of $A+B$, up to
homotopy. Let $x,y:A+B$. We proceed by case analysis on $x$ and $y$.

Consider the cases where $x\jdeq \inl(a)$ and $y\jdeq \inr(b)$ or
$x\jdeq \inr(b)$ and $y\jdeq \inl(a)$ for some $a:A$ and $b:B$. By the
characterization of paths in coproduct types (\cref{sec:compute-coprod}), these
can't be equal. In particular, by \eqref{eq:inlrdj}, given $p:x=y$, we can
conclude anything we like.

Now suppose that $x\jdeq \inl(a_1)$ and $y\jdeq \inl(a_2)$ for $a_1,a_2:A$. Then
by \eqref{eq:inlinj},
\begin{equation*}
	(x=y)\jdeq {(\inl(a_1)=\inl(a_2))}\eqvsym {(a_1=a_2)}.
\end{equation*}
Since $A$ is a set, $a_1=a_2$ is a mere proposition. It follows that
$x=y$ is a mere proposition (one can use univalence and
transport, as in the previous exercise). A symmetric proof shows that 
in the case that $x\jdeq \inr(b_1)$ and $y\jdeq \inr(b_2)$ for $b_1,b_2:B$,
$x=y$ is also a mere proposition. Therefore, $A+B$ is a set.

\subsection*{Solution to \cref{ex:prop-endocontr}}

($\Rightarrow$) Let $A:\type$ and $P:\isprop(A)$. To show that
$A\to A$ is contractible, we must give a center of contraction and show that
every other function $A\to A$ is equal to the center. Define our center to be
$\idfunc[A]$, and let $f:A\to A$. Define a homotopy $\idfunc[A]\htpy f$ by
\begin{gather*}
  \alpha:\prd{x:A}\id[]{\idfunc[A](x)}{f(x)} \\
  \alpha(x)\defeq P(\idfunc[A](x),f(x))
\end{gather*}
Then by function extensionality, $\idfunc[A]=f$.

($\Leftarrow$) Assume $A\to A$ is contractible with center of contraction $c$,
and let $x,y:A$. We want to show that $x=y$. Define $f:A\to A$ by $f(z)\defeq
y$. By contractability of $A\to A$, $\idfunc[A]=c=f$. Using $\happly$ on the
equality between $\idfunc[A]$ and $f$, we obtain that
$x\jdeq \idfunc[A](x)=f(x)\jdeq y$, so $\id[]xy$. We have shown that any
two elements of $A$ are equal, that is, $A$ is a mere proposition.

\subsection*{Solution to \cref{ex:lem-mereprop}}

Assume $A$ is a proposition, and let $x,y:A+(\neg A)$. We want to show that
$x=y$. We proceed by cases using the induction principle for coproducts.
\begin{enumerate}
  \item Assume $x\jdeq \inl(a)$ and $y\jdeq \inr(n)$. Then
    $n(a):\emptyt$ gives us a contradiction.
  \item Assume $x\jdeq \inr(n)$ and $y\jdeq \inl(a)$. Then
    $n(a):\emptyt$ gives us a contradiction.
  \item Assume $x\jdeq \inl(a_1)$ and $y\jdeq \inl(a_2)$. By the
    characterization of paths in coproduct types (\cref{sec:compute-coprod}), we
    know $\eqv{(\id[]xy)}{(\id[]{a_1}{a_2})}$, and we have $\id[]{a_1}{a_2}$
    since $A$ is a proposition. 
  \item Finally, assume $x\jdeq \inr(n_1)$ and $y\jdeq \inr(n_2)$.
    Again by the characterization of paths in coproduct types, we know
    $\eqv{(\id[]xy)}{(\id[]{n_1}{n_2})}$, so it suffices to show $\id[]{n_1}{n_2}$.
    Since $\neg A\jdeq A\to \emptyt$ and $\emptyt$ is a mere proposition, we
    have by \cref{thm:isprop-forall} that $\neg A$ is a mere proposition.
    Therefore, any two elements of $\neg A$ are equal, and in particular,
    $\id[]{n_1}{n_2}$.
\end{enumerate}

\subsection*{Solution to \cref{ex:disjoint-or}}

Assume $h:\neg(A\times B)$, and let $x,y:A+B$. We want to show that
$x=y$. We proceed by cases using the induction principle for coproducts.
\begin{enumerate}
  \item Assume $x\jdeq \inl(a)$ and $y\jdeq \inr(b)$ for $a:A$ and $b:B$.
    Then $h(a,b):\emptyt$, and we can use the destructor for $\emptyt$ to
    conclude anything we wish.
  \item Assume $x\jdeq \inr(b)$ and $y\jdeq \inl(a)$. Then $h(a,b):\emptyt$, and
    we're done.
  \item Assume $x\jdeq \inl(a_1)$ and $y\jdeq \inl(a_2)$. By the
    characterization of paths in coproduct types (\cref{sec:compute-coprod}), we
    know $\eqv{(\id[]xy)}{(\id[]{a_1}{a_2})}$, and we have $\id[]{a_1}{a_2}$
    since $A$ is a proposition. 
  \item Assume $x\jdeq \inr(b_1)$ and $y\jdeq \inr(b_2)$. Just as above,
    we have $\eqv{(\id[]xy)}{(\id[]{b_1}{b_2})}$, and $\id[]{b_1}{b_2}$.
\end{enumerate}

\subsection*{Solution to \cref{ex:decidable-choice}}

The hypotheses imply that
\[ \Parens{\sm{n:\nat}P(n)} \to \sm{n:\nat}\Parens{P(n) \times \prd{m:\nat} \big((m<n) \to \neg P(m)\big)}. \]
In words, given $n$ such that $P(n)$, we can find the least such $n$: we test every $m<n$ in turn, using decidability to do a case analysis, until we find the first one that satisfies $P(m)$.
However, the right-hand side of the above implication is a mere proposition: if both $n$ and $n'$ are least numbers satisfying~$P$ then they must be equal.
Therefore, we also have
\[ \Brck{\sm{n:\nat}P(n)} \to \sm{n:\nat}\Parens{P(n) \times \prd{m:\nat} \big((m<n) \to \neg P(m)\big)} \]
from which the claim follows.

\section*{Exercises from \cref{cha:equivalences}}

\subsection*{Solution to \cref{ex:symmetric-equiv}}

First note that for any type $A$ we have $\eqv{\iscontr(A)}{A\times \iscontr(A)}$.
Thus
\begin{align*}
  \prd{a:A} \iscontr\Parens{\sm{b:B} R(a,b)}
  &\eqvsym \prd{a:A} \Parens{\sm{b:B} R(a,b)} \times  \iscontr\Parens{\sm{b:B} R(a,b)}\\
  &\eqvsym \Parens{\prd{a:A}\sm{b:B} R(a,b)} \times  \Parens{\prd{a:A}\iscontr\Parens{\sm{b:B} R(a,b)}}\\
  &\eqvsym \Parens{\sm{f:A\to B} \prd{a:A} R(a,f(a))} \times  \Parens{\prd{a:A}\iscontr\Parens{\sm{b:B} R(a,b)}}
\end{align*}
using \cref{thm:ttac} at the last step.
So the type given in the exercise is equivalent to
\begin{equation*}
\sm{f:A\to B}{R:A\to B\to \type}
\Parens{\prd{a:A} R(a,f(a))}\times
\Parens{\prd{a:A} \iscontr\Parens{\sm{b:B} R(a,b)}} \times
\Parens{\prd{b:B} \iscontr\Parens{\sm{a:A} R(a,b)}}.
\end{equation*}
It will therefore suffice to show that for any $f:A\to B$, the type
\begin{equation}\label{eq:symmetric-isequiv}
\sm{R:A\to B\to \type}
\Parens{\prd{a:A} R(a,f(a))}\times
\Parens{\prd{a:A} \iscontr\Parens{\sm{b:B} R(a,b)}} \times
\Parens{\prd{b:B} \iscontr\Parens{\sm{a:A} R(a,b)}}.
\end{equation}
is equivalent to $\isequiv(f)$, or equivalently that it satisfies the three desiderata of $\isequiv(f)$.

Firstly, suppose $f$ has a quasi-inverse $g$, and define $R(a,b) \defeq (f(a)=b)$.
For any $a$ we have $\iscontr(\sm{b:B} R(a,b))$ by \cref{thm:contr-paths}, and in particular we have $R(a,f(a))$.
On the other hand, by \cref{thm:paths-respects-equiv} we have $\eqv{R(a,b)}{(gf(a) = g(b))}$, which is equivalent to $a = g(b)$, so \cref{thm:contr-paths} also implies that $\iscontr(\sm{a:A} R(a,b))$ for any $b:B$.

Secondly, suppose~\eqref{eq:symmetric-isequiv} is inhabited, i.e.\  we have $R:A\to B\to \type$ and witnesses $r:\prd{a:A} R(a,f(a))$ and $c:\prd{a:A} \iscontr(\sm{b:B} R(a,b))$ and $d:\prd{b:B} \iscontr(\sm{a:A} R(a,b))$.
Let $g(b) \defeq \proj1 (\proj1(d(b)))$, yielding $g:B\to A$; thus we have $R(g(b),b)$ for any $b:B$.
Then for any $a_0:A$ we have $R(a_0,f(a_0))$ and $R(g(f(a_0)),f(a_0))$; but $\sm{a:A} R(a,f(a_0))$ is contractible, so $a_0 = g(f(a_0))$.
Similarly, $b_0 = f(g(b_0))$ for any $b_0:B$, so $g$ is a quasi-inverse to $f$.

Finally, we must show that~\eqref{eq:symmetric-isequiv} is a mere proposition.
Since $\prd{b:B} \iscontr\Parens{\sm{a:A} R(a,b)}$ is a mere proposition by \cref{thm:isprop-forall,thm:isprop-iscontr}, by \cref{thm:path-subset} we may ignore it and consider only the remainder:
\begin{equation*}
\sm{R:A\to B\to \type}
\Parens{\prd{a:A} R(a,f(a))}\times
\Parens{\prd{a:A} \iscontr\Parens{\sm{b:B} R(a,b)}}.
\end{equation*}
Using \cref{thm:ttac} again, this is equivalent to
\begin{equation*}
\prd{a:A}\sm{R:B\to \type} R(fa)\times \iscontr\Parens{\sm{b:B} R(b)}.
\end{equation*}
Thus it will suffice to show that for any $b_0:B$, the type
\[ \sm{R:B\to \type} R(b_0)\times \iscontr\Parens{\sm{b:B} R(b)} \]
is a mere proposition.
But in fact, this type is contractible; its center of contraction consists of $\lam{b}(b_0=b)$ and $\refl{b_0}$ and \cref{thm:contr-paths}, and the contracting homotopy arises from \cref{thm:identity-systems}\ref{item:identity-systems4}$\Rightarrow$\ref{item:identity-systems3} (together with univalence and function extensionality).

\subsection*{Solution to \cref{ex:embedding-cancellable}}

An embedding clearly has properties~\ref{item:ex:ec1} and~\ref{item:ex:ec2}.
Conversely, suppose $f$ has properties~\ref{item:ex:ec1} and~\ref{item:ex:ec2} and let $x,y:A$; we must show that $\apfunc f: (x=y) \to (f(x)=f(y))$ is an equivalence.
By \cref{thm:equiv-inhabcod}, we are free to assume that $f(x)=f(y)$.
Thus, by~\ref{item:ex:ec1}, we have some $p:x=y$.
Now the following square commutes by \cref{lem:ap-functor}:
\begin{equation*}
  \vcenter{\xymatrix@C=4pc{
      \Omega(A,y)\ar[r]^-{p\ct\blank}\ar[d]_{\apfunc{f}} &
      (x=y)\ar[d]^{\apfunc{f}}\\
      \Omega(B,f(y))\ar[r]_-{\ap f p \ct \blank} &
      (f(x)=f(y)).
      }}
\end{equation*}
Both horizontal maps are equivalences by \cref{ex:equiv-concat}, while the left-hand vertical map is an equivalence by~\ref{item:ex:ec2}.
Thus, by \cref{thm:two-out-of-three}, so is the right-hand vertical map, as desired.

As for examples, the unique map $\bool\to\unit$ satisfies~\ref{item:ex:ec2} but not~\ref{item:ex:ec1}, while the map $\lam{x}\bool:\unit\to\UU$ satisfies~\ref{item:ex:ec1} but not~\ref{item:ex:ec2}.

\section*{Exercises from \cref{cha:hits}}

\subsection*{Solution to \cref{ex:torus}}
The torus $T^2$ is a higher inductive type generated by a point $b : T^2$, two paths $p : b = b$, $q : b = b$, and a 2-path $t : p \ct q = q \ct p$. The recursion principle thus says that given $C : \type$, for a function $f : T^2 \to C$ we require
\begin{itemize}
\item a point $b':C$,
\item a path $p' : b' = b'$,
\item a path $q' : b' = b'$, and
\item a 2-path $t' : p' \ct q' = q' \ct p'$.
\end{itemize}
The recursor $f : T^2 \to C$ then has the property that $f(b) \jdeq b'$. Furthermore, there exist terms $\beta : \ap{f}{p} = p'$ and $\gamma : \ap{f}{q} = q'$ such that the following diagram commutes:
\begin{center}
\begin{tikzpicture}
\node (Nc) at (1.5,0) {=};
\node (N0) at (0,1.5) {$\ap{f}{p\ct q}$};
\node (N1) at (3,1.5) {$\ap{f}{q\ct p}$};
\node (N2) at (0,0) {$\ap{f}{p}\ct\ap{f}{q}$};
\node (N3) at (3,0) {$\ap{f}{q}\ct\ap{f}{p}$};
\node (N4) at (0,-1.5) {$p' \ct q'$};
\node (N5) at (3,-1.5) {$q' \ct p'$};
\draw[-] (N0) -- node[above]{\footnotesize $\mapfunc{\mapfunc{f}}(t)$} (N1);
\draw[-] (N0) -- node[left]{} (N2);
\draw[-] (N1) -- node[above]{} (N3);
\draw[-] (N2) -- node[left]{\footnotesize via $\beta$, $\gamma$} (N4);
\draw[-] (N3) -- node[right]{\footnotesize via $\beta$, $\gamma$} (N5);
\draw[-] (N4) -- node[below]{\footnotesize $t'$} (N5);
\end{tikzpicture}
\end{center}

The induction principle is more complicated; it says that given a family $P : T^2 \to \type$, for a section $f : \prd{x:T^2} P(x)$ we require
\begin{itemize}
\item a point $b':P(b)$,
\item a path $p' : \trans{p}{b'} = b'$,
\item a path $q' : \trans{q}{b'} = b'$, and
\item a 2-path $t'$ witnessing the equality of the following two paths from $\trans{(q\ct p)}{b'}$ to $b'$:
\begin{align*}
& \opp{\big(\mapfunc{\alpha \mapsto \trans{\alpha}{b'}}(t)\big)} \ct \big(\happly_{\transfun{P}{p}{q}}(b') \ct \mapfunc{\transf{q}}(p') \ct q' \big)\\
& \happly_{\transfun{P}{q}{p}}(b') \ct \mapfunc{\transf{p}}(q') \ct p'
\end{align*}
where for any type family $B : A \to \type$ and paths $\alpha: x =_A y$ and $\alpha' : y =_A z$, the path \[\transfun{E}{\alpha}{\alpha'} : \transf{(\alpha \ct \alpha')} = \lam{u:B(x)} \trans{\alpha'}{\trans{\alpha}{u}}\] is obtained by a path induction on $\alpha$ and $\alpha'$.
\end{itemize}
The inductor $f : \prd{x:T^2} P(x)$ then has the property that $f(b) \jdeq b'$. Furthermore, there exist terms $\beta : \mapdep{f}{p} = p'$ and $\gamma : \mapdep{f}{q} = q'$ such that the 2-path
\[ \mapdep{\mapdepfunc{f}}{t} : \transfib{\alpha \mapsto \trans{\alpha}{b'} = b'}{t}{\mapdepfunc{f}{(p\ct q)}} = \mapdepfunc{f}{(q \ct p)} \]
is equal to the 2-path
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,7.5) {$\transfib{\alpha \mapsto \trans{\alpha}{b'} = b'}{t}{\mapdepfunc{f}{(p\ct q)}}$};
\node (N1) at (0,6) {$\opp{\big(\mapfunc{\alpha \mapsto \trans{\alpha}{b'}}(t)\big)} \ct \mapdepfunc{f}{(p\ct q)}$};
\node (N2) at (0,4.5) {$\opp{\big(\mapfunc{\alpha \mapsto \trans{\alpha}{b'}}(t)\big)} \ct \big(\happly_{\transfun{P}{p}{q}}(b') \ct \mapfunc{\transf{q}}(\mapdep{f}{p}) \ct \mapdep{f}{q}\big)$};
\node (N3) at (0,3) {$\opp{\big(\mapfunc{\alpha \mapsto \trans{\alpha}{b'}}(t)\big)} \ct \big(\happly_{\transfun{P}{p}{q}}(b') \ct \mapfunc{\transf{q}}(p') \ct q'\big)$};
\node (N4) at (0,1.5) {$\happly_{\transfun{P}{q}{p}}(b') \ct \mapfunc{\transf{p}}(q') \ct p'$};
\node (N5) at (0,0) {$\happly_{\transfun{P}{q}{p}}(b') \ct \mapfunc{\transf{p}}(\mapdep{f}{q}) \ct \mapdep{f}{p}$};
\node (N6) at (0,-1.5) {$\mapdep{f}{q\ct p}$};
\draw[-] (N0) -- node[right]{\footnotesize $\mathcal{T}^{b'}_{\alpha \mapsto \trans{\alpha}{b'}}(t,\mapdepfunc{f}{(p\ct q)})$} (N1);
\draw[-] (N1) -- node[right]{\footnotesize via $\mathcal{D}_f(p,q)$} (N2);
\draw[-] (N2) -- node[right]{\footnotesize via $\beta$, $\gamma$} (N3);
\draw[-] (N3) -- node[right]{\footnotesize $t'$} (N4);
\draw[-] (N4) -- node[right]{\footnotesize via $\opp{\beta}$, $\opp{\gamma}$} (N5);
\draw[-] (N5) -- node[right]{\footnotesize $\opp{\mathcal{D}_f(q,p)}$} (N6);
\end{tikzpicture}
\end{center}
where for any $g : A \to B$, $c : B$, $\alpha : a =_A a'$ and $u : g(a) =_B c$, the path \[\mathcal{T}_g^c(\alpha,u) : \transfib{x \to g(x) = c}{\alpha}{u} = \opp{\ap{g}{\alpha}} \ct u\]
is obtained by a straightforward path induction on $\alpha$. Similarly, for any $g : \prd{x : A}B(x)$ and paths $\alpha: x =_A y$, $\alpha' : y =_A z$, the path
\[ \mathcal{D}_g(\alpha,\alpha') : \mapdep{g}{\alpha \ct \alpha'} = \happly_{\transfun{B}{\alpha}{\alpha'}}(g(x)) \ct \mapfunc{\transf{\alpha'}}(\mapdep{g}{\alpha}) \ct \mapdep{g}{\alpha'}\]
is obtained by a path induction on $\alpha$ and $\alpha'$.

\subsection*{Solution to \cref{ex:torus-s1-times-s1}}

\subsubsection*{Logical equivalence between $\Sn^1 \times \Sn^1$ and $T^2$}
We define a function $f : \Sn^1 \to T^2$ by circle recursion, mapping $\base \mapsto b$ and $\lloop \mapsto p$. We define a function $F^\to : \Sn^1 \to \Sn^1 \to T^2$ again by circle recursion, mapping $\base \mapsto f$ and $\lloop \mapsto \funext(H)$, where $H : \prd{x:\Sn^1} f(x) = f(x)$ is defined by circle induction as follows. We map $\base$ to $q$ and $\lloop$ to the path
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,3) {$\transfib{z \mapsto f(z) = f(z)}{\lloop}{q}$};
\node (N1) at (0,1.5) {$\opp{\ap{f}{\lloop}} \ct (q \ct \ap{f}{\lloop})$};
\node (N2) at (0,0) {$q$};
\draw[-] (N0) -- node[right]{\footnotesize $\Tgh{\lloop}{q}$} (N1);
\draw[-] (N1) -- node[right]{\footnotesize $\I(\delta)$} (N2);
\end{tikzpicture}
\end{center}
where for any $\alpha : x =_{\Sn^1} y$, and $u : f(x) = f(x)$, the path \[\Tgh{\alpha}{u} : \transfib{z \mapsto f(z) = f(z)}{\alpha}{u} = \opp{\ap{f}{\alpha}} \ct u \ct \ap{f}{\alpha} \]
is obtained by a straightforward path induction on $\alpha$. For any $u : a =_A b$, $v : b =_A d$, $w : a =_A c$, $z : c =_A d$, we have functions
\begin{align*}
\I & : (u \ct v = w \ct z) \to (\opp{u} \ct w \ct z = v)\\
\I^{-1} & : (\opp{u} \ct w \ct z = v) \to (u \ct v = w \ct z)
\end{align*}
defined by path induction on $u$ and $z$, which form a quasi-equivalence. Finally, $\delta$ is the path
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,4.5) {$\ap{f}{\lloop} \ct q$};
\node (N1) at (0,3) {$p \ct q$};
\node (N2) at (0,1.5) {$q \ct p$};
\node (N3) at (0,0) {$q \ct \ap{f}{\lloop}$};
\draw[-] (N0) -- node[right]{\footnotesize via $\beta_f$} (N1);
\draw[-] (N1) -- node[right]{\footnotesize $t$} (N2);
\draw[-] (N2) -- node[right]{\footnotesize via $\beta_f$} (N3);
\end{tikzpicture}
\end{center}
where $\beta_f : \ap{f}{\lloop} = p$ witnesses the second computation rule for the circle.

Having defined a function $F^\to : \Sn^1 \to \Sn^1 \to T^2$, it is now straightforward to define a function $F^\times : \Sn^1 \times \Sn^1 \to T^2$. For the other direction, we define $G : T^2 \to \Sn^1 \times \Sn^1$ by torus recursion as follows. We map $b \mapsto (\base,\base)$, $p \mapsto \pairpath(\refl{\base},\lloop)$, $q \mapsto \pairpath(\lloop, \refl{\base})$, and $t \mapsto \Phi_{\lloop,\lloop}$, where for $\alpha : x =_A x'$ and $\alpha' : y =_A y'$,
\[ \Phi_{\alpha,\alpha'} : \Big(\pairpath(\refl{x},\alpha') \ct \pairpath(\alpha, \refl{y'})\Big) = \Big(\pairpath(\alpha, \refl{y}) \ct \pairpath(\refl{x'},\alpha')\Big) \]
is defined by induction on $\alpha'$.

This completes the definition of a logical equivalence between $\Sn^1 \times \Sn^1$ and $T^2$. Before we proceed to show that it is in fact a quasi-equivalence, we note a few key properties of the functions $H$, $F^\times$, $G$ constructed above.

The 1-path computation rule for $F^\to$ gives us a term
\[ \beta_{F^\to} : \ap{F^\to}{\lloop} = \funext(H) \]
The 1-path computation rules for $G$ give us terms
\begin{align*}
& \beta_G : \ap{G}{p} = \pairpath(\refl{\base},\lloop)\\
& \gamma_G : \ap{G}{q} =\pairpath(\lloop, \refl{\base})
\end{align*}
The 2-path computation rule for $G$ gives us the following commuting diagram:
\begin{center}
\begin{tikzpicture}
\node (Nc) at (4.5,0) {$(1)$};
\node (N0) at (0,1.5) {$\ap{G}{p\ct q}$};
\node (N1) at (9,1.5) {$\ap{G}{q\ct p}$};
\node (N2) at (0,0) {$\ap{G}{p}\ct\ap{G}{q}$};
\node (N3) at (9,0) {$\ap{G}{q}\ct\ap{G}{p}$};
\node (N4) at (0,-1.5) {$\pairpath(\refl{},\lloop) \ct \pairpath(\lloop, \refl{})$};
\node (N5) at (9,-1.5) {$\pairpath(\lloop, \refl{}) \ct \pairpath(\refl{},\lloop)$};
\draw[-] (N0) -- node[above]{\footnotesize via $t$} (N1);
\draw[-] (N0) -- node[left]{} (N2);
\draw[-] (N1) -- node[above]{} (N3);
\draw[-] (N2) -- node[left]{\footnotesize via $\beta_G$, $\gamma_G$} (N4);
\draw[-] (N3) -- node[right]{\footnotesize via $\beta_G$, $\gamma_G$} (N5);
\draw[-] (N4) -- node[below]{\footnotesize $\Phi_{\lloop,\lloop}$} (N5);
\end{tikzpicture}
\end{center}
For any $\alpha : x =_{T^2} x'$ and $\alpha' : y =_{T^2} y'$, we have path families
\begin{align*}
& \mu(\alpha') : \ap{F^\times}{\pairpath(\refl{x},\alpha')} = \ap{F^\to(x)}{\alpha'}\\
& \nu(\alpha) : \ap{F^\times}{\pairpath(\alpha,\refl{y})} = \happly_{\ap{F^\to}{\alpha}}(y)
\end{align*}
defined by path induction on $\alpha$ and $\alpha'$.

The function $H$ is a homotopy between $f$ and $f$. As such, for any path $\alpha : x =_{\Sn^1} y$, there exists a 2-path \[\nathom{H}{\alpha} : \ap{f}{\alpha} \ct H(y)  = H(x) \ct \ap{f}{\alpha}\] defined by induction on $\alpha$. In the case when $\alpha \defeq \lloop$, we can show that the following diagram commutes:
\begin{center}
\begin{tikzpicture}
\node (Na) at (2,1) {$(2)$};
\node (N0) at (0,2) {$\ap{f}{\lloop} \ct q$};
\node (N1) at (4,2) {$p \ct q$};
\node (N2) at (0,0) {$q \ct \ap{f}{\lloop}$};
\node (N3) at (4,0) {$q \ct p$};
\draw[-] (N0) -- node[above]{\footnotesize via $\beta_f$} (N1);
\draw[-] (N1) -- node[right]{\footnotesize $t$} (N3);
\draw[-] (N0) -- node[left]{\footnotesize $\nathom{H}{\lloop}$} (N2);
\draw[-] (N2) -- node[below]{\footnotesize via $\beta_f$} (N3);
\end{tikzpicture}
\end{center}
To show this, we note that for any $\alpha : x =_{\Sn^1} y$, applying $\I^{-1}$ to the path
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,3) {$\opp{\ap{f}{\alpha}} \ct H(x) \ct \ap{f}{\alpha}$};
\node (N1) at (0,1.5) {$\transfib{z \mapsto f(z) = f(z)}{\alpha}{H(x)}$};
\node (N2) at (0,0) {$H(y)$};
\draw[-] (N0) -- node[right]{\footnotesize $\opp{\Tgh{\alpha}{H(x)}}$} (N1);
\draw[-] (N1) -- node[right]{\footnotesize $\mapdep{H}{\alpha}$} (N2);
\end{tikzpicture}
\end{center}
yields precisely $\nathom{H}{\alpha}$ (by a simple path induction on $\alpha$). The second computation rule for $H$ tells us that $\mapdep{H}{\lloop} = \Tgh{\lloop}{q} \ct \I(\delta)$. Thus
\[\nathom{H}{\lloop} = \I^{-1}\big(\opp{\Tgh{\lloop}{q}} \ct \mapdep{H}{\lloop}\big) = \delta \]
which proves the commutativity of $(2)$.

\subsubsection*{Equivalence between $\Sn^1 \times \Sn^1$ and $T^2$}
\paragraph*{Left-to-right}
We need to show that for any $x,y : \Sn^1$ we have $G(F^\times(x,y)) = (x,y)$. To use the circle induction, we first define a path family $\epsilon : \prd{y:\Sn^1} G(f(y)) = (\base,y)$. The definition of $\epsilon$ itself proceeds by circle induction: we map $\base$ to the path $\refl{(\base,\base)}$ and $\lloop$ to the path
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,6) {$\transfib{z \mapsto G(f(z)) = (\base,z)}{\lloop}{\refl{}}$};
\node (N1) at (0,4.5) {$\opp{\ap{G}{\ap{f}{\lloop}}} \ct \refl{} \ct \pairpath(\refl{},\lloop)$};
\node (N2) at (0,3) {$\refl{}$};
\draw[-] (N0) -- node[right]{\footnotesize $\T{\lloop}{\refl{}}$} (N1);
\draw[-] (N1) -- node[right]{\footnotesize $\I(\kappa)$} (N2);
\end{tikzpicture}
\end{center}
where for any $\alpha : x =_{\Sn^1} y$ and $u : G(f(x)) = (\base,x)$, the path \[\T{\alpha}{u} : \transfib{z \mapsto G(f(z)) = (\base,z)}{\alpha}{u} = \opp{\ap{G}{\ap{f}{\alpha}}} \ct u \ct \pairpath(\refl{},\alpha) \]
is defined by path induction on $\alpha$. Finally, $\kappa$ is the path
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,6) {$\ap{G}{\ap{f}{\lloop}} \ct \refl{}$};
\node (N1) at (0,4.5) {$\ap{G}{\ap{f}{\lloop}}$};
\node (N2) at (0,3) {$\pairpath(\refl{},\lloop)$};
\node (N3) at (0,1.5) {$\refl{} \ct \pairpath(\refl{},\lloop)$};
\draw[-] (N0) -- node[right]{} (N1);
\draw[-] (N1) -- node[right]{\footnotesize via $\beta_f$, $\beta_G$} (N2);
\draw[-] (N2) -- node[right]{} (N3);
\end{tikzpicture}
\end{center}
This finishes the definition of $\epsilon$. As before, for any $\alpha : x =_{\Sn^1} y$ we have a 2-path \[\nathom{\epsilon}{\alpha} : \ap{G}{\ap{f}{\alpha}} \ct \epsilon(y) = \epsilon(x) \ct \pairpath(\refl{},\alpha)\] defined by induction on $\alpha$. In the case $\alpha \defeq \lloop$, the following diagram commutes:
\begin{center}
\begin{tikzpicture}
\node (Na) at (2,1) {$(3)$};
\node (N0) at (0,2) {$\ap{G}{\ap{f}{\lloop}} \ct \refl{}$};
\node (N1) at (4,2) {$\ap{G}{\ap{f}{\lloop}}$};
\node (N2) at (0,0) {$\refl{} \ct \pairpath(\refl{},\lloop)$};
\node (N3) at (4,0) {$\pairpath(\refl{},\lloop)$};
\draw[-] (N0) -- node[above]{\footnotesize} (N1);
\draw[-] (N1) -- node[right]{\footnotesize via $\beta_f$, $\beta_G$} (N3);
\draw[-] (N0) -- node[left]{\footnotesize $\nathom{\epsilon}{\lloop}$} (N2);
\draw[-] (N2) -- node[below]{\footnotesize} (N3);
\end{tikzpicture}
\end{center}
To show this, we note that for any $\alpha : x =_{\Sn^1} y$, applying $\I^{-1}$ to the path
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,3) {$\opp{\ap{G}{\ap{f}{\alpha}}} \ct \epsilon(x) \ct \pairpath(\refl{},\alpha)$};
\node (N1) at (0,1.5) {$\transfib{z \mapsto G(f(z)) = (\base,z)}{\alpha}{\epsilon(x)}$};
\node (N2) at (0,0) {$\epsilon(y)$};
\draw[-] (N0) -- node[right]{\footnotesize $\opp{\T{\alpha}{\epsilon(x)}}$} (N1);
\draw[-] (N1) -- node[right]{\footnotesize $\mapdep{\epsilon}{\alpha}$} (N2);
\end{tikzpicture}
\end{center}
yields precisely $\nathom{\epsilon}{\alpha}$ (by a simple path induction on $\alpha$). The second computation rule for $\epsilon$ tells us that $\mapdep{\epsilon}{\lloop} = \T{\lloop}{\refl{}} \ct \I(\kappa)$. Thus
\[\nathom{\epsilon}{\lloop} = \I^{-1}\big(\opp{\T{\lloop}{\refl{}}} \ct \mapdep{\epsilon}{\lloop}\big) = \kappa \]
which proves the commutativity of $(3)$.

All that remains now is to prove that \[\transfib{x \mapsto \prd{y:\Sn^1} G(F^\times(x,y)) = (x,y)}{\lloop}{\epsilon} = \epsilon\] The left endpoint can be expressed explicitly as the function
\[ y \mapsto \opp{\ap{G}{\happly_{\ap{F^\to}{\lloop}}(y)}} \ct \epsilon(y) \ct \pairpath(\lloop,\refl{})\]
as a generalization of $\lloop$ to an arbitrary $\alpha$ and a subsequent path induction on $\alpha$ shows. By function extensionality it thus suffices to show that for any $y : \Sn^1$, we have
\[ \opp{\ap{G}{\happly_{\ap{F^\to}{\lloop}}(y)}} \ct \epsilon(y) \ct \pairpath(\lloop,\refl{}) = \epsilon(y) \]
The left endpoint can be simplified using $\beta_{F^\to}$ and the fact that $\happly$ and $\funext$ form a quasi-inverse:
\[ \opp{\ap{G}{H(y)}} \ct \epsilon(y) \ct \pairpath(\lloop,\refl{}) = \epsilon(y) \]
Showing the above is the same as showing
\[ \ap{G}{H(y)} \ct \epsilon(y) = \epsilon(y) \ct \pairpath(\lloop,\refl{}) \]
for any $y :\Sn^1$. We proceed yet again by circle induction. We map $\base$ to the path $\eta$ below:
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,3) {$\ap{G}{q} \ct \refl{}$};
\node (N1) at (0,1.5) {$\ap{G}{q}$};
\node (N2) at (0,0) {$\pairpath(\lloop,\refl{})$};
\node (N3) at (0,-1.5) {$\refl{} \ct \pairpath(\lloop,\refl{})$};
\draw[-] (N0) -- node[right]{\footnotesize} (N1);
\draw[-] (N1) -- node[right]{\footnotesize $\gamma_G$} (N2);
\draw[-] (N2) -- node[right]{\footnotesize} (N3);
\end{tikzpicture}
\end{center}
Now it remains to show that
\[ \transfib{z \mapsto \ap{G}{H(z)} \ct \epsilon(z) = \epsilon(z) \ct \pairpath(\lloop,\refl{})}{\lloop}{\eta} = \eta \]
For any $u : a =_A b$, $v : b =_A d$, $w : a =_A c$, $z : c =_A d$, we have functions
\begin{align*}
\II & : (u \ct v = w \ct z) \to (v \ct \opp{z} = \opp{u} \ct w) \\
\II^{-1} & : (v \ct \opp{z} = \opp{u} \ct w) \to (u \ct v = w \ct z)
\end{align*}
defined by induction on $u$ and $z$, which form a quasi-equivalence.
For any $\alpha : x =_{\Sn^1} y$, let $\delta^\star(\alpha)$ be the path
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,3) {$\ap{G}{\ap{f}{\alpha}} \ct \ap{G}{H_y}$};
\node (N1) at (0,1.5) {$\ap{G}{\ap{f}{\alpha} \ct H_y}$};
\node (N2) at (0,0) {$\ap{G}{H_x \ct \ap{f}{\alpha}}$};
\node (N3) at (0,-1.5) {$\ap{G}{H_x} \ct \ap{G}{\ap{f}{\alpha}}$};
\draw[-] (N0) -- node[right]{\footnotesize} (N1);
\draw[-] (N1) -- node[right]{\footnotesize via $\nathom{H}{\alpha}$} (N2);
\draw[-] (N2) -- node[right]{\footnotesize} (N3);
\end{tikzpicture}
\end{center}
Given any $\alpha : x =_{\Sn^1} y$ and $\eta' : G(H(x)) \ct \eta(x) = \eta(x) \ct \pairpath(\lloop,\refl{})$, we can now express the path $\transfib{z \mapsto \ap{G}{H(z)} \ct \epsilon(z) = \epsilon(z) \ct \pairpath(\lloop,\refl{})}{\alpha}{\eta'}$ explicitly as the following path:
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,19.8)  {$\ap{G}{H_y} \ct \epsilon_y$};
\node (N1) at (0,18.15){$\ap{G}{H_y} \ct \Big(\opp{\ap{G}{\ap{f}{\alpha}}} \ct \ap{G}{\ap{f}{\alpha}}\Big) \ct \epsilon_y$};
\node (N2) at (0,16.5)  {$\Big(\ap{G}{H_y} \ct \opp{\ap{G}{\ap{f}{\alpha}}}\Big) \ct \Big(\ap{G}{\ap{f}{\alpha}} \ct \epsilon_y\Big)$};
\node (N3) at (0,14.85){$\Big(\opp{\ap{G}{\ap{f}{\alpha}}} \ct \ap{G}{H_x}\Big) \ct \Big(\ap{G}{\ap{f}{\alpha}} \ct \epsilon_y\Big)$};
\node (N4) at (0,13.2){$\Big(\opp{\ap{G}{\ap{f}{\alpha}}}\ct \ap{G}{H_x}\Big) \ct \Big(\epsilon_x \ct \pairpath(\refl{},\alpha)\Big)$};
\node (N5) at (0,11.55){$\opp{\ap{G}{\ap{f}{\alpha}}}\ct\Big(\ap{G}{H_x}\ct \epsilon_x\Big) \ct \pairpath(\refl{},\alpha)$};
\node (N6) at (0,9.9){$\opp{\ap{G}{\ap{f}{\alpha}}}\ct\Big(\epsilon_x\ct\pairpath(\lloop,\refl{})\Big) \ct \pairpath(\refl{},\alpha)$};
\node (N7) at (0,8.25){$\Big(\opp{\ap{G}{\ap{f}{\alpha}}}\ct\epsilon_x\Big)\ct\Big(\pairpath(\lloop,\refl{})\ct \pairpath(\refl{},\alpha)\Big)$};
\node (N8) at (0,6.6){$\Big(\opp{\ap{G}{\ap{f}{\alpha}}}\ct\epsilon_x\Big)\ct\Big(\pairpath(\refl{},\alpha)\ct \pairpath(\lloop,\refl{})\Big)$};
\node (N9) at (0,4.95){$\opp{\ap{G}{\ap{f}{\alpha}}}\ct\Big(\epsilon_x\ct\pairpath(\refl{},\alpha)\Big)\ct\pairpath(\lloop,\refl{})$};
\node (N10) at (0,3.3){$\opp{\ap{G}{\ap{f}{\alpha}}}\ct\Big(\ap{G}{\ap{f}{\alpha}}\ct\epsilon_y\Big)\ct\pairpath(\lloop,\refl{})$};
\node (N11) at (0,1.65){$\Big(\opp{\ap{G}{\ap{f}{\alpha}}}\ct\ap{G}{\ap{f}{\alpha}}\Big)\ct\Big(\epsilon_y\ct\pairpath(\lloop,\refl{})\Big)$};
\node (N12) at (0,0){$\epsilon_y\ct\pairpath(\lloop,\refl{})$};
\draw[-] (N0) -- node[right]{\footnotesize} (N1);
\draw[-] (N1) -- node[right]{\footnotesize} (N2);
\draw[-] (N2) -- node[right]{\footnotesize via $\II(\delta^\star(\alpha))$} (N3);
\draw[-] (N3) -- node[right]{\footnotesize via $\nathom{\epsilon}{\alpha}$} (N4);
\draw[-] (N4) -- node[right]{\footnotesize} (N5);
\draw[-] (N5) -- node[right]{\footnotesize via $\eta'$} (N6);
\draw[-] (N6) -- node[right]{\footnotesize} (N7);
\draw[-] (N7) -- node[right]{\footnotesize via $\Phi^{-1}_{\lloop,\alpha}$} (N8);
\draw[-] (N8) -- node[right]{\footnotesize} (N9);
\draw[-] (N9) -- node[right]{\footnotesize via $\opp{\nathom{\epsilon}{\alpha}}$} (N10);
\draw[-] (N10) -- node[right]{\footnotesize} (N11);
\draw[-] (N11) -- node[right]{\footnotesize} (N12);
\end{tikzpicture}
\end{center}
In the case $\alpha \defeq \lloop$ and $\eta' \defeq \eta$ we thus have:
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,19.8)  {$\ap{G}{q} \ct \refl{}$};
\node (N1) at (0,18.15){$\ap{G}{q} \ct \Big(\opp{\ap{G}{\ap{f}{\lloop}}} \ct \ap{G}{\ap{f}{\lloop}}\Big) \ct \refl{}$};
\node (N2) at (0,16.5)  {$\Big(\ap{G}{q} \ct \opp{\ap{G}{\ap{f}{\lloop}}}\Big) \ct \Big(\ap{G}{\ap{f}{\lloop}} \ct \refl{}\Big)$};
\node (N3) at (0,14.85){$\Big(\opp{\ap{G}{\ap{f}{\lloop}}} \ct \ap{G}{q}\Big) \ct \Big(\ap{G}{\ap{f}{\lloop}} \ct \refl{}\Big)$};85
\node (N4) at (0,13.2){$\Big(\opp{\ap{G}{\ap{f}{\lloop}}}\ct \ap{G}{q}\Big) \ct \Big(\refl{} \ct \pairpath(\refl{},\lloop)\Big)$};
\node (N5) at (0,11.55){$\opp{\ap{G}{\ap{f}{\lloop}}}\ct\Big(\ap{G}{q}\ct \refl{}\Big) \ct \pairpath(\refl{},\lloop)$};
\node (N6) at (0,9.8){$\opp{\ap{G}{\ap{f}{\lloop}}}\ct\Big(\refl{}\ct\pairpath(\lloop,\refl{})\Big) \ct \pairpath(\refl{},\lloop)$};
\node (N7) at (0,8.25){$\Big(\opp{\ap{G}{\ap{f}{\lloop}}}\ct\refl{}\Big)\ct\Big(\pairpath(\lloop,\refl{})\ct \pairpath(\refl{},\lloop)\Big)$};
\node (N8) at (0,6.6){$\Big(\opp{\ap{G}{\ap{f}{\lloop}}}\ct\refl{}\Big)\ct\Big(\pairpath(\refl{},\lloop)\ct \pairpath(\lloop,\refl{})\Big)$};
\node (N9) at (0,4.95){$\opp{\ap{G}{\ap{f}{\lloop}}}\ct\Big(\refl{}\ct\pairpath(\refl{},\lloop)\Big)\ct\pairpath(\lloop,\refl{})$};
\node (N10) at (0,3.3){$\opp{\ap{G}{\ap{f}{\lloop}}}\ct\Big(\ap{G}{\ap{f}{\lloop}}\ct\refl{}\Big)\ct\pairpath(\lloop,\refl{})$};
\node (N11) at (0,1.65){$\Big(\opp{\ap{G}{\ap{f}{\lloop}}}\ct\ap{G}{\ap{f}{\lloop}}\Big)\ct\Big(\refl{}\ct\pairpath(\lloop,\refl{})\Big)$};
\node (N12) at (0,0){$\refl{}\ct\pairpath(\lloop,\refl{})$};
\draw[-] (N0) -- node[right]{\footnotesize} (N1);
\draw[-] (N1) -- node[right]{\footnotesize} (N2);
\draw[-] (N2) -- node[right]{\footnotesize via $\II(\delta^\star(\lloop))$} (N3);
\draw[-] (N3) -- node[right]{\footnotesize via $\nathom{\epsilon}{\lloop}$} (N4);
\draw[-] (N4) -- node[right]{\footnotesize} (N5);
\draw[-] (N5) -- node[right]{\footnotesize via $\eta$} (N6);
\draw[-] (N6) -- node[right]{\footnotesize} (N7);
\draw[-] (N7) -- node[right]{\footnotesize via $\Phi^{-1}_{\lloop,\lloop}$} (N8);
\draw[-] (N8) -- node[right]{\footnotesize} (N9);
\draw[-] (N9) -- node[right]{\footnotesize via $\opp{\nathom{\epsilon}{\lloop}}$} (N10);
\draw[-] (N10) -- node[right]{\footnotesize} (N11);
\draw[-] (N11) -- node[right]{\footnotesize} (N12);
\end{tikzpicture}
\end{center}
We can now use the commutativity of $(3)$ and get rid of the extraneous identity paths to obtain:
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,19.8)  {$\ap{G}{q} \ct \refl{}$};
\node (N1) at (0,18.15) {$\ap{G}{q}$};
\node (N2) at (0,16.5)  {$\ap{G}{q} \ct \Big(\opp{\ap{G}{\ap{f}{\lloop}}} \ct \ap{G}{\ap{f}{\lloop}}\Big)$};
\node (N3) at (0,14.85) {$\Big(\ap{G}{q} \ct \opp{\ap{G}{\ap{f}{\lloop}}}\Big) \ct \ap{G}{\ap{f}{\lloop}}$};
\node (N4) at (0,13.2)  {$\Big(\opp{\ap{G}{\ap{f}{\lloop}}} \ct \ap{G}{q}\Big) \ct \ap{G}{\ap{f}{\lloop}}$};
\node (N5) at (0,11.55) {$\Big(\opp{\ap{G}{\ap{f}{\lloop}}}\ct \ap{G}{q}\Big) \ct \pairpath(\refl{},\lloop)$};
\node (N6) at (0,9.8)   {$\Big(\opp{\ap{G}{\ap{f}{\lloop}}}\ct\pairpath(\lloop,\refl{})\Big) \ct \pairpath(\refl{},\lloop)$};
\node (N7) at (0,8.25)  {$\opp{\ap{G}{\ap{f}{\lloop}}}\ct\Big(\pairpath(\lloop,\refl{})\ct \pairpath(\refl{},\lloop)\Big)$};
\node (N8) at (0,6.6)   {$\opp{\ap{G}{\ap{f}{\lloop}}}\ct\Big(\pairpath(\refl{},\lloop)\ct \pairpath(\lloop,\refl{})\Big)$};
\node (N9) at (0,4.95)  {$\Big(\opp{\ap{G}{\ap{f}{\lloop}}}\ct\pairpath(\refl{},\lloop)\Big)\ct\pairpath(\lloop,\refl{})$};
\node (N10) at (0,3.3)  {$\Big(\opp{\ap{G}{\ap{f}{\lloop}}}\ct\ap{G}{\ap{f}{\lloop}}\Big)\ct\pairpath(\lloop,\refl{})$};
\node (N11) at (0,1.65) {$\pairpath(\lloop,\refl{})$};
\node (N12) at (0,0) {$\refl{}\ct\pairpath(\lloop,\refl{})$};
\draw[-] (N0) -- node[right]{\footnotesize} (N1);
\draw[-] (N1) -- node[right]{\footnotesize} (N2);
\draw[-] (N2) -- node[right]{\footnotesize} (N3);
\draw[-] (N3) -- node[right]{\footnotesize via $\II(\delta^\star(\lloop))$} (N4);
\draw[-] (N4) -- node[right]{\footnotesize via $\beta_f$, $\beta_G$} (N5);
\draw[-] (N5) -- node[right]{\footnotesize via $\gamma_G$} (N6);
\draw[-] (N6) -- node[right]{\footnotesize} (N7);
\draw[-] (N7) -- node[right]{\footnotesize via $\Phi^{-1}_{\lloop,\lloop}$} (N8);
\draw[-] (N8) -- node[right]{\footnotesize} (N9);
\draw[-] (N9) -- node[right]{\footnotesize via $\beta^{-1}_G$, $\beta^{-1}_f$} (N10);
\draw[-] (N10) -- node[right]{\footnotesize} (N11);
\draw[-] (N11) -- node[right]{\footnotesize} (N12);
\end{tikzpicture}
\end{center}
or equivalently:
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,19.8)  {$\ap{G}{q} \ct \refl{}$};
\node (N1) at (0,18.15) {$\ap{G}{q}$};
\node (N2) at (0,16.5)  {$\ap{G}{q} \ct \Big(\opp{\ap{G}{\ap{f}{\lloop}}} \ct \ap{G}{\ap{f}{\lloop}}\Big)$};
\node (N3) at (0,14.85) {$\Big(\ap{G}{q} \ct \opp{\ap{G}{\ap{f}{\lloop}}}\Big) \ct \ap{G}{\ap{f}{\lloop}}$};
\node (N4) at (0,13.2)  {$\Big(\opp{\ap{G}{\ap{f}{\lloop}}} \ct \ap{G}{q}\Big) \ct \ap{G}{\ap{f}{\lloop}}$};
\node (N5) at (0,11.55) {$\Big(\opp{\ap{G}{\ap{f}{\lloop}}}\ct \ap{G}{q}\Big) \ct \pairpath(\refl{},\lloop)$};
\node (N6) at (0,9.8)   {$\Big(\opp{\ap{G}{\ap{f}{\lloop}}}\ct\pairpath(\lloop,\refl{})\Big) \ct \pairpath(\refl{},\lloop)$};
\node (N7) at (0,8.25)  {$\opp{\ap{G}{\ap{f}{\lloop}}}\ct\Big(\pairpath(\lloop,\refl{})\ct \pairpath(\refl{},\lloop)\Big)$};
\node (N8) at (0,6.6)   {$\opp{\ap{G}{\ap{f}{\lloop}}}\ct\Big(\pairpath(\refl{},\lloop)\ct \pairpath(\lloop,\refl{})\Big)$};
\node (N9) at (0,4.95)  {$\Big(\opp{\ap{G}{\ap{f}{\lloop}}}\ct\pairpath(\refl{},\lloop)\Big)\ct\pairpath(\lloop,\refl{})$};
\node[red] (N10) at (0,3.3)  {$\Big(\opp{\pairpath(\refl{},\lloop)}\ct\pairpath(\refl{},\lloop)\Big)\ct\pairpath(\lloop,\refl{})$};
\node (N11) at (0,1.65) {$\pairpath(\lloop,\refl{})$};
\node (N12) at (0,0) {$\refl{}\ct\pairpath(\lloop,\refl{})$};
\draw[-] (N0) -- node[right]{\footnotesize} (N1);
\draw[-] (N1) -- node[right]{\footnotesize} (N2);
\draw[-] (N2) -- node[right]{\footnotesize} (N3);
\draw[-] (N3) -- node[right]{\footnotesize via $\II(\delta^\star(\lloop))$} (N4);
\draw[-] (N4) -- node[right]{\footnotesize via $\beta_f$, $\beta_G$} (N5);
\draw[-] (N5) -- node[right]{\footnotesize via $\gamma_G$} (N6);
\draw[-] (N6) -- node[right]{\footnotesize} (N7);
\draw[-] (N7) -- node[right]{\footnotesize via $\Phi^{-1}_{\lloop,\lloop}$} (N8);
\draw[-] (N8) -- node[right]{\footnotesize} (N9);
\draw[red,-] (N9) -- node[right]{\footnotesize via $\beta_f$, $\beta_G$} (N10);
\draw[red,-] (N10) -- node[right]{\footnotesize} (N11);
\draw[-] (N11) -- node[right]{\footnotesize} (N12);
\end{tikzpicture}
\end{center}
After some rearranging we get:
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,19.8)  {$\ap{G}{q} \ct \refl{}$};
\node (N1) at (0,18.15) {$\ap{G}{q}$};
\node (N2) at (0,16.5)  {$\ap{G}{q} \ct \Big(\opp{\ap{G}{\ap{f}{\lloop}}} \ct \ap{G}{\ap{f}{\lloop}}\Big)$};
\node (N3) at (0,14.85) {$\Big(\ap{G}{q} \ct \opp{\ap{G}{\ap{f}{\lloop}}}\Big) \ct \ap{G}{\ap{f}{\lloop}}$};
\node[red] (N4) at (0,13.2)  {$\Big(\ap{G}{q} \ct \opp{\ap{G}{\ap{f}{\lloop}}}\Big) \ct \pairpath(\refl{},\lloop)$};
\node (N5) at (0,11.55) {$\Big(\opp{\ap{G}{\ap{f}{\lloop}}}\ct \ap{G}{q}\Big) \ct \pairpath(\refl{},\lloop)$};
\node (N6) at (0,9.8)   {$\Big(\opp{\ap{G}{\ap{f}{\lloop}}}\ct\pairpath(\lloop,\refl{})\Big) \ct \pairpath(\refl{},\lloop)$};
\node[red] (N7) at (0,8.25)  {$\Big(\opp{\pairpath(\refl{},\lloop)}\ct\pairpath(\lloop,\refl{})\Big)\ct \pairpath(\refl{},\lloop)$};
\node[red] (N8) at (0,6.6)   {$\opp{\pairpath(\refl{},\lloop)}\ct\Big(\pairpath(\lloop,\refl{})\ct \pairpath(\refl{},\lloop)\Big)$};
\node[red] (N9) at (0,4.95)  {$\opp{\pairpath(\refl{},\lloop)}\ct\Big(\pairpath(\refl{},\lloop)\ct\pairpath(\lloop,\refl{})\Big)$};
\node (N10) at (0,3.3)  {$\Big(\opp{\pairpath(\refl{},\lloop)}\ct\pairpath(\refl{},\lloop)\Big)\ct\pairpath(\lloop,\refl{})$};
\node (N11) at (0,1.65) {$\pairpath(\lloop,\refl{})$};
\node (N12) at (0,0) {$\refl{}\ct\pairpath(\lloop,\refl{})$};
\draw[-] (N0) -- node[right]{\footnotesize} (N1);
\draw[-] (N1) -- node[right]{\footnotesize} (N2);
\draw[-] (N2) -- node[right]{\footnotesize} (N3);
\draw[red,-] (N3) -- node[right]{\footnotesize via $\beta_f$, $\beta_G$} (N4);
\draw[red,-] (N4) -- node[right]{\footnotesize via $\II(\delta^\star(\lloop))$} (N5);
\draw[-] (N5) -- node[right]{\footnotesize via $\gamma_G$} (N6);
\draw[red,-] (N6) -- node[right]{\footnotesize via $\beta_f$, $\beta_G$} (N7);
\draw[red,-] (N7) -- node[right]{\footnotesize} (N8);
\draw[red,-] (N8) -- node[right]{\footnotesize via $\Phi^{-1}_{\lloop,\lloop}$} (N9);
\draw[red,-] (N9) -- node[right]{\footnotesize} (N10);
\draw[-] (N10) -- node[right]{\footnotesize} (N11);
\draw[-] (N11) -- node[right]{\footnotesize} (N12);
\end{tikzpicture}
\end{center}
We now observe the following:
\begin{itemize}
\item For any paths $\alpha_u : u_1 =_{a =_A b} u_2$, $\alpha_v : v_1 =_{b =_A d} v_2$, $\alpha_w : w_1 =_{a =_A c} w_2$, $\alpha_z : z_1 =_{c =_A d} z_2$ and $\phi : u_1 \ct v_1 = w_1 \ct z_1$, $\phi' : u_2 \ct v_2 = w_2 \ct z_2$, we have
\begin{center}
\begin{tikzpicture}
\node (Na) at (2.5,1) {$=$};
\node (N0) at (0,2) {$u_1 \ct v_1$};
\node (N1) at (2.5,2) {$u_1 \ct v_2$};
\node (N2) at (5,2) {$u_2 \ct v_2$};
\node (N3) at (0,0) {$w_1 \ct z_1$};
\node (N4) at (2.5,0) {$w_1 \ct z_2$};
\node (N5) at (5,0) {$w_2 \ct z_2$};
\draw[-] (N0) -- node[above]{\footnotesize via $\alpha_v$} (N1);
\draw[-] (N1) -- node[above]{\footnotesize via $\alpha_u$} (N2);
\draw[-] (N0) -- node[left]{\footnotesize $\phi$} (N3);
\draw[-] (N3) -- node[below]{\footnotesize via $\alpha_z$} (N4);
\draw[-] (N4) -- node[below]{\footnotesize via $\alpha_w$} (N5);
\draw[-] (N2) -- node[right]{\footnotesize $\phi'$} (N5);
\end{tikzpicture}
\end{center}
if and only if
\begin{center}
\begin{tikzpicture}
\node (Na) at (2.5,1) {$=$};
\node (N0) at (0,2) {$v_1 \ct z^{-1}_1$};
\node (N1) at (2.5,2) {$v_1 \ct z^{-1}_2$};
\node (N2) at (5,2) {$v_2 \ct z^{-1}_2$};
\node (N3) at (0,0) {$u^{-1}_1 \ct w_1$};
\node (N4) at (2.5,0) {$u^{-1}_1 \ct w_2$};
\node (N5) at (5,0) {$u^{-1}_2 \ct w_2$};
\draw[-] (N0) -- node[above]{\footnotesize via $\alpha_z$} (N1);
\draw[-] (N1) -- node[above]{\footnotesize via $\alpha_v$} (N2);
\draw[-] (N0) -- node[left]{\footnotesize $\II(\phi)$} (N3);
\draw[-] (N3) -- node[below]{\footnotesize via $\alpha_w$} (N4);
\draw[-] (N4) -- node[below]{\footnotesize via $\alpha_u$} (N5);
\draw[-] (N2) -- node[right]{\footnotesize $\II(\phi')$} (N5);
\end{tikzpicture}
\end{center}
This follows at once by path induction on $\alpha_u, \alpha_v, \alpha_w, \alpha_z$ and the fact that $\II$ is an equivalence.
\end{itemize}
Next we want to show that the following diagram commutes:
\begin{center}
\begin{tikzpicture}
\node (Na) at (4.5,1) {$(4)$};
\node (N0) at (0,2) {$\ap{G}{\ap{f}{\lloop}} \ct \ap{G}{q}$};
\node (N1) at (0,0) {$\ap{G}{q} \ct \ap{G}{\ap{f}{\lloop}}$};
\node (N2) at (9,2) {$\pairpath(\refl{},\lloop) \ct \pairpath(\lloop,\refl{})$};
\node (N3) at (9,0) {$\pairpath(\lloop,\refl{}) \ct \pairpath(\refl{},\lloop)$};
\draw[-] (N0) -- node[left]{\footnotesize $\delta^\star(\lloop)$} (N1);
\draw[-] (N0) -- node[above]{\footnotesize via $\beta_f$, $\beta_G$, $\gamma_G$} (N2);
\draw[-] (N2) -- node[right]{\footnotesize $\Phi_{\lloop,\lloop}$} (N3);
\draw[-] (N1) -- node[below]{\footnotesize via $\beta_f$, $\beta_G$, $\gamma_G$} (N3);
\end{tikzpicture}
\end{center}
This is the same as saying that the outer rectangle in the diagram below commutes:
\begin{center}
\begin{tikzpicture}
\node (Na) at (2.5,4.125) {A};
\node (Nb) at (2.5,2.375) {B};
\node (Nc) at (2.5,0.725) {C};
\node (Nd) at (8,2.475) {D};
\node (N0) at (0,4.95) {$\ap{G}{\ap{f}{\lloop}} \ct \ap{G}{q}$};
\node (N2) at (5,4.95) {$\ap{G}{p} \ct \ap{G}{q}$};
\node (N4) at (11,4.95) {$\pairpath(\refl{},\lloop) \ct \pairpath(\lloop,\refl{})$};
\node (N1) at (0,3.3) {$\ap{G}{\ap{f}{\lloop}\ct q}$};
\node (N1c) at (0,1.65) {$\ap{G}{q\ct \ap{f}{\lloop}}$};
\node (N3) at (0,0) {$\ap{G}{q}\ct\ap{G}{\ap{f}{\lloop}}$};
\node (N5) at (5,0) {$\ap{G}{q} \ct \ap{G}{p}$};
\node (N7) at (11,0) {$\pairpath(\lloop,\refl{}) \ct \pairpath(\refl{},\lloop)$};
\node (N6) at (5,3.3) {$\ap{G}{p\ct q}$};
\node (N6a) at (5,1.65) {$\ap{G}{q\ct p}$};

\draw[-] (N0) -- node[above]{\footnotesize via $\beta_f$} (N2);
\draw[-] (N2) -- node[above]{\footnotesize via $\beta_G$, $\gamma_G$} (N4);
\draw[-] (N0) -- node[left]{\footnotesize} (N1);
\draw[-] (N1c) -- node[left]{\footnotesize} (N3);
\draw[-] (N3) -- node[below]{\footnotesize via $\beta_f$} (N5);
\draw[-] (N5) -- node[below]{\footnotesize via $\beta_G$, $\gamma_G$} (N7);
\draw[-] (N4) -- node[right]{\footnotesize $\Phi_{\lloop,\lloop}$} (N7);
\draw[-] (N1) -- node[below]{\footnotesize via $\beta_f$} (N6);
\draw[-] (N6) -- node[right]{\footnotesize via $t$} (N6a);
\draw[-] (N1c) -- node[below]{\footnotesize via $\beta_f$} (N6a);
\draw[-] (N2) -- node[above]{\footnotesize} (N6);
\draw[-] (N1) -- node[left]{\footnotesize $\nathom{H}{\lloop}$} (N1c);
\draw[-] (N6a) -- node[below]{\footnotesize} (N5);
\end{tikzpicture}
\end{center}
But this is clear: A and C obviously commute, B is precisely the diagram $(2)$, and D is the diagram $(1)$.

Since $(4)$ commutes, by our earlier observation the following diagram commutes:
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,2) {$\ap{G}{q} \ct \opp{\ap{G}{\ap{f}{\lloop}}}$};
\node (N1) at (0,0) {$\opp{\ap{G}{\ap{f}{\lloop}}} \ct \ap{G}{q}$};
\node (N2) at (9,2) {$\pairpath(\lloop,\refl{}) \ct \opp{\pairpath(\refl{},\lloop)}$};
\node (N3) at (9,0) {$\opp{\pairpath(\refl{},\lloop)} \ct \pairpath(\lloop,\refl{})$};
\draw[-] (N0) -- node[left]{\footnotesize $\II(\delta^\star(\lloop))$} (N1);
\draw[-] (N0) -- node[above]{\footnotesize via $\beta_f$, $\beta_G$, $\gamma_G$} (N2);
\draw[-] (N2) -- node[right]{\footnotesize $\II(\Phi_{\lloop,\lloop})$} (N3);
\draw[-] (N1) -- node[below]{\footnotesize via $\gamma_G$, $\beta_f$, $\beta_G$} (N3);
\end{tikzpicture}
\end{center}
Our path can now be equivalently stated as:
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,19.8)  {$\ap{G}{q} \ct \refl{}$};
\node (N1) at (0,18.15) {$\ap{G}{q}$};
\node (N2) at (0,16.5)  {$\ap{G}{q} \ct \Big(\opp{\ap{G}{\ap{f}{\lloop}}} \ct \ap{G}{\ap{f}{\lloop}}\Big)$};
\node (N3) at (0,14.85) {$\Big(\ap{G}{q} \ct \opp{\ap{G}{\ap{f}{\lloop}}}\Big) \ct \ap{G}{\ap{f}{\lloop}}$};
\node (N4) at (0,13.2)  {$\Big(\ap{G}{q} \ct \opp{\ap{G}{\ap{f}{\lloop}}}\Big) \ct \pairpath(\refl{},\lloop)$};
\node[red] (N5) at (0,11.55) {$\Big(\ap{G}{q} \ct \pairpath(\refl{},\lloop)\Big) \ct \pairpath(\refl{},\lloop)$};
\node[red] (N6) at (0,9.8)   {$\Big(\pairpath(\lloop,\refl{}) \ct \pairpath(\refl{},\lloop)\Big) \ct \pairpath(\refl{},\lloop)$};
\node (N7) at (0,8.25)  {$\Big(\opp{\pairpath(\refl{},\lloop)}\ct\pairpath(\lloop,\refl{})\Big)\ct \pairpath(\refl{},\lloop)$};
\node (N8) at (0,6.6)   {$\opp{\pairpath(\refl{},\lloop)}\ct\Big(\pairpath(\lloop,\refl{})\ct \pairpath(\refl{},\lloop)\Big)$};
\node (N9) at (0,4.95)  {$\opp{\pairpath(\refl{},\lloop)}\ct\Big(\pairpath(\refl{},\lloop)\ct\pairpath(\lloop,\refl{})\Big)$};
\node (N10) at (0,3.3)  {$\Big(\opp{\pairpath(\refl{},\lloop)}\ct\pairpath(\refl{},\lloop)\Big)\ct\pairpath(\lloop,\refl{})$};
\node (N11) at (0,1.65) {$\pairpath(\lloop,\refl{})$};
\node (N12) at (0,0) {$\refl{}\ct\pairpath(\lloop,\refl{})$};
\draw[-] (N0) -- node[right]{\footnotesize} (N1);
\draw[-] (N1) -- node[right]{\footnotesize} (N2);
\draw[-] (N2) -- node[right]{\footnotesize} (N3);
\draw[-] (N3) -- node[right]{\footnotesize via $\beta_f$, $\beta_G$} (N4);
\draw[red,-] (N4) -- node[right]{\footnotesize via $\beta_f$, $\beta_G$} (N5);
\draw[red,-] (N5) -- node[right]{\footnotesize via $\gamma_G$} (N6);
\draw[red,-] (N6) -- node[right]{\footnotesize via $\II(\Phi_{\lloop,\lloop})$} (N7);
\draw[-] (N7) -- node[right]{\footnotesize} (N8);
\draw[-] (N8) -- node[right]{\footnotesize via $\Phi^{-1}_{\lloop,\lloop}$} (N9);
\draw[-] (N9) -- node[right]{\footnotesize} (N10);
\draw[-] (N10) -- node[right]{\footnotesize} (N11);
\draw[-] (N11) -- node[right]{\footnotesize} (N12);
\end{tikzpicture}
\end{center}
which is equal to:
\begin{center}
\begin{tikzpicture}
\node (N1) at (0,18.15)  {$\ap{G}{q} \ct \refl{}$};
\node (N2) at (0,16.5)   {$\ap{G}{q}$};
\node[red] (N3) at (0,14.85)  {$\pairpath(\lloop,\refl{})$};
\node[red] (N4) at (0,13.2) {$\pairpath(\lloop,\refl{}) \ct \Big(\opp{\pairpath(\refl{},\lloop)} \ct \pairpath(\refl{},\lloop)\Big)$};
\node (N5) at (0,11.5)  {$\Big(\pairpath(\lloop,\refl{}) \ct \opp{\pairpath(\refl{},\lloop)}\Big) \ct \pairpath(\refl{},\lloop)$};
\node (N6) at (0,9.8)   {$\Big(\opp{\pairpath(\refl{},\lloop)}\ct\pairpath(\lloop,\refl{})\Big) \ct \pairpath(\refl{},\lloop)$};
\node (N8) at (0,8.25)   {$\opp{\pairpath(\refl{},\lloop)}\ct\Big(\pairpath(\lloop,\refl{})\ct \pairpath(\refl{},\lloop)\Big)$};
\node (N9) at (0,6.6)  {$\opp{\pairpath(\refl{},\lloop)}\ct\Big(\pairpath(\refl{},\lloop)\ct\pairpath(\lloop,\refl{})\Big)$};
\node (N10) at (0,4.95)  {$\Big(\opp{\pairpath(\refl{},\lloop)}\ct\pairpath(\refl{},\lloop)\Big)\ct\pairpath(\lloop,\refl{})$};
\node (N11) at (0,3.3) {$\pairpath(\lloop,\refl{})$};
\node (N12) at (0,1.65) {$\refl{}\ct\pairpath(\lloop,\refl{})$};
\draw[-] (N1) -- node[right]{\footnotesize} (N2);
\draw[red,-] (N2) -- node[right]{\footnotesize via $\gamma_G$} (N3);
\draw[red,-] (N3) -- node[right]{\footnotesize} (N4);
\draw[red,-] (N4) -- node[right]{\footnotesize} (N5);
\draw[-] (N5) -- node[right]{\footnotesize via $\II(\Phi_{\lloop,\lloop})$} (N6);
\draw[-] (N6) -- node[right]{\footnotesize} (N8);
\draw[-] (N8) -- node[right]{\footnotesize via $\Phi^{-1}_{\lloop,\lloop}$} (N9);
\draw[-] (N9) -- node[right]{\footnotesize} (N10);
\draw[-] (N10) -- node[right]{\footnotesize} (N11);
\draw[-] (N11) -- node[right]{\footnotesize} (N12);
\end{tikzpicture}
\end{center}
We now make the following observation:
\begin{itemize}
\item For any paths $u :a =_A b$, $v: b =_A d$, $w: a =_A c$, $z: c =_A d$ and $\phi : u \ct v = w \ct z$, the path
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,9) {$v$};
\node (N1) at (0,7.5) {$v \ct (\opp{z}\ct z)$};
\node (N2) at (0,6) {$(v \ct \opp{z})\ct z$};
\node (N3) at (0,4.5) {$(\opp{u}\ct w) \ct z$};
\node (N4) at (0,3) {$\opp{u}\ct(w \ct z)$};
\node (N5) at (0,1.5) {$\opp{u}\ct(u \ct v)$};
\node (N6) at (0,0) {$(\opp{u}\ct u) \ct v$};
\node (N7) at (0,-1.5) {$v$};
\draw[-] (N0) -- node[right]{\footnotesize} (N1);
\draw[-] (N1) -- node[right]{\footnotesize} (N2);
\draw[-] (N2) -- node[right]{\footnotesize via $\II(\phi)$} (N3);
\draw[-] (N3) -- node[right]{\footnotesize} (N4);
\draw[-] (N4) -- node[right]{\footnotesize $\opp{\phi}$} (N5);
\draw[-] (N5) -- node[right]{\footnotesize} (N6);
\draw[-] (N6) -- node[right]{\footnotesize} (N7);
\end{tikzpicture}
\end{center}
is equal to the identity path at $v$. This follows by path induction on $u$ and $z$.
\end{itemize}
Using the above observation, we can express our path simply as
\begin{center}
\begin{tikzpicture}
\node (N1) at (0,18.15)  {$\ap{G}{q} \ct \refl{}$};
\node (N2) at (0,16.5)   {$\ap{G}{q}$};
\node (N3) at (0,14.85)  {$\pairpath(\lloop,\refl{})$};
\node (N12) at (0,13.2) {$\refl{}\ct\pairpath(\lloop,\refl{})$};
\draw[-] (N1) -- node[right]{\footnotesize} (N2);
\draw[-] (N2) -- node[right]{\footnotesize via $\gamma_G$} (N3);
\draw[-] (N3) -- node[right]{\footnotesize} (N12);
\end{tikzpicture}
\end{center}
which is precisely $\eta$.

\paragraph*{Right-to-left}
We need to show that for any $x:T^2$ we have $F^\times(G(t)) = t$. We use torus induction, with $b' \defeq \refl{b}$. We let $p'$ be the path
\begin{center}
\begin{tikzpicture}
\node (N1) at (0,9.9)  {$\transfib{z \mapsto F^\times(G(z))=z}{p}{\refl{}}$};
\node (N2) at (0,8.25) {$\opp{\ap{F^\times}{\ap{G}{p}}} \ct \refl{} \ct p$};
\node (N3) at (0,6.6) {$\refl{}$};
\draw[-] (N1) -- node[right]{\footnotesize $\TT{p}{\refl{}}$} (N2);
\draw[-] (N2) -- node[right]{\footnotesize $\zeta_p$} (N3);
\end{tikzpicture}
\end{center}
where for any $\alpha : x =_{T^2} y$ and $u : F^\times(G(x))=x$, the path \[\TT{\alpha}{u} : \transfib{z \mapsto F^\times(G(z))=z}{\alpha}{u} = \opp{\ap{F^\times}{\ap{G}{\alpha}}} \ct u \ct \alpha \]
is defined by path induction on $\alpha$ and $\zeta_p$ is the path
\begin{center}
\begin{tikzpicture}
\node (N2) at (0,8.25) {$\opp{\ap{F^\times}{\ap{G}{p}}} \ct \refl{} \ct p$};
\node (N3) at (0,6.6)  {$\opp{\ap{F^\times}{\ap{G}{p}}} \ct p$};
\node (N4) at (0,4.95) {$\opp{\ap{F^\times}{\pairpath(\refl{},\lloop)}} \ct p$};
\node (N5) at (0,3.3)  {$\opp{\ap{f}{\lloop}} \ct p$};
\node (N6) at (0,1.65) {$\opp{p} \ct p$};
\node (N7) at (0,0) {$\refl{}$};
\draw[-] (N2) -- node[right]{\footnotesize} (N3);
\draw[-] (N3) -- node[right]{\footnotesize via $\beta_G$} (N4);
\draw[-] (N4) -- node[right]{\footnotesize via $\mu(\lloop)$} (N5);
\draw[-] (N5) -- node[right]{\footnotesize via $\beta_f$} (N6);
\draw[-] (N6) -- node[right]{\footnotesize} (N7);
\end{tikzpicture}
\end{center}
Similarly, let $q'$ be the path
\begin{center}
\begin{tikzpicture}
\node (N1) at (0,9.9)  {$\transfib{z \mapsto F^\times(G(z))=z}{q}{\refl{}}$};
\node (N2) at (0,8.25) {$\opp{\ap{F^\times}{\ap{G}{q}}} \ct \refl{} \ct q$};
\node (N3) at (0,6.6)   {$\refl{}$};
\draw[-] (N1) -- node[right]{\footnotesize $\TT{q}{\refl{}}$} (N2);
\draw[-] (N2) -- node[right]{\footnotesize $\zeta_q$} (N3);
\end{tikzpicture}
\end{center}
where $\zeta_q$ is the path
\begin{center}
\begin{tikzpicture}
\node (N2) at (0,8.25) {$\opp{\ap{F^\times}{\ap{G}{q}}} \ct \refl{} \ct q$};
\node (N3) at (0,6.6)  {$\opp{\ap{F^\times}{\ap{G}{q}}} \ct q$};
\node (N4) at (0,4.95) {$\opp{\ap{F^\times}{\pairpath(\lloop,\refl{})}} \ct q$};
\node (N5) at (0,3.3)  {$\opp{\happly_{\ap{F^\to}{\lloop}}(\base)} \ct q$};
\node (N6) at (0,1.65) {$\opp{\happly_{\funext(H)}(\base)} \ct q$};
\node (N7) at (0,0)    {$\opp{q} \ct q$};
\node (N8) at (0,-1.65)   {$\refl{}$};
\draw[-] (N2) -- node[right]{\footnotesize} (N3);
\draw[-] (N3) -- node[right]{\footnotesize via $\gamma_G$} (N4);
\draw[-] (N4) -- node[right]{\footnotesize via $\nu(\lloop)$} (N5);
\draw[-] (N5) -- node[right]{\footnotesize via $\beta_{F^\to}$} (N6);
\draw[-] (N6) -- node[right]{\footnotesize via $\hapfuneq(H)$} (N7);
\draw[-] (N7) -- node[right]{\footnotesize} (N8);
\end{tikzpicture}
\end{center}
All that remains now is to show that the following diagram commutes:
\begin{center}
\begin{tikzpicture}
\node (N1) at (0,9.9)  {\footnotesize $\transfib{z \mapsto F^\times(G(z))=z}{p \ct q}{\refl{}}$};
\node (N2) at (0,8.25) {\footnotesize $\transfib{z \mapsto F^\times(G(z))=z}{q}{\transfib{z \mapsto F^\times(G(z))=z}{p}{\refl{}}}$\;\;\;\;\;};
\node (N3) at (0,6.6)  {\footnotesize $\transfib{z \mapsto F^\times(G(z))=z}{q}{\refl{}}$};
\node (N4) at (4.5,4.95) {$\refl{}$};

\node (N5) at (8,9.9)  {\footnotesize $\transfib{z \mapsto F^\times(G(z))=z}{q \ct p}{\refl{}}$};
\node (N6) at (8,8.25) {\footnotesize $\transfib{z \mapsto F^\times(G(z))=z}{p}{\transfib{z \mapsto F^\times(G(z))=z}{q}{\refl{}}}$};
\node (N7) at (8,6.6)  {\footnotesize $\transfib{z \mapsto F^\times(G(z))=z}{p}{\refl{}}$};

\draw[-] (N1) -- node[above]{\footnotesize via $t$} (N5);
\draw[-] (N1) -- node[right]{\footnotesize} (N2);
\draw[-] (N2) -- node[right]{\footnotesize via $p'$} (N3);
\draw[-] (N3) -- node[below]{\footnotesize $q'$} (N4);
\draw[-] (N5) -- node[right]{\footnotesize} (N6);
\draw[-] (N6) -- node[right]{\footnotesize via $q'$} (N7);
\draw[-] (N7) -- node[below]{\footnotesize $p'$} (N4);
\end{tikzpicture}
\end{center}
We make the following observation:
\begin{itemize}
\item For any $\alpha : x =_{T^2} y$, $\alpha' : y =_{T^2} z$, $u_x : F^\times(G(x))=x$, $u_y : F^\times(G(y))=y$, $u_z : F^\times(G(z))=z$, and $\eta_y : \opp{\ap{F^\times}{\ap{G}{\alpha}}} \ct u_x \ct \alpha = u_y$, $\eta_z : \opp{\ap{F^\times}{\ap{G}{\alpha'}}} \ct u_y \ct \alpha' = u_z$, the path
\begin{center}
\begin{tikzpicture}
\node (N1) at (0,9.9)  {$\transfib{z \mapsto F^\times(G(z))=z}{\alpha \ct \alpha'}{u_x}$};
\node (N2) at (0,8.25) {$\transfib{z \mapsto F^\times(G(z))=z}{\alpha'}{\transfib{z \mapsto F^\times(G(z))=z}{\alpha}{u_x}}$};
\node (N3) at (0,6.6)  {$\transfib{z \mapsto F^\times(G(z))=z}{\alpha'}{\opp{\ap{F^\times}{\ap{G}{\alpha}}} \ct u_x \ct \alpha}$};
\node (N4) at (0,4.95) {$\transfib{z \mapsto F^\times(G(z))=z}{\alpha'}{u_y}$};
\node (N5) at (0,3.3) {$\opp{\ap{F^\times}{\ap{G}{\alpha'}}} \ct u_y \ct \alpha'$};
\node (N6) at (0,1.65) {$u_z$};

\draw[-] (N1) -- node[right]{\footnotesize} (N2);
\draw[-] (N2) -- node[right]{\footnotesize via $\TT{\alpha}{u_x}$} (N3);
\draw[-] (N3) -- node[right]{\footnotesize via $\eta_y$} (N4);
\draw[-] (N4) -- node[right]{\footnotesize $\TT{\alpha'}{u_y}$} (N5);
\draw[-] (N5) -- node[right]{\footnotesize $\eta_z$} (N6);
\end{tikzpicture}
\end{center}
can be equivalently expressed as the path
\begin{center}
\begin{tikzpicture}
\node (N1) at (0,9.9)  {$\transfib{z \mapsto F^\times(G(z))=z}{\alpha \ct \alpha'}{u_x}$};
\node (N2) at (0,8.25) {$\opp{\ap{F^\times}{\ap{G}{\alpha \ct \alpha'}}} \ct u_x \ct (\alpha \ct \alpha')$};
\node (N3) at (0,6.6)  {$\opp{\ap{F^\times}{\ap{G}{\alpha'}}} \ct \Big(\opp{\ap{F^\times}{\ap{G}{\alpha}}} \ct u_x \ct \alpha\Big) \ct \alpha'$};
\node (N4) at (0,4.95) {$\opp{\ap{F^\times}{\ap{G}{\alpha'}}} \ct u_y \ct \alpha'$};
\node (N5) at (0,3.3) {$u_z$};

\draw[-] (N1) -- node[right]{\footnotesize $\TT{\alpha \ct \alpha'}{u_x}$} (N2);
\draw[-] (N2) -- node[right]{\footnotesize} (N3);
\draw[-] (N3) -- node[right]{\footnotesize via $\eta_y$} (N4);
\draw[-] (N4) -- node[right]{\footnotesize $\eta_z$} (N5);
\end{tikzpicture}
\end{center}
To prove this, it suffices to show that the outer rectangle in the diagram below commutes:
\begin{center}
\begin{tikzpicture}
\node (Na) at (4.5,8.25) {A};
\node (Nb) at (4.5,5.575) {B};
\node (N1) at (0,9.9)  {\scriptsize $\transfib{z \mapsto F^\times(G(z))=z}{\alpha \ct \alpha'}{u_x}$};
\node (N2) at (0,8.25) {\scriptsize $\transfib{z \mapsto F^\times(G(z))=z}{\alpha'}{\transfib{z \mapsto F^\times(G(z))=z}{\alpha}{u_x}}$};
\node (N3) at (0,6.6)  {\scriptsize $\transfib{z \mapsto F^\times(G(z))=z}{\alpha'}{\opp{\ap{F^\times}{\ap{G}{\alpha}}} \ct u_x \ct \alpha}$};
\node (N4) at (0,4.95) {\scriptsize $\transfib{z \mapsto F^\times(G(z))=z}{\alpha'}{u_y}$};
\node (N5) at (9,4.95) {\scriptsize $\opp{\ap{F^\times}{\ap{G}{\alpha'}}} \ct u_y \ct \alpha'$};

\node (N7) at (9,9.9) {\scriptsize $\opp{\ap{F^\times}{\ap{G}{\alpha \ct \alpha'}}} \ct u_x \ct (\alpha \ct \alpha')$};
\node (N8) at (9,6.6) {\scriptsize $\opp{\ap{F^\times}{\ap{G}{\alpha'}}} \ct \Big(\opp{\ap{F^\times}{\ap{G}{\alpha}}} \ct u_x \ct \alpha\Big) \ct \alpha'$};
\draw[-] (N1) -- node[right]{\footnotesize} (N2);
\draw[-] (N2) -- node[right]{\scriptsize via $\TT{\alpha}{u_x}$} (N3);
\draw[-] (N3) -- node[right]{\footnotesize via $\eta_y$} (N4);
\draw[-] (N4) -- node[below]{\scriptsize $\TT{\alpha'}{u_y}$} (N5);
\draw[-] (N1) -- node[above]{\scriptsize $\TT{\alpha \ct \alpha'}{u_x}$} (N7);
\draw[-] (N7) -- node[right]{\footnotesize} (N8);
\draw[-] (N3) -- node[below]{\scriptsize $\TT{\alpha'}{\opp{\ap{F^\times}{\ap{G}{\alpha}}} \ct u_x \ct \alpha}$} (N8);
\draw[-] (N8) -- node[right]{\footnotesize  via $\eta_y$} (N5);
\end{tikzpicture}
\end{center}
Both of the rectangles A and B are easily shown to commute by a suitable path induction.
\end{itemize}
Using the above observation, it suffices to show that the outer part of the following diagram commutes:
\begin{center}
\begin{tikzpicture}
\node (Na) at (5,9.075) {A};
\node (Nb) at (5,6.6) {B};
\node (N1) at (0,9.9)  {\scriptsize $\transfib{z \mapsto F^\times(G(z))=z}{p \ct q}{\refl{}}$};
\node (N2) at (0,8.25) {\scriptsize $\opp{\ap{F^\times}{\ap{G}{p \ct q}}} \ct \refl{} \ct (p \ct q)$};
\node (N3) at (0,6.6)  {\scriptsize $\opp{\ap{F^\times}{\ap{G}{q}}} \ct \Big(\opp{\ap{F^\times}{\ap{G}{p}}} \ct \refl{} \ct p\Big) \ct q$};
\node (N4) at (0,4.95) {\scriptsize $\opp{\ap{F^\times}{\ap{G}{q}}} \ct \refl{} \ct q$};
\node (N5) at (5,3.3) {\scriptsize $\refl{}$};

\node (N6) at (10,9.9)  {\scriptsize $\transfib{z \mapsto F^\times(G(z))=z}{q \ct p}{\refl{}}$};
\node (N7) at (10,8.25) {\scriptsize $\opp{\ap{F^\times}{\ap{G}{q \ct p}}} \ct \refl{} \ct (q \ct p)$};
\node (N8) at (10,6.6)  {\scriptsize $\opp{\ap{F^\times}{\ap{G}{p}}} \ct \Big(\opp{\ap{F^\times}{\ap{G}{q}}} \ct \refl{} \ct q\Big) \ct p$};
\node (N9) at (10,4.95) {\scriptsize $\opp{\ap{F^\times}{\ap{G}{p}}} \ct \refl{} \ct q$};

\node (N10) at (5,8.25) {\scriptsize $\opp{\ap{F^\times}{\ap{G}{q \ct p}}} \ct \refl{} \ct (p \ct q)$};

\draw[-] (N1) -- node[above]{\scriptsize via $t$} (N6);
\draw[-] (N1) -- node[right]{\scriptsize $\TT{p \ct q}{\refl{}}$} (N2);
\draw[-] (N2) -- node[right]{\scriptsize} (N3);
\draw[-] (N3) -- node[right]{\scriptsize via $\zeta_p$} (N4);
\draw[-] (N4) -- node[below]{\scriptsize $\zeta_q$} (N5);
\draw[-] (N6) -- node[right]{\scriptsize $\TT{q \ct p}{\refl{}}$} (N7);
\draw[-] (N7) -- node[below]{\footnotesize} (N8);
\draw[-] (N8) -- node[right]{\scriptsize via $\zeta_q$} (N9);
\draw[-] (N9) -- node[below]{\scriptsize $\zeta_p$} (N5);
\draw[-] (N2) -- node[below]{\scriptsize via $t$} (N10);
\draw[-] (N10) -- node[below]{\scriptsize via $t$} (N7);
\end{tikzpicture}
\end{center}
Since rectangle A clearly commutes, it suffices to prove that part B commutes.

We can equivalently express diagram B as
\begin{center}
\begin{tikzpicture}
\node (N2) at (0,8.25) {\scriptsize $\opp{\ap{F^\times}{\ap{G}{p \ct q}}} \ct \refl{} \ct (p \ct q)$};
\node[red] (N2a) at (0,6.6) {\scriptsize $\opp{\Big(\ap{F^\times}{\ap{G}{p}} \ct \ap{F^\times}{\ap{G}{q}}\Big)} \ct \refl{} \ct (p \ct q)$};
\node (N3) at (0,4.95)  {\scriptsize $\opp{\ap{F^\times}{\ap{G}{q}}} \ct \Big(\opp{\ap{F^\times}{\ap{G}{p}}} \ct \refl{} \ct p\Big) \ct q$};
\node (N4) at (0,3.3) {\scriptsize $\opp{\ap{F^\times}{\ap{G}{q}}} \ct \refl{} \ct q$};
\node (N5) at (5,1.65) {\scriptsize $\refl{}$};

\node (N7) at (10,8.25) {\scriptsize $\opp{\ap{F^\times}{\ap{G}{q \ct p}}} \ct \refl{} \ct (q \ct p)$};
\node[red] (N7a) at (10,6.6) {\scriptsize $\opp{\Big(\ap{F^\times}{\ap{G}{q}} \ct \ap{F^\times}{\ap{G}{p}}\Big)} \ct \refl{} \ct (q \ct p)$};
\node (N8) at (10,4.95)  {\scriptsize $\opp{\ap{F^\times}{\ap{G}{p}}} \ct \Big(\opp{\ap{F^\times}{\ap{G}{q}}} \ct \refl{} \ct q\Big) \ct p$};
\node (N9) at (10,3.3) {\scriptsize $\opp{\ap{F^\times}{\ap{G}{p}}} \ct \refl{} \ct q$};

\node (N10) at (5,8.25) {\scriptsize $\opp{\ap{F^\times}{\ap{G}{q \ct p}}} \ct \refl{} \ct (p \ct q)$};

\draw[red,-] (N2) -- node[right]{\scriptsize} (N2a);
\draw[red,-] (N2a) -- node[right]{\scriptsize} (N3);
\draw[-] (N3) -- node[right]{\scriptsize via $\zeta_p$} (N4);
\draw[-] (N4) -- node[below]{\scriptsize $\zeta_q$} (N5);
\draw[red,-] (N7) -- node[below]{\footnotesize} (N7a);
\draw[red,-] (N7a) -- node[below]{\footnotesize} (N8);
\draw[-] (N8) -- node[right]{\scriptsize via $\zeta_q$} (N9);
\draw[-] (N9) -- node[below]{\scriptsize $\zeta_p$} (N5);
\draw[-] (N2) -- node[below]{\scriptsize via $t$} (N10);
\draw[-] (N10) -- node[below]{\scriptsize via $t$} (N7);
\end{tikzpicture}
\end{center}
We make the following observation:
\begin{itemize}
\item For any $\alpha_u : u_1 =_{a =_A b} u_2$, $\alpha_v : v_1 =_{b =_A c} v_2$, the path
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,9) {$\opp{(u_1 \ct v_1)} \ct \refl{} \ct (u_2 \ct v_2)$};
\node (N1) at (0,7.5) {$v^{-1}_1 \ct (u^{-1}_1 \ct \refl{} \ct u_2) \ct v_2$};
\node (N2) at (0,6) {$v^{-1}_1 \ct (u^{-1}_1 \ct u_2) \ct v_2$};
\node (N3) at (0,4.5) {$v^{-1}_1 \ct (u^{-1}_2 \ct u_2) \ct v_2$};
\node (N4) at (0,3) {$v^{-1}_1 \ct \refl{} \ct v_2$};
\node (N5) at (0,1.5) {$v^{-1}_1 \ct v_2$};
\node (N6) at (0,0) {$v^{-1}_2 \ct v_2$};
\node (N7) at (0,-1.5) {$\refl{}$};

\draw[-] (N0) -- node[right]{} (N1);
\draw[-] (N1) -- node[right]{} (N2);
\draw[-] (N2) -- node[right]{\footnotesize via $\alpha_u$} (N3);
\draw[-] (N3) -- node[right]{} (N4);
\draw[-] (N4) -- node[right]{} (N5);
\draw[-] (N5) -- node[right]{\footnotesize via $\alpha_v$} (N6);
\draw[-] (N6) -- node[right]{} (N7);
\end{tikzpicture}
\end{center}
is equivalent to the path
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,9) {$\opp{(u_1 \ct v_1)} \ct \refl{} \ct (u_2 \ct v_2)$};
\node (N1) at (0,7.5) {$\opp{(u_2 \ct v_1)} \ct \refl{} \ct (u_2 \ct v_2)$};
\node (N2) at (0,6) {$\opp{(u_2 \ct v_2)} \ct \refl{} \ct (u_2 \ct v_2)$};
\node (N3) at (0,4.5) {$\opp{(u_2 \ct v_2)} \ct (u_2 \ct v_2)$};
\node (N4) at (0,3) {$\refl{}$};

\draw[-] (N0) -- node[right]{\footnotesize via $\alpha_u$} (N1);
\draw[-] (N1) -- node[right]{\footnotesize via $\alpha_v$} (N2);
\draw[-] (N2) -- node[right]{} (N3);
\draw[-] (N3) -- node[right]{} (N4);
\end{tikzpicture}
\end{center}
This is clear by path induction.
\end{itemize}
Using this observation, it suffices to show that the outer part of the following diagram commutes:
\begin{center}
\begin{tikzpicture}
\node (Na) at (5,7) {A};
\node (Nb) at (5,1.65) {B};
\node (N2) at (0,8.25) {\scriptsize $\opp{\ap{F^\times}{\ap{G}{p \ct q}}} \ct \refl{} \ct (p \ct q)$};
\node (N2a) at (0,6.6) {\scriptsize $\opp{\Big(\ap{F^\times}{\ap{G}{p}} \ct \ap{F^\times}{\ap{G}{q}}\Big)} \ct \refl{} \ct (p \ct q)$};
\node[red] (N3) at (0,4.95) {\scriptsize $\opp{\Big(p \ct \ap{F^\times}{\ap{G}{q}}\Big)} \ct \refl{} \ct (p \ct q)$};
\node[red] (N4) at (0,3.3) {\scriptsize $\opp{(p \ct q)} \ct \refl{} \ct (p \ct q)$};
\node[red] (N5) at (0,1.65)  {\scriptsize $\opp{(p \ct q)} \ct (p \ct q)$};
\node (N6) at (5,0) {\scriptsize $\refl{}$};
\node (N7) at (10,8.25) {\scriptsize $\opp{\ap{F^\times}{\ap{G}{q \ct p}}} \ct \refl{} \ct (q \ct p)$};
\node (N7a) at (10,6.6) {\scriptsize $\opp{\Big(\ap{F^\times}{\ap{G}{q}} \ct \ap{F^\times}{\ap{G}{p}}\Big)} \ct \refl{} \ct (q \ct p)$};
\node[red] (N8) at (10,4.95)  {\scriptsize $\opp{\Big(q \ct \ap{F^\times}{\ap{G}{p}}\Big)} \ct \refl{} \ct (q \ct p)$};
\node[red] (N9) at (10,3.3)  {\scriptsize $\opp{(q \ct p)} \ct \refl{} \ct (q \ct p)$};
\node[red] (N11) at (10,1.65) {\scriptsize $\opp{(q \ct p)} \ct (q \ct p)$};
\node (N10) at (5,8.25) {\scriptsize $\opp{\ap{F^\times}{\ap{G}{q \ct p}}} \ct \refl{} \ct (p \ct q)$};
\node[red] (N12) at (5,3.3) {\scriptsize $\opp{(q \ct p)} \ct \refl{} \ct (p \ct q)$};

\draw[-] (N2) -- node[right]{\scriptsize} (N2a);
\draw[red,-] (N2a) -- node[right]{\scriptsize via $\beta_G$, $\mu(\lloop)$, $\beta_f$} (N3);
\draw[red,-] (N3) -- node[right]{\scriptsize via $\gamma_G$, $\nu(\lloop)$, $\beta_{F^\to}$, $\hapfuneq(H)$} (N4);
\draw[red,-] (N4) -- node[right]{\scriptsize} (N5);
\draw[red,-] (N5) -- node[below]{\scriptsize} (N6);

\draw[-] (N7) -- node[below]{\footnotesize} (N7a);
\draw[red,-] (N7a) -- node[left]{\scriptsize via $\gamma_G$, $\nu(\lloop)$, $\beta_{F^\to}$, $\hapfuneq(H)$} (N8);
\draw[red,-] (N8) -- node[left]{\scriptsize via $\beta_G$, $\mu(\lloop)$, $\beta_f$} (N9);
\draw[red,-] (N9) -- node[right]{\scriptsize} (N11);
\draw[red,-] (N11) -- node[below]{\scriptsize} (N6);
\draw[-] (N2) -- node[below]{\scriptsize via $t$} (N10);
\draw[-] (N10) -- node[below]{\scriptsize via $t$} (N7);

\draw[red,-] (N4) -- node[below]{\scriptsize via $t$} (N12);
\draw[red,-] (N12) -- node[below]{\scriptsize via $t$} (N9);
\end{tikzpicture}
\end{center}
Part B clearly commutes. This leaves us to show that part A commutes. We now make the following observation:
\begin{itemize}
\item For any 2-paths $\alpha^1_u : u_1 =_{a =_A b} u_2$, $\alpha_u^2 : u_1 =_{a =_A b} u_3$, $\alpha_u^3 : u_3 =_{a =_A b} u_4$, $\alpha_u^4 : u_2 =_{a =_A b} u_4$, $\alpha_v : v_1 =_{c =_A d} v_2$ and path $w : b=_A c$ such that
\begin{center}
\begin{tikzpicture}
\node (Na) at (1,0.75) {=};
\node (N0) at (0,1.5) {$u_1$};
\node (N1) at (0,0) {$u_2$};
\node (N2) at (2,1.5) {$u_3$};
\node (N3) at (2,0) {$u_4$};

\draw[-] (N0) -- node[left]{\footnotesize $\alpha^1_u$} (N1);
\draw[-] (N0) -- node[above]{\footnotesize $\alpha^2_u$} (N2);
\draw[-] (N1) -- node[below]{\footnotesize $\alpha^4_u$} (N3);
\draw[-] (N2) -- node[right]{\footnotesize $\alpha^3_u$} (N3);
\end{tikzpicture}
\end{center}
the following diagram commutes:
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,1.5) {$u^{-1}_1 \ct w \ct v_1$};
\node (N1) at (0,0) {$u^{-1}_2 \ct w \ct v_1$};
\node (N2) at (4,1.5) {$u^{-1}_3 \ct w \ct v_1$};
\node (N3) at (4,0) {$u^{-1}_4 \ct w \ct v_1$};
\node (N4) at (8,1.5) {$u^{-1}_3 \ct w \ct v_2$};
\node (N5) at (8,0) {$u^{-1}_4 \ct w \ct v_2$};

\draw[-] (N0) -- node[left]{\footnotesize via $\alpha^1_u$} (N1);
\draw[-] (N0) -- node[above]{\footnotesize via $\alpha^2_u$} (N2);
\draw[-] (N1) -- node[below]{\footnotesize via $\alpha^4_u$} (N3);
\draw[-] (N2) -- node[above]{\footnotesize via $\alpha_v$} (N4);
\draw[-] (N3) -- node[below]{\footnotesize via $\alpha_v$} (N5);
\draw[-] (N4) -- node[right]{\footnotesize via $\alpha^3_u$} (N5);
\end{tikzpicture}
\end{center}
This is clear by path induction on $\alpha_v$, $\alpha_u^2$, $\alpha_u^4$.
\end{itemize}
Using this observation, it suffices to show that the following diagram commutes:
\begin{center}
\begin{tikzpicture}
\node (N2) at (0,8.25) {$\ap{F^\times}{\ap{G}{p \ct q}}$};
\node (N2a) at (0,6.6) {$\ap{F^\times}{\ap{G}{p}} \ct \ap{F^\times}{\ap{G}{q}}$};
\node (N3) at (0,4.95) {$p \ct \ap{F^\times}{\ap{G}{q}}$};
\node (N4) at (0,3.3) {$p \ct q$};

\node (N7) at (10,8.25) {$\ap{F^\times}{\ap{G}{q \ct p}}$};
\node (N7a) at (10,6.6) {$\ap{F^\times}{\ap{G}{q}} \ct \ap{F^\times}{\ap{G}{p}}$};
\node (N8) at (10,4.95) {$q \ct \ap{F^\times}{\ap{G}{p}}$};
\node (N9) at (10,3.3)  {$q \ct p$};

\draw[-] (N2) -- node[right]{\footnotesize} (N2a);
\draw[-] (N2a) -- node[right]{\footnotesize via $\beta_G$, $\mu(\lloop)$, $\beta_f$} (N3);
\draw[-] (N3) -- node[right]{\footnotesize via $\gamma_G$, $\nu(\lloop)$, $\beta_{F^\to}$, $\hapfuneq(H)$} (N4);
\draw[-] (N7) -- node[below]{\footnotesize} (N7a);
\draw[-] (N7a) -- node[left]{\footnotesize via $\gamma_G$, $\nu(\lloop)$, $\beta_{F^\to}$, $\hapfuneq(H)$} (N8);
\draw[-] (N8) -- node[left]{\footnotesize via $\beta_G$, $\mu(\lloop)$, $\beta_f$} (N9);
\draw[-] (N2) -- node[above]{\footnotesize via $t$} (N7);
\draw[-] (N4) -- node[below]{\footnotesize via $t$} (N9);
\end{tikzpicture}
\end{center}
After some rearranging we get:
\begin{center}
\begin{tikzpicture}
\node (N1) at (0,9.9) {\footnotesize $\ap{F^\times}{\ap{G}{p \ct q}}$};
\node[red] (N2) at (0,8.25) {\footnotesize $\ap{F^\times}{\ap{G}{p} \ct \ap{G}{q}}$};
\node[red] (N3) at (0,6.6) {\footnotesize $\ap{F^\times}{\ap{G}{p}} \ct \ap{F^\times}{\ap{G}{q}}$};
\node[red] (N4) at (0,4.95) {\footnotesize $\ap{F^\times}{\pairpath(\refl{},\lloop)} \ct \ap{F^\times}{\pairpath(\lloop,\refl{})}$};
\node[red] (N5) at (0,3.3) {\footnotesize $\ap{f}{\lloop} \ct \happly_{\ap{F^\to}{\lloop}}(\base)$};
\node[red] (N6) at (0,1.65) {\footnotesize $\ap{f}{\lloop} \ct q$};
\node (N7) at (0,0)    {\footnotesize $p \ct q$};

\node (N11) at (9,9.9) {\footnotesize $\ap{F^\times}{\ap{G}{q \ct p}}$};
\node[red] (N12) at (9,8.25) {\footnotesize $\ap{F^\times}{\ap{G}{q} \ct \ap{G}{p}}$};
\node[red] (N13) at (9,6.6) {\footnotesize $\ap{F^\times}{\ap{G}{q}} \ct \ap{F^\times}{\ap{G}{p}}$};
\node[red] (N14) at (9,4.95) {\footnotesize $\ap{F^\times}{\pairpath(\lloop,\refl{})} \ct \ap{F^\times}{\pairpath(\refl{},\lloop)}$};
\node[red] (N15) at (9,3.3) {\footnotesize $\happly_{\ap{F^\to}{\lloop}}(\base) \ct \ap{f}{\lloop}$};
\node[red] (N16) at (9,1.65) {\footnotesize $q \ct \ap{f}{\lloop}$};
\node (N17) at (9,0)    {\footnotesize $q \ct p$};

\draw[red,-] (N1) -- node[right]{\scriptsize} (N2);
\draw[red,-] (N2) -- node[right]{\scriptsize} (N3);
\draw[red,-] (N3) -- node[right]{\scriptsize via $\beta_G$, $\gamma_G$} (N4);
\draw[red,-] (N4) -- node[right]{\scriptsize via $\mu(\lloop)$, $\nu(\lloop)$} (N5);
\draw[red,-] (N5) -- node[right]{\scriptsize via $\beta_{F^\to}$, $\hapfuneq(H)$} (N6);
\draw[red,-] (N6) -- node[right]{\scriptsize via $\beta_f$} (N7);
\draw[red,-] (N11) -- node[right]{\scriptsize} (N12);
\draw[red,-] (N12) -- node[right]{\scriptsize} (N13);
\draw[red,-] (N13) -- node[right]{\scriptsize via $\beta_G$, $\gamma_G$} (N14);
\draw[red,-] (N14) -- node[right]{\scriptsize via $\mu(\lloop)$, $\nu(\lloop)$} (N15);
\draw[red,-] (N15) -- node[right]{\scriptsize via $\beta_{F^\to}$, $\hapfuneq(H)$} (N16);
\draw[red,-] (N16) -- node[right]{\scriptsize via $\beta_f$} (N17);
\draw[-] (N1) -- node[above]{\scriptsize via $t$} (N11);
\draw[-] (N7) -- node[below]{\scriptsize via $t$} (N17);
\end{tikzpicture}
\end{center}
or equivalently:
\begin{center}
\begin{tikzpicture}
\node (N1) at (0,9.9) {\footnotesize $\ap{F^\times}{\ap{G}{p \ct q}}$};
\node (N2) at (0,8.25) {\footnotesize $\ap{F^\times}{\ap{G}{p} \ct \ap{G}{q}}$};
\node[red] (N3) at (0,6.6) {\footnotesize $\ap{F^\times}{\pairpath(\refl{},\lloop) \ct \pairpath(\lloop,\refl{})}$};
\node (N4) at (0,4.95) {\footnotesize $\ap{F^\times}{\pairpath(\refl{},\lloop)} \ct \ap{F^\times}{\pairpath(\lloop,\refl{})}$};
\node (N5) at (0,3.3) {\footnotesize $\ap{f}{\lloop} \ct \happly_{\ap{F^\to}{\lloop}}(\base)$};
\node (N6) at (0,1.65) {\footnotesize $\ap{f}{\lloop} \ct q$};
\node (N7) at (0,0)    {\footnotesize $p \ct q$};

\node (N11) at (9,9.9) {\footnotesize $\ap{F^\times}{\ap{G}{q \ct p}}$};
\node (N12) at (9,8.25) {\footnotesize $\ap{F^\times}{\ap{G}{q} \ct \ap{G}{p}}$};
\node[red] (N13) at (9,6.6) {\footnotesize $\ap{F^\times}{\pairpath(\lloop,\refl{}) \ct \pairpath(\refl{},\lloop)}$};
\node (N14) at (9,4.95) {\footnotesize $\ap{F^\times}{\pairpath(\lloop,\refl{})} \ct \ap{F^\times}{\pairpath(\refl{},\lloop)}$};
\node (N15) at (9,3.3) {\footnotesize $\happly_{\ap{F^\to}{\lloop}}(\base) \ct \ap{f}{\lloop}$};
\node (N16) at (9,1.65) {\footnotesize $q \ct \ap{f}{\lloop}$};
\node (N17) at (9,0)    {\footnotesize $q \ct p$};

\draw[-] (N1) -- node[right]{\scriptsize} (N2);
\draw[red,-] (N2) -- node[right]{\scriptsize via $\beta_G$, $\gamma_G$} (N3);
\draw[red,-] (N3) -- node[right]{\scriptsize} (N4);
\draw[-] (N4) -- node[right]{\scriptsize via $\mu(\lloop)$, $\nu(\lloop)$} (N5);
\draw[-] (N5) -- node[right]{\scriptsize via $\beta_{F^\to}$, $\hapfuneq(H)$} (N6);
\draw[-] (N6) -- node[right]{\scriptsize via $\beta_f$} (N7);
\draw[-] (N11) -- node[right]{\scriptsize} (N12);
\draw[red,-] (N12) -- node[right]{\scriptsize  via $\beta_G$, $\gamma_G$} (N13);
\draw[red,-] (N13) -- node[right]{\scriptsize} (N14);
\draw[-] (N14) -- node[right]{\scriptsize via $\mu(\lloop)$, $\nu(\lloop)$} (N15);
\draw[-] (N15) -- node[right]{\scriptsize via $\beta_{F^\to}$, $\hapfuneq(H)$} (N16);
\draw[-] (N16) -- node[right]{\scriptsize via $\beta_f$} (N17);
\draw[-] (N1) -- node[above]{\scriptsize via $t$} (N11);
\draw[-] (N7) -- node[below]{\scriptsize via $t$} (N17);
\end{tikzpicture}
\end{center}
Finally, this diagram can be viewed as follows:
\begin{center}
\begin{tikzpicture}
\node (Na) at (4.5,8.25) {A};
\node (Nb) at (4.5,4.95) {B};
\node (Nc) at (4.5,2.475) {C};
\node (Nd) at (4.5,0.76) {D};
\node (N1) at (0,9.9) {\footnotesize $\ap{F^\times}{\ap{G}{p \ct q}}$};
\node (N2) at (0,8.25) {\footnotesize $\ap{F^\times}{\ap{G}{p} \ct \ap{G}{q}}$};
\node (N3) at (0,6.6) {\footnotesize $\ap{F^\times}{\pairpath(\refl{},\lloop) \ct \pairpath(\lloop,\refl{})}$};
\node (N4) at (0,4.95) {\footnotesize $\ap{F^\times}{\pairpath(\refl{},\lloop)} \ct \ap{F^\times}{\pairpath(\lloop,\refl{})}$};
\node (N5) at (0,3.3) {\footnotesize $\ap{f}{\lloop} \ct \happly_{\ap{F^\to}{\lloop}}(\base)$};
\node (N6) at (0,1.65) {\footnotesize $\ap{f}{\lloop} \ct q$};
\node (N7) at (0,0)    {\footnotesize $p \ct q$};

\node (N11) at (9,9.9) {\footnotesize $\ap{F^\times}{\ap{G}{q \ct p}}$};
\node (N12) at (9,8.25) {\footnotesize $\ap{F^\times}{\ap{G}{q} \ct \ap{G}{p}}$};
\node (N13) at (9,6.6) {\footnotesize $\ap{F^\times}{\pairpath(\lloop,\refl{}) \ct \pairpath(\refl{},\lloop)}$};
\node (N14) at (9,4.95) {\footnotesize $\ap{F^\times}{\pairpath(\lloop,\refl{})} \ct \ap{F^\times}{\pairpath(\refl{},\lloop)}$};
\node (N15) at (9,3.3) {\footnotesize $\happly_{\ap{F^\to}{\lloop}}(\base) \ct \ap{f}{\lloop}$};
\node (N16) at (9,1.65) {\footnotesize $q \ct \ap{f}{\lloop}$};
\node (N17) at (9,0)    {\footnotesize $q \ct p$};

\draw[-] (N1) -- node[right]{\scriptsize} (N2);
\draw[-] (N2) -- node[right]{\scriptsize via $\beta_G$, $\gamma_G$} (N3);
\draw[-] (N3) -- node[right]{\scriptsize} (N4);
\draw[-] (N4) -- node[right]{\scriptsize via $\mu(\lloop)$, $\nu(\lloop)$} (N5);
\draw[-] (N5) -- node[right]{\scriptsize via $\beta_{F^\to}$, $\hapfuneq(H)$} (N6);
\draw[-] (N6) -- node[right]{\scriptsize via $\beta_f$} (N7);
\draw[-] (N11) -- node[right]{\scriptsize} (N12);
\draw[-] (N12) -- node[right]{\scriptsize  via $\beta_G$, $\gamma_G$} (N13);
\draw[-] (N13) -- node[right]{\scriptsize} (N14);
\draw[-] (N14) -- node[right]{\scriptsize via $\mu(\lloop)$, $\nu(\lloop)$} (N15);
\draw[-] (N15) -- node[right]{\scriptsize via $\beta_{F^\to}$, $\hapfuneq(H)$} (N16);
\draw[-] (N16) -- node[right]{\scriptsize via $\beta_f$} (N17);
\draw[-] (N1) -- node[above]{\scriptsize via $t$} (N11);
\draw[-] (N7) -- node[below]{\scriptsize via $t$} (N17);
\draw[-] (N3) -- node[above]{\scriptsize via $\Phi_{\lloop,\lloop}$} (N13);
\draw[-] (N5) -- node[above]{\scriptsize $\nathom{\happly_{\ap{F^\to}{\lloop}}}{\lloop}$} (N15);
\draw[-] (N6) -- node[below]{\scriptsize $\nathom{H}{\lloop}$} (N16);
\end{tikzpicture}
\end{center}
where for any $\alpha : x =_{\Sn^1} y$, the 2-path
\[ \nathom{\happly_{\ap{F^\to}{\lloop}}}{\alpha} : \ap{f}{\alpha} \ct \happly_{\ap{F^\to}{\lloop}}(y) =
\happly_{\ap{F^\to}{\lloop}}(x) \ct \ap{f}{\alpha} \]
is defined by induction on $\alpha$.

Now rectangles A and D commute by diagrams (1) and (2) respectively. Rectangles B and C commute by a suitable path induction. \qed

\subsection*{Solution to \cref{ex:trunc-bool-interval}}

Let's call the given homotopy $p:\prd{x:A}(f(x)=g(x))$.
Since $B$ may not be a mere proposition, we consider the contractible type $\sm{y:B}(f(x)=y)$.
For all $x:A$ we define a function ${q}_x:\bool\to{}\sm{y:B}(f(x)=y)$ by recursion on $\bool$, with:
\begin{align*}
{q}_x(\btrue) &\defeq \pairr{f(x),\refl{f(x)}},\\
{q}_x(\bfalse) &\defeq \pairr{g(x),p(x)}.
\end{align*}
By induction on truncation, since $\sm{y:B}(f(x)=y)$ is a mere proposition, we get $\widetilde{p}_x:\brck \bool\to{}\sm{y:B}(f(x)=y)$ satisfying $\widetilde{p}_x (\bproj b) \equiv {q}_x(b)$ for all $b:B$.
Hence we can define $q:\brck \bool \to(A\to{}B)$ by
\[q(i)\defeq \lam{x} \proj1(\widetilde{p}_x(i))\]
Then we have $q(\bproj\btrue)(x)\jdeq f(x)$ for all $x:A$, and hence $q(\bproj\btrue) \jdeq f$.
Similarly, $q(\bproj\bfalse)\jdeq g$, and hence $\map{q} r : \id[(A\to{}B)]fg$, where $r: \bproj\btrue =_{\brck \bool} \bproj\bfalse$ exists since $\brck\bool$ is a mere proposition.

\section*{Exercises from \cref{cha:hlevels}}

\subsection*{Solution to \cref{ex:ntype-from-nconn-const}}

Let $\modal$ be a modality; it remains to show that if all maps into $B$ out of a $\modal$-connected type are constant, then $B$ is $\modal$-modal.
We show under that hypothesis that $\eta:B\to \modal B$ is an equivalence, by showing that its fibers are contractible.

Since $\eta$ is always $\modal$-connected, its fibers are $\modal$-connected, and thus the inclusion of $\hfib{\eta}{z}$ into $B$ is constant.
Thus, there is an $a:B$ such that for any $b:B$ and $p:\eta b=z$ we have $q(b,p):a=b$.
Then $\apfunc{\eta}(q(b,p))\ct p : \eta a=z$ for any $(b,p):\hfib\eta z$, so we have a map $\hfib\eta z \to (\eta a=z)$.
But $\modal B$ is $\modal$-modal, hence so is $\eta a = z$.
Thus, by \cref{thm:nconn-to-ntype-const}, this map is constant; hence we have $r:\eta a=z$ such that $\apfunc{\eta}(q(b,p))\ct p = r$ for all $(b,p)$.
But using the characterization of paths in fibers, this means exactly that $(b,p)=(a,r)$ for all $(b,p)$; hence $\hfib\eta z$ is contractible with center $(a,r)$.

\subsection*{Solution to \cref{ex:connectivity-inductively}}

If $A$ is $n$-connected, then since $\trunc{-1}A = \trunc{-1}{\trunc{n}A}$, also $A$ is $(-1)$-connected.
And since $\trunc{n-1}{\id[A]ab} = (\id[\trunc n A]{\tproj na}{\tproj nb})$ by \cref{thm:path-truncation} and the path spaces of a contractible type are contractible, each $\id[A]ab$ is $(n-1)$-connected.

Conversely, suppose $A$ is $(-1)$-connected and all its path spaces are $(n-1)$-connected.
Firstly, we claim $\trunc nA$ is a mere proposition, i.e.\ that for all $x,y:\trunc nA$, the type $x=y$ is contractible.
Since contractibility of $x=y$ is a mere proposition, it suffices to assume that $x$ and $y$ are of the form $\tproj na$ and $\tproj nb$ respectively.
But $\id[\trunc n A]{\tproj na}{\tproj nb}$ is contractible by \cref{thm:path-truncation} and the assumption.
Thus, $\trunc nA$ is a mere proposition.
Since it is also $(-1)$-connected by assumption, it is therefore contractible, so $A$ is $n$-connected.


\subsection*{Solution to \cref{ex:lemnm}}

Evidently $\mathsf{LEM}$ is the same as $\mathsf{LEM}_{-1,-1}$, so for the first part it suffices to assume $\mathsf{LEM}$ and prove $\mathsf{LEM}_{n,-1}$ and $\mathsf{LEM}_{-1,m}$ for all $n,m$.
For the latter, note that if $A$ is a mere proposition, then by \cref{ex:lem-mereprop} so is $A+\neg A$, and thus $\trunc m{A+\neg A}= A+\neg A$ for any $m\ge -1$.
For the former, note that assuming LEM, by \cref{ex:lem-brck} we have $\trunc{-1}{B} = \neg\neg B$ for any $B$, while $\neg\neg(A+\neg A)$ is always true for any type $A$ (\cref{ex:not-not-lem}).

For the second part, it suffices to derive a contradiction from $\mathsf{LEM}_{0,0}$; but the proof of \cref{thm:not-lem} already uses an $A$ that is a set (namely $\bool$).

\subsection*{Solution to \cref{ex:acconn}}

Suppose the $(-1)$-connected AC, and by induction suppose also the $n$-connected AC.
Let $X$ be a set and $Y:X\to \type$ a family of $(n+1)$-connected types.
By \cref{ex:connectivity-inductively}, to show that $\prd{x:X} Y(x)$ is $(n+1)$-connected, it suffices to show that it is $(-1)$-connected and that all its path-types are $n$-connected.
But also by \cref{ex:connectivity-inductively}, each $Y(x)$ is $(-1)$-connected and all its path types are $n$-connected.
Applying function extensionality to characterize the path types of $\prd{x:X} Y(x)$, the claim follows from the $(-1)$-connected and $n$-connected axioms of choice.

\subsection*{Solution to \cref{ex:is-conn-trunc-functor}}

We distinguish the cases $k \le n$ and $k \ge n$. If $k \le n$, we know
by \cref{lem:connected-map-equiv-truncation} that $\trunc nf : \trunc nA \to \trunc nB$ is an
equivalence. We can now prove that $\trunc kf$ is also an equivalence. This follows from the fact
that $\trunc kf$ is homotopic to $\trunc k{\trunc nf}$, under the equivalence given
by \cref{lem:truncation-le}. This homotopy is easily proven by truncation induction. Now since
$\trunc kf$ is an equivalence, it's clearly $n$-connected.

If $k \ge n$ we apply \cref{prop:nconnected_tested_by_lv_n_dependent types}. It is sufficient to
show that the map $\lam{s} s\circ \trunc kf : \Parens{\prd{b:\trunc kB}
P(b)}\to\Parens{\prd{a:\trunc kA}P(\trunc kf(a))}$ has a section, for all $P : \trunc
kB\to\type$. We know that the map $\lam{s} s\circ f :\Parens{\prd{b:B}
Q(b)}\to\Parens{\prd{a:A}Q(f(a))}$ has a section $g$, for $Q:B\to\type$ defined by $Q(b)\defeq
P(\tproj kb)$. We define $h : \Parens{\prd{a:\trunc kA}P(\trunc kf(a))}\to\Parens{\prd{b:\trunc kB}
P(b)}$ by $h(t,\tproj kb):\equiv g(t \circ \tprojf k, b)$. The function $h$ is indeed a section,
which means that we need to show that for $t : \prd{a:\trunc kA}P(\trunc kf(a))$ we have
$h(t)\circ \trunc kf = t$. By function extensionality and truncation induction, it is sufficient to
show that the functions have the same value when applied to $\tproj ka$, for $a : A$. This follows
from the following computation
\begin{align*}
  (h(t)\circ \trunc kf)(\tproj ka) & \equiv h(t, \tproj k{f(a)})\\
  & \equiv g(t \circ \tprojf k, f(a)) \\
  &= (t \circ \tprojf k)(a) \tag{since $g$ is a section of $\lam{s} s\circ f$}\\
  & \equiv t(\tproj ka).
\end{align*}
\subsection*{Solution to \cref{ex:categorical-connectedness}}

Let us denote by $\mathsf{isConn}(A)$ the proposition that a type $A$ is connected. It is known that
\begin{displaymath}
 \eqv{\mathsf{isConn}(A)}{\brck A \times \prd{x,y:A} \brck {\id[A]xy}}
\end{displaymath}
(see \cref{ex:connectivity-inductively}).
\begin{enumerate}
 \item Suppose a type $A$ is connected. The goal $\prd{B,C:\type} \isequiv(e_{A,B,C})$ is a mere proposition, so we can assume $a:A$ and $\prd{x,y:A} \brck {x = y}$.

       Let $B,C$ be types.
       We want to construct $h:(A\to B+C) \to (A\to B)+(A\to C)$ such that
       $h \circ e_{A,B,C} = \idfunc[(A \to B) + (A \to C)]$ and
       $e_{A,B,C} \circ h = \idfunc[A \to B + C]$.
       Let $f:A \to B+C$ be an arbitrary function.
       Let us define $h(f):(A \to B) + (A \to C)$
       by case analysis on $f(a):B + C$:
       \begin{itemize}
	\item if $f(a) \jdeq \inl(u)$ for some $u:B$:
	      Let us define $k_1:B+C\to B$ by
	      \begin{align*}
	       k_1(\inl(b)) &\defeq b;\\
	       k_1(\inr(c)) &\defeq u,
	      \end{align*}
	      and let $h(f)$ be $\inl(k_1 \circ f)$.
	\item if $f(a) \jdeq \inr(u)$ for some $u:C$:
	      Let us define $k_2:B+C\to C$ by
	      \begin{align*}
	       k_2(\inl(b)) &\defeq u;\\
	       k_2(\inr(c)) &\defeq c,
	      \end{align*}
	      and let $h(f)$ be $\inr(k_2 \circ f)$.
       \end{itemize}
       Let us prove that this $h$ is indeed an inverse of $e_{A,B,C}$.
       First we prove $e_{A,B,C}(h(f)) = f$ for every $f:A \to B + C$
       by case analysis on $f(a)$:
       \begin{enumerate}[label=(\alph*)]
        \item \label{enum:categorical-connectedness-inl}
	      if $f(a) \jdeq \inl(u)$ for some $u:B$:
	      We have $\inl(k_1(f(x))) = f(x)$ for every $x:A$
	      by case analysis on $f(x)$:
	      \begin{itemize}
	       \item if $f(x) \jdeq \inl(v)$ for some $v:B$:
		     $\inl(k_1(f(x))) = \inl(k_1(\inl(v))) = \inl(v) = f(x)$,
	       \item if $f(x) \jdeq \inr(v)$ for some $v:C$:
		     we have $f(a) \neq f(x)$,
		     which contradicts $\brck {\id[A]{a}{x}}$.
	      \end{itemize}
	      Then we have
	      \begin{displaymath}
	       e_{A,B,C}(h(f)) = e_{A,B,C}(\inl(k_1 \circ f))
	       = \lam{x} \inl(k_1(f(x))) = f.
	      \end{displaymath}
	\item if $f(a) \jdeq \inr(u)$ for some $u:C$:
	      Similar to \ref{enum:categorical-connectedness-inl}.
       \end{enumerate}
       Next we prove $h(e_{A,B,C}(f)) = f$ for every $f:(A \to B) + (A \to C)$
       by case analysis on $f$:
       \begin{enumerate}[label=(\alph*)]
        \item if $f \jdeq \inl(g)$ for some $g: A \to B$:
	      \begin{displaymath}
	       h(e_{A,B,C}(f)) = h(e_{A,B,C}(\inl(g))) = h(\lam{x} \inl(g(x)))
	       = \inl(\lam{x} g(x)) = f,
	      \end{displaymath}
	\item if $f \jdeq \inr(g)$ for some $g: A \to C$:
	      \begin{displaymath}
	       h(e_{A,B,C}(f)) = h(e_{A,B,C}(\inr(g))) = h(\lam{x} \inr(g(x)))
	       = \inr(\lam{x} g(x)) = f.
	      \end{displaymath}
       \end{enumerate}
       Therefore we have $\isequiv(e_{A,B,C})$.
 \item (Categorical connectedness to $\mathsf{isConn}$ implies $\LEM{}$):
       Assume for every type $A$,
       \begin{displaymath}
	\Parens{\prd{B,C:\type}\isequiv(e_{A,B,C})} \to \mathsf{isConn}(A).
       \end{displaymath}
       Assuming $\neg \neg P$ for a mere proposition $P$, we want to prove $P$.
       Let us define $A \defeq \susp P$.
       Since $P \eqvsym (\id[\susp P]{\north}{\south}) \eqvsym \brck {\id[\susp P]{\north}{\south}}$ (by \cref{prop:trunc_of_prop_is_set}
       and since $P$ is a mere proposition) and $\mathsf{isConn}(\susp P)$ implies $\brck {\id[\susp P]{\north}{\south}}$ (by \cref{ex:connectivity-inductively}),
       it suffices to prove $\prd{B,C:\type}\isequiv(e_{\susp P,B,C})$.

       Before proving this, we prove that
       \begin{equation}
	\label{lem:cat-conn-neg-neg-eq-xy}
	\prd{x, y:\susp P} \neg \neg (x =_{\susp P} y)
       \end{equation}
       by case analysis on $x$ and $y$:
       \begin{enumerate}[label=(\alph*)]
	\item if $x \jdeq \north$:
	      \begin{itemize}
	       \item if $y \jdeq \north$: $\lam{k} k(\refl{\north})$ has type
		     $\neg \neg (\north = \north)$.
	       \item if $y \jdeq \south$:
		     $\neg \neg (\north = \south)$ is equivalent to
		     $\neg \neg P$, so it is inhabited.
	       \item if $y$ varies on $\merid(p)$ for some $p: P$: Since
		     $\neg \neg (\north =_{\susp P} y)$ is a mere proposition
		     for every $y$ (see \cref{thm:isprop-forall}),
		     we do not need to consider this case.
	      \end{itemize}
	      \label{enum:categorical-connectedness-north}
	\item if $x \jdeq \south$:
	      Similar to \ref{enum:categorical-connectedness-north}.
	\item if $x$ varies on $\merid(p)$ for some $p: P$:
	      Since $\prd{y:\susp P} \neg \neg (x =_{\susp P} y)$
	      is a mere proposition for every $x$,
	      we do not need to consider this case.
       \end{enumerate}

       Let us prove $\prd{B,C:\type}\isequiv(e_{\susp P,B,C})$.
       Let $B, C$ be types.
       We want to construct
       $h:(\susp P\to B+C) \to (\susp P \to B)+(\susp P\to C)$ such that
       $h \circ e_{\susp P,B,C} = \idfunc[(\susp P\to B) + (\susp P\to C)]$ and
       $e_{\susp P,B,C} \circ h = \idfunc[\susp P\to B + C]$.

       Let $f:\susp P\to B+C$ be an arbitrary function.
       Let us define $h(f):(\susp P\to B) + (\susp P\to C)$
       by case analysis on $(f(\north), f(\south)):(B + C) \times (B + C)$:
       \begin{itemize}
	\item if $(f(\north), f(\south)) \jdeq (\inl(u_1), \inl(u_2))$
	      for some $u_1, u_2:B$:
	      Let us define $k_1:B+C\to B$ by
	      \begin{align*}
	       k_1(\inl(b)) &\defeq b;\\
	       k_1(\inr(c)) &\defeq u_1,
	      \end{align*}
	      and let $h(f)$ be $\inl(k_1 \circ f)$.
	\item if $(f(\north), f(\south)) \jdeq (\inr(u_1), \inr(u_2))$
	      for some $u_1, u_2:C$:
	      Let us define $k_2:B+C\to C$ by
	      \begin{align*}
	       k_2(\inl(b)) &\defeq u_1;\\
	       k_2(\inr(c)) &\defeq c,
	      \end{align*}
	      and let $h(f)$ be $\inl(k_2 \circ f)$.
	\item if $(f(\north), f(\south)) \jdeq (\inl(u), \inr(v))$
	      for some $u: B, v:C$: This case is impossible.
	      $f(\north) \neq f(\south)$ implies $\north \neq \south$,
	      which contradicts \eqref{lem:cat-conn-neg-neg-eq-xy}.
	\item if $(f(\north), f(\south)) \jdeq (\inr(u), \inl(v))$
	      for some $u: C, v:B$: This case is also impossible.
       \end{itemize}
       Let us prove that this $h$ is indeed an inverse of $e_{\susp P,B,C}$.
       First we prove $e_{\susp P,B,C}(h(f)) = f$ for every $f:\susp P\to B+C$.
       It is done by case analysis on
       $(f(\north), f(\south)):(B + C) \times (B + C)$:
       \begin{enumerate}[label=(\alph*)]
        \item if $(f(\north), f(\south)) \jdeq (\inl(u_1), \inl(u_2))$
	      for some $u_1, u_2:B$:
	      We have $\inl(k_1(f(x))) = f(x)$ for every $x:\susp P$
	      by case analysis on $f(x)$:
	      \begin{itemize}
	       \item if $f(x) \jdeq \inl(v)$ for some $v:B$:
		     $\inl(k_1(f(x))) = \inl(k_1(\inl(v))) = \inl(v) = f(x)$,
	       \item if $f(x) \jdeq \inr(v)$ for some $v:C$:
		     we have $f(\north) \neq f(x)$ and hence $\north \neq x$,
		     which contradicts \eqref{lem:cat-conn-neg-neg-eq-xy}.
	      \end{itemize}
	      Then we have
	      \begin{displaymath}
	       e_{\susp P,B,C}(h(f)) = e_{\susp P,B,C}(\inl(k_1 \circ f))
	       = \lam{x} \inl(k_1(f(x))) = f.
	      \end{displaymath}
	      \label{enum:inl-inl}
	\item if $(f(\north), f(\south)) \jdeq (\inr(u_1), \inr(u_2))$
	      for some $u_1, u_2:C$: Similar to \ref{enum:inl-inl}.
       \end{enumerate}
       Next we prove $h(e_{\susp P,B,C}(f)) = f$
       for every $f:(\susp P\to B) + (\susp P\to C)$
       by case analysis on $f$:
       \begin{enumerate}
        \item if $f \jdeq \inl(g)$ for some $g: \susp P\to B$:
	      \begin{displaymath}
	       h(e_{\susp P,B,C}(f)) = h(e_{\susp P,B,C}(\inl(g)))
	       = h(\lam{x} \inl(g(x)))
	       = \inl(\lam{x} g(x)) = f,
	      \end{displaymath}
	\item if $f \jdeq \inr(g)$ for some $g: \susp P\to C$:
	      \begin{displaymath}
	       h(e_{\susp P,B,C}(f)) = h(e_{\susp P,B,C}(\inr(g)))
	       = h(\lam{x} \inr(g(x)))
	       = \inr(\lam{x} g(x)) = f.
	      \end{displaymath}
       \end{enumerate}
       Therefore we have $\isequiv(e_{\susp P,B,C})$.

       ($\LEM{}$ implies categorical connectedness to $\mathsf{isConn}$):
       Assume $\LEM{}$, $A:\type$ and
       \begin{displaymath}
        \prd{B,C:\type} \isequiv(e_{A,B,C}).
       \end{displaymath}
We need to prove $\mathsf{isConn}(A)$.
       By $\LEM{}$ we have $\brck A$, because if $\neg \brck A$ we have $\eqv{A}{\emptyt}$ and $\eqv{\unit + \unit}{\unit}$, which is not the case.
       Also by $\LEM{}$, for every $x,y:A$ we have $\brck {x = y} + \neg \brck {x = y}$. So if we fix $x:A$ we have a function $f_x:A \to \unit + \unit$ such that
       \begin{displaymath}
	f_x(y) \defeq \begin{cases}
		     \inl(\ttt) & \mbox{if } \brck {x = y} \\
		     \inr(\ttt) & \mbox{if } \neg \brck {x = y}
		    \end{cases}
       \end{displaymath}
       Applying the assumption to $f_x$, we obtain
       \begin{displaymath}
	\inv{e_{A,\unit,\unit}}(f_x): (A \to \unit) + (A \to \unit)
       \end{displaymath}
       but by definition of $e$ and because $f_x(x) = \inl(\ttt)$,
       it must be equal to $\inl(\lam{y} \ttt): (A \to \unit) + (A \to \unit)$,
       which means we have $\prd{y:A} \brck {x = y}$.
\end{enumerate}


\section*{Exercises from \cref{cha:homotopy}}

\subsection*{Solution to \cref{ex:homotopy-groups-resp-prod}}
Remember that the fundamental group of a pointed space is defined as the
$0$-truncation of the loop space of that space.
If we prove the equivalence without applying $\trunc 0{\blank}$ to both sides
we are done.  We use induction on the natural numbers, with base case $1$.

Suppose we have two pointed types $(A,a)$ and $(B,b)$.
For the base case, we have $\eqv{\Omega(A \times B)}{\Omega(A) \times \Omega(B)}$
because it is, by definition, the equivalence of pointed types:

\[\eqv{ \Parens{(a,b)=(a,b), \refl{(a,b)}} }{\Parens{(a=a \times b=b), (\refl{a}, \refl{b})}}.\]

By the characterization of \cref{thm:path-sigma} we see
that it suffices to give a:
\[p:\eqv{\Parens{(a,b)=(a,b)}}{\Parens{(a=a)\times (b=b)}}\]

And to show that transporting $\refl{(a,b)}$ along $p$ is equal to
$(\refl{a}, \refl{b})$.  To construct $p$ just use \cref{thm:path-prod}. To
show that transport respects the equality we use
the definition
of our function $p$, that is just an application of the projections and
functoriality (see \cref{eq:path-prod}).

For the inductive step we use the inductive hypothesis to get an equivalence:
$\eqv{\Omega^n(A \times B)}{\Omega^n(A) \times \Omega^n(B)}$.
Then we apply $\Omega(\blank)$ on both sides and use exactly the same
propositions we used in the base
case. This settles the inductive case, because of the inductive definition of
$\Omega^{\suc(n)}(\blank)$.


\subsection*{Solution to \cref{ex:contr-infinity-sphere-colim}}

To solve this exercise we must first define the spheres as a type family
$\Sn^{\blank} : \nat \to \UU$.
Then we must define the inclusions that appear the in the diagram:
\[ \Sn^0 \to \Sn^1 \to \Sn^2 \to\cdots \]

Then we will be able to define the colimit as
a higher inductive type.

So, by induction on the natural numbers, we define $\Sn^{\blank} : \nat \to \UU$
with the base case being the two point type $\bool$, and the inductive case
being the iterated application of the suspension.

Now we define the inclusions $i_n : \Sn^n \to \Sn^{n+1}$.
For the base case we have to give a function $i_0 : \bool \to \susp \bool$.
This is easy: send one point to $\north$ and the other to $\south$.

For the inductive case we notice that the domain of the function $i_n$ that
we have to define is the suspension $\susp \Sn^{n-1}$. So we can use the
induction of $\susp \Sn^{n-1}$. The codomain is also a suspension, so we can
use any of the constructors:
\begin{align*}
  \north_{n+1} &: \Sn^{n+1}\\
  \south_{n+1} &: \Sn^{n+1}\\
  \merid_{n+1} &:\Sn^n \to \north_{n+1} = \south_{n+1}
\end{align*}
to define our function.
We send $\north_n \mapsto \north_{n+1}$ and $\south_n \mapsto \south_{n+1}$.
Now we must give a $\susp \Sn^{n-1}$-indexed family of equalities between
$\north_{n+1}$ and $\south_{n+1}$. By inductive hypothesis we have
$i_{n-1} : \Sn^{n-1} \to \Sn^n$, so we can use:
\[ \merid_{n+1} \circ i_{n-1} \]
It is also interesting to note that this construction works in a more general
setting: any function $f : A \to B$ induces a function $\susp f : \susp A \to \susp B$.

Now is a good time to make a drawing to convince oneself that this is the
right way to define the inclusions between consecutive spheres, and that this
is the diagram intended in the exercise.

Let's define the type $\Sn^{\infty}$ as the colimit of the diagram we just
constructed. The constructors are:
\begin{align*}
  j_{\blank} &: \prd{n : \nat} \Sn^n \to \Sn^{\infty}\\
  \glue_{\blank} &: \prd{n : \nat}{x: \Sn^n} j_n(x) = j_{n+1}(i_n (x))
\end{align*}
And the induction:
\[
  \ind{\Sn^{\infty}} : \prd{C:\Sn^\infty \to \UU}{J_{\blank} : \prd{n : \nat}{x : \Sn^n} C(j_n(x))}
  \Parens{\prd{n:\nat}{x:\Sn^n} \dpath C {\glue_n(x)} {J_n(x)} {J_{n+1} (i_n (x))}}
  \to \prd{e:\Sn^{\infty}} C(e)
\]

We also have the usual computational rules.
Now, we can interpret the proof that we are going to give as follows.
Each sphere is a meridian of the next one, as it passes
through the $\north$ and $\south$ of the bigger sphere.
The intuitive idea is that we can retract to a point a circle that is the equator of a sphere.
Just as we can retract to a point two points that are the equator of a circle.
This idea extends to all $n$-spheres. If we have all the spheres at the same time
we can retract them all. But we have to be careful: the homotopies
must be coherent for the total homotopy to be well defined. This can be done in
classical homotopy theory using the fact that a CW complex is the colimit of
the inclusions between its skeletons. In our case we constructed the colimit.
So, if we define a homotopy for each sphere, and prove that this functions
coincide in the glued parts (respect the equalities given by $\glue$), by
induction on the colimit we get a homotopy defined in the colimit.

The outline of the argument is as follows. It suffices to show that every point in
$\Sn^{\infty}$ is equal to $j_0(\north_0)$, we prove it in two steps.
The first step is to prove it only for the points of the form $j_n(\north_n)$.
For the second step we will take an arbitrary $x:\Sn^{\infty}$
and, by induction, we will assume it comes from a $y : \Sn^n$ for some $n$,
that is $x \defeq j_n(y)$.
Then we note that using the commutative diagram given by $\glue_n(x)$:
\begin{center}
\begin{tikzpicture}
\node (N0) at (0,2) {$\Sn^{n}$};
\node (N1) at (2,2) {$\Sn^{n+1}$};
\node (N2) at (2,0) {$\Sn^{\infty}$};
\node (N3) at (1.1,1.1) {};
\node (N4) at (1.5,1.5) {};
\draw[->] (N0) -- node[above]{\footnotesize $i_n$} (N1);
\draw[->] (N0) -- node[left]{\footnotesize $j_n$} (N2);
\draw[->] (N1) -- node[right]{\footnotesize $j_{n+1}$} (N2);
\draw[double, double equal sign distance] (N3) -- node[left,above]{\footnotesize $glue_n$} (N4);
\end{tikzpicture}
\end{center}
we get a path $x \defeq j_n(y) = j_{n+1} (i_n(y))$.
But, as we will show, the inclusion $i_n$ of $\Sn^n$ in $\Sn^{n+1}$ is nullhomotopic,
every point in the image is equal to $\north_{n+1}$. Thus, we are able to show that
$j_{n+1}(i_n(y)) = j_{n+1}(\north_{n+1})$. Composing the proof of the first step
with the proof of the second step we conclude the exercise.

To construct a $D_{\blank} : \prd{n:\nat} j_n(\north_n) = j_0(\north_0)$ we
proceed by induction on $n$. For the base case we can
use $\refl{j_0(\north_0)}$. For the inductive case, we have by inductive
hypothesis $j_n(\north_n) = j_0(\north_0)$. By our definition of $i_{\blank}$,
we have that $\north_{n+1} \equiv i_n(\north_n)$. So $j_{n+1} (\north_{n+1})$
equals $j_{n+1}(i_n(\north_n))$. By concatenation with $\glue_n(\north_n)$,
we reduce our goal to the inductive hypothesis.

Let's now show that the inclusion of $\Sn^n$ in $\Sn^{n+1}$ can be
continuously retracted to $\north_{n+1}$.
That is, let's construct a homotopy:
\[ H_{\blank} : \prd{n:\nat}{x:\Sn^n} i_n(x) = \north_{n+1} \]
For the case $n\equiv 0$ we know that $i_0(\btrue) \equiv \north_1$ and
$i_0(\bfalse) \equiv \south_1$.  This is because we constructed the inclusion
that way. So we can prove the equalities
using $\refl{\north_1}$ and $\merid_1(\btrue) : \north_1 = \south_1$.

For the inductive case we defined, previously, $i_n(\north_n) \equiv \north_{n+1}$
and $i_n(\south_{n}) \equiv \south_{n+1}$. So we can prove the equalities using
$\refl{\north_{n+1}}$ and $(\merid_{n+1}(\north_n))^{-1}$.
Then we have to prove that the function respects $\merid_n$:
\[ \prd{x:\Sn^{n-1}} \dpath {x\mapsto (i_n(x) = \north_{n+1})} {\merid_n(x)} {\refl{\north_{n+1}}} {(\merid_{n+1}(\north_n))^{-1}} \]
By \cref{thm:transport-path} (and some straightforward computation) this reduces to:
\[ i_n(\merid_n(x)) = \merid_{n+1}(\north_{n}) \]
But, by our definition of $i_{\blank}$, and the computation rule of the
suspension induction $i_n(\merid_n(x))$ equals $\merid_{n+1} (i_{n-1}(x))$.
And, by inductive hypothesis, $i_{n-1}(x) = \north_n$, which gives us the
desired result.

Composing the two proofs we just gave we get a function:
\[ J_n(x) \defeq \glue_n(x)\ct \apfunc{j_{n+1}}{H_n(x)}\ct D_{n+1}
    : \prd{n:\nat}{x:\Sn^n} j_n(x) = j_0(\north_0). \]
We use this function and induction on $\Sn^{\infty}$ to derive
the contractibility of the space.
Now it remains to show that our function respects the gluing:
\[ \prd{n:\nat}{x:\Sn^n} \dpath {x\mapsto (x = j_0(\north_0))}
  {\glue_n(x)} {J_n(x)} {J_{n+1}(i_n (x))} \]
By definition this is:
\[ \prd{n:\nat}{x:\Sn^n}
    \transfib{x\mapsto (x = j_0(\north_0))}{\glue_n(x)}{J_n(x)}
    = {J_{n+1}(i_n (x))} \]

The LHS is equal to $\glue_{n}(x)^{-1}\ct J_n(x)$, which, by definition of
$J_n(x)$, is:
\[ \glue_n(x)^{-1}\ct\glue_n(x)\ct\apfunc{j_{n+1}}{H_n(x)}\ct D_{n+1} \]
Cancelling we get:
\[ \apfunc{j_{n+1}}{H_n(x)}\ct D_{n+1} \]

We also use the definition of $J_{\blank}$ in the RHS, and then the computation
rule of $D_{\blank}$, giving us the equalities:
\begin{align*}
  & J_{n+1}(i_n(x))\\
  &= \glue_{n+1}(i_n(x))\ct\apfunc{j_{n+2}}{H_{n+1}(i_n(x))}\ct D_{n+2}\\
  &= \glue_{n+1}(i_n(x))\ct\apfunc{j_{n+2}}{H_{n+1}(i_n(x))}\ct
                                  \glue_{n+1}(\north_{n+1})^{-1}\ct D_{n+1}.
\end{align*}

So it suffices to show:
\[ \apfunc{j_{n+1}}{H_n(x)} = \glue_{n+1}(i_n(x))\ct\apfunc{j_{n+2}}{H_{n+1}(i_n(x))}
  \ct\glue_{n+1}(\north_{n+1})^{-1} \]
Or equivalently:
\[ \apfunc{j_{n+1}}{H_n(x)} \ct\glue_{n+1}(\north_{n+1}) =
  \glue_{n+1}(i_n(x))\ct\apfunc{j_{n+2}}{H_{n+1}(i_n(x))} \]

But we remember that we have the homotopy
$\glue_{n+1} : j_{n+1} = j_{n+2}\circ i_{n+1}$, so, by a simple application
of \cref{lem:htpy-natural} and the functoriality of $\apfunc{}{}$, we get
a proof of the equality:
\[ \apfunc{j_{n+1}}{H_n(x)} \ct\glue_{n+1}(\north_{n+1}) =
  \glue_{n+1}(i_n(x))\ct\apfunc{j_{n+2}}{\apfunc{i_{n+1}}{H_n(x)}} \]
So we reduced the goal to showing:
\[ \apfunc{i_{n+1}}{H_n(x)} = H_{n+1}(i_n(x)) \]

This can be done easily by induction in $\Sn^n$ using the definition of $H_{\blank}$.


\subsection*{Solution to \cref{ex:contr-infinity-sphere-susp}}

First we write down the type of the induction principle explicitly:

\[ \ind{\Sn^\infty} : \prd{C:\Sn^\infty \to \UU}{n:C(\north)}{s:C(\south)}
  \Parens{\prd{x:\Sn^\infty} C(x) \to \dpath C {\merid(x)} {n}{s}} \to \prd{x:\Sn^\infty} C(x) . \]

  We take $\north$ as center of contraction. So we have to prove
  $\prd{x:\Sn^\infty} \north = x$. For this we use induction on $\Sn^\infty$ taking:
\[C \defeq (\lambda x. \north = x) : \Sn^\infty \to \UU .\]

  When $x$ is $\north$ we just use $\refl{\north} : \north = \north$. When $x$
  is $\south$ we use $\merid(\north) : \north = \south$.
  When $x$ varies along $\merid$ we have to give a function of type:
\[\prd{x:\Sn^\infty} \Parens{\north = x} \to \Parens{\dpath C {\merid(x)} {\refl{\north}}{\merid(\north)}}. \]
  So, given $x : \Sn^\infty$ and $p : \north = x$, we have to prove:
  \[\transfib{x \mapsto (\north = x)}{\merid(x)}{\refl{\north}} = \merid(\north).\]

By \cref{cor:transport-path-prepost} it suffices to show
$\refl{\north}\ct \merid(x) = \merid(\north)$. Canceling $\refl{\north}$ and
applying $\merid$ to $p$ gets us the desired result.

\subsection*{Solution to \cref{ex:unique-fiber}}

We know that every two points $y_1,y_2 : Y$ are merely equal, because $Y$ is
is connected. That is, we have a function
$c : \prd{y_1,y_2:Y}\trunc {} {y_1 = y_2}$. To prove this we can use the remark
after \cref{thm:connected-pointed}. If we want to show that any pair of
points $y_1,y_2 : Y$ are merely equal we can use the first point $y_1$ to get
a pointed space $(Y,y_1)$, and then use the remark.

We note that it suffices to show that for any $y_1,y_2:Y$ we have
$\trunc {} {\hfib{f}{y_1} = \hfib{f}{y_2}}$ because
$\hfib{f}{y_1} = \hfib{f}{y_2}$ implies (using $\idtoeqv$)
$\hfib{f}{y_1}\simeq \hfib{f}{y_2}$
and thus, by recursion on the truncation of $\hfib{f}{y_1} = \hfib{f}{y_2}$,
we get that $\trunc {} {\hfib{f}{y_1} = \hfib{f}{y_2}}$ implies
$\trunc {} {\hfib{f}{y_1} \simeq \hfib{f}{y_2}}$.

The type of $c(y_1,y_2)$ is a truncation, so we can use its recursion to
prove the desired result.
By recursion we can assume that $y_1 = y_2$, and in that case we obviously have
$\trunc {} {\hfib{f}{y_1} = \hfib{f}{y_2}}$. We also have to show that
the proposition we want to prove is $-1$-truncated, but that is straightforward
because it is a $-1$-truncation.


\section*{Exercises from \cref{cha:category-theory}}

\subsection*{Solution to \cref{ex:stack}}

Define $K$ to be the precategory with $K_0 \defeq Y$ and $\hom_K(y_1,y_2) \defeq (p(y_1)=p(y_2))$.
Then $\mathrm{Desc}(A,p)\defeq A^K$ is a good definition.
Moreover, the obvious functor $K\to X$ (where $X$ denotes the discrete category on itself) is a weak equivalence, so \cref{ct:esofull-precomp-ff,ct:cat-weq-eq} yield the second and third parts.
Finally, $K$ is a strict category, so if it is a stack, then $p$ has a section, while conversely if $p$ has a section then $K\to X$ is a (strong) equivalence.

\section*{Exercises from \cref{cha:set-math}}

\subsection*{Solution to \cref{ex:prop-ord}}

Define $A<B$ iff $B \land \neg A$.

\subsection*{Solution to \cref{ex:ninf-ord}}

Define $a<b$ iff $\exis{n:\nat} (b_n < a_n)$.

\end{document}