Spectral/Notes/smash.tex

\documentclass{article}

\input{preamble-articles}

\title{Notes on the smash product}
\date{\today}
\usepackage{fullpage}
\newcommand{\pmap}{\to}
\newcommand{\lpmap}{\xrightarrow}
\renewcommand{\smash}{\wedge}
\renewcommand{\phi}{\varphi}
\renewcommand{\epsilon}{\varepsilon}
\newcommand{\tr}{\cdot}
\renewcommand{\o}{\ensuremath{\circ}}
\newcommand{\auxl}{\mathsf{auxl}}
\newcommand{\auxr}{\mathsf{auxr}}
\newcommand{\gluel}{\mathsf{gluel}}
\newcommand{\gluer}{\mathsf{gluer}}
\newcommand{\sy}{^{-1}}
\newcommand{\const}{\ensuremath{\mathbf{0}}\xspace}
\newcommand{\alphabar}{\overline{\alpha}}
\newcommand{\rhobar}{\overline{\rho}}
\newcommand{\lambdabar}{\overline{\lambda}}
\newcommand{\gammabar}{\overline{\gamma}}
\newcommand{\pType}{\mathsf{Type}_\ast}
\newcommand{\two}{\mathbf{2}}
\newcommand{\yoneda}{\mathbf{Y}}

\begin{document}

\maketitle

\section{Pointed Types}

\begin{defn}
  We work in the $(\infty,1)$-category of pointed types.
  \begin{itemize}
  \item The objects are pointed types $A$, types together with a basepoint $a_0:A$.
\item 1-cells are pointed maps $f:A\to B$ which are maps with a chosen path $f_0:f(a_0)=b_0$. We
  write $A\pmap B$ for pointed maps and $A\pmap B\pmap C$ means $A\pmap (B\pmap C)$.
\item 2-cells are pointed homotopies. A pointed homotopy $h:f\sim g$ is a homotopy with a chosen 2-path
  $h(a_0) \tr g_0 = f_0$.
\item As 3-cells (or higher cells) we take equalities between 2-cells (or higher cells).
\end{itemize}
\end{defn}

\begin{rmk}
\item All types, maps and homotopies in these notes are pointed, unless explicitly mentioned
  otherwise. Whenever we say that a diagram of $n$-cells commutes we mean it in the sense that there
  is an $(n+1)$-cell witnessing it.
\item Pointed homotopies are equivalent to equalities of pointed types: $(f\sim g)\equiv (f=g)$. So
  we could have chosen to define our 2-cells as equalities between 1-cells. We choose not to, since
  the aforementioned equivalence requires function extensionality. In a type theory where function
  extensionality doesn't compute (like Lean) it is better to define the type of pointed homotopies
  manually so that the underlying homotopy of a 2-cell is definitionally equal to the homotopy we
  started with. In diagrams, we will denote pointed homotopies by equalities, but we always mean
  pointed homotopies.
\item The type $A\to B$ of pointed maps from $A$ to $B$ is itself pointed, with as basepoint the
  constant map $0\equiv0_{A,B}:A\to B$ which has as underlying function $\lam{a:A}b_0$. We have
  $0\o g \sim 0$ and $f \o 0 \sim 0$.
\item A pointed equivalence is a pointed map $f : A \to B$ whose underlying map is an
  equivalence. In this case, we can find a pointed map $f\sy:B\to A$ with pointed homotopies
  $f\o f\sy\sim0$ and $f\sy\o f\sim0$.
\end{rmk}

\begin{lem}
  Given maps $f:A'\pmap A$ and $g:B\pmap B'$. Then there are maps
  $(f\pmap C):(A\pmap C)\pmap(A'\pmap C)$ and $(C\pmap g):(C\pmap B)\pmap(C\pmap B')$ given by
  precomposition with $f$, resp. postcomposition with $g$. The map $\lam{g}C\pmap g$ preserves the basepoint, giving rise to a map $$(C\pmap ({-})):(B\pmap B')\pmap(C\pmap B)\pmap(C\pmap B').$$
  Also, the following square commutes
\begin{center}
\begin{tikzcd}
(A\pmap B) \arrow[r,"A\pmap g"]\arrow[d,"f\pmap B"] & (A\pmap B')\arrow[d,"f\pmap B'"] \\
(A'\pmap B) \arrow[r,"A'\pmap g"] & (A'\pmap B')
\end{tikzcd}
\end{center}

\end{lem}

\begin{defn}[Naturality]\label{def:naturality}
	Let $F$, $G$ be functors of pointed types, i.e. pointed maps with a functorial action (e.g. if $f : A \to B$, then we can define $F(f) : F(A) \to F(B)$, respecting identity and composition). 
	Let $\theta : F \Rightarrow G$ be a natural transformation from $F$ to $G$, i.e. a pointed map $F(X) \to G(X)$ for all pointed types $X$. For every $f : A \to B$, there is a diagram:
	\begin{center}
	\begin{tikzcd}
		F(A)
			\arrow[r, "F(f)"]
			\arrow[d, swap, "\theta_A"]
		& F(B)
			\arrow[d, "\theta_B"]
		\\
		G(A)
			\arrow[r, swap, "F(g)"]
		& G(B)
	\end{tikzcd}
	\end{center}
	We define the following notions of naturality for $\theta$:
	\begin{itemize}
		\item \textbf{(strong) naturality} will refer to a pointed homotopy
		\[p(f) : \theta_B \o F(f) \sim G(f) \o \theta_A\]
		for every $f : A \to B$ and \textbf{weak naturality} to the underlying (non-pointed) homotopy;
		\item \textbf{pointed (strong) naturality} will refer to the same pointed homotopy, with the additional condition that $p(0) = p_0$, where
		\[p_0 : \theta_B \o F(0) \sim \theta_B \o 0 \sim 0 \sim 0 \o \theta_A \sim G(0) \o \theta_A\]
		is the canonical proof of the pointed homotopy $\theta_B \o F(0) \sim G(0) \o \theta_A$, whereas \textbf{pointed weak naturality} will refer to the corresponding non-pointed condition.
	\end{itemize}
\end{defn}

\begin{rmk}
	The relation between the four notions of naturality is as expected: strong implies weak, and pointed implies simple. Weak naturality is generally ill-behaved: for example, weak naturality of $\theta$ does not imply weak naturality of $\theta \to X$ or $X \to \theta$, whereas the implication holds for strong naturality.
\end{rmk}

\section{Smash Product}

\begin{defn}
  The smash of $A$ and $B$ is the HIT generated by the point constructor $(a,b)$ for $a:A$ and $b:B$
  and two auxilliary points $\auxl,\auxr:A\smash B$ and path constructors $\gluel_a:(a,b_0)=\auxl$
  and $\gluer_b:(a_0,b)=\auxr$ (for $a:A$ and $b:B$). $A\smash B$ is pointed with point $(a_0,b_0)$.
\end{defn}
\begin{rmk}
\item This definition of $A\smash B$ is basically the pushout of
  $\bool\leftarrow A+B\to A \times B$.  A more traditional definition of $A\smash B$ is the pushout
  $\unit\leftarrow A\vee B\to A \times B$. Here $\vee$ denotes the wedge product, which can be
  equivalently described as either the pushout $A\leftarrow \unit\to B$ or
  $\unit\leftarrow \bool\to A + B$. These two definitions of $A\smash B$ are equivalent, because in
  the following diagram the top-left square and the top rectangle are pushout squares, hence the
  top-right square is a pushout square by applying the pushout lemma. Another application of the
  pushout lemma now states that the two definitions of $A\smash B$ are equivalent.
\begin{center}
\begin{tikzcd}
\bool \arrow[r]\arrow[d] & A+B     \arrow[r]\arrow[d] & \bool \arrow[d] \\
\unit \arrow[r]          & A\vee B \arrow[r]\arrow[d] & \unit \arrow[d] \\
                     & A\times B        \arrow[r] & A\smash B
\end{tikzcd}
\end{center}

\end{rmk}
\begin{lem}\mbox{}\label{lem:smash-general}
  \begin{itemize}
  \item The smash is functorial: if $f:A\pmap A'$ and $g:B\pmap B'$ then
    $f\smash g:A\smash B\pmap A'\smash B'$. We write $A\smash g$ or $f\smash B$ if one of the
    functions is the identity function.
  \item Smash preserves composition, which gives rise to the interchange law:
    $i:(f' \o f)\smash (g' \o g) \sim f' \smash g' \o f \smash g$
  \item If $p:f\sim f'$ and $q:g\sim g'$ then $p\smash q:f\smash g\sim f'\smash g'$. This operation
    preserves reflexivities, symmetries and transitivies.
  \item There are homotopies $f\smash0\sim0$ and $0\smash g\sim 0$ such that the following diagrams
    commute for given homotopies $p : f\sim f'$ and $q : g\sim g'$.
    \begin{center}
\begin{tikzcd}
f\smash 0 \arrow[rr, equals,"p\smash1"]\arrow[dr,equals] & &
f'\smash 0\arrow[dl,equals] \\
& 0 &
\end{tikzcd}
\qquad
\begin{tikzcd}
0\smash g\arrow[rr, equals,"1\smash q"]\arrow[dr,equals] & &
0\smash g'\arrow[dl,equals] \\
& 0 &
\end{tikzcd}
\end{center}

  \end{itemize}
\end{lem}

\begin{lem}\label{lem:smash-coh}
  Suppose that we have maps $A_1\lpmap{f_1}A_2\lpmap{f_2}A_3$ and $B_1\lpmap{g_1}B_2\lpmap{g_2}B_3$
  and suppose that either $f_1$ or $f_2$ is constant. Then there are two homotopies
  $(f_2 \o f_1)\smash (g_2 \o g_1)\sim 0$, one which uses interchange and one which doesn't. These two
  homotopies are equal. Specifically, the following two diagrams commute:
\begin{center}
\begin{tikzcd}
(f_2 \o 0)\smash (g_2 \o g_1) \arrow[r, equals]\arrow[dd,equals] &
(f_2 \smash g_2)\o (0 \smash g_1)\arrow[d,equals] \\
& (f_2 \smash g_2)\o 0\arrow[d,equals] \\
0\smash (g_2 \o g_1) \arrow[r,equals] &
0
\end{tikzcd}
\qquad
\begin{tikzcd}
(0 \o f_1)\smash (g_2 \o g_1) \arrow[r, equals]\arrow[dd,equals] &
(0 \smash g_2)\o (f_1 \smash g_1)\arrow[d,equals] \\
& 0\o (f_1 \smash g_1)\arrow[d,equals] \\
0\smash (g_2 \o g_1) \arrow[r,equals] &
0
\end{tikzcd}
\end{center}

\end{lem}
\begin{proof}
  We will only do the case where $f_1\jdeq 0$, i.e. fill the diagram on the left. The other case is
  similar (and slightly easier). First apply induction on the paths that $f_2$, $g_1$ and $g_2$
  respect the basepoint. In this case $f_2\o0$ is definitionally equal to $0$, and the canonical
  proof that $f_2\o 0\sim0$ is (definitionally) equal to reflexivity. This means that the homotopy
  $(f_2 \o 0)\smash (g_2 \o g_1)\sim0\smash (g_2 \o g_1)$ is also equal to reflexivity, and also the
  path that $f_2 \smash g_2$ respects the basepoint is reflexivity, hence the homotopy
  $(f_2 \smash g_2)\o 0\sim0$ is also reflexivity. This means we need to fill the following square,
  where $q$ is the proof that $0\smash f\sim 0$.
\begin{center}
\begin{tikzcd}
(f_2 \o 0)\smash (g_2 \o g_1) \arrow[r, equals,"i"]\arrow[d,equals,"1"] &
(f_2 \smash g_2)\o (0 \smash g_1)\arrow[d,equals,"(f_2\smash g_2)\o q"] \\
0\smash (g_2 \o g_1) \arrow[r,equals,"q"] &
0
\end{tikzcd}
\end{center}

  For the underlying homotopy, take $x : A_1\smash B_1$ and apply induction on $x$. Suppose
  $x\equiv(a,b)$ for $a:A_1$ and $b:B_1$. Then we have to fill the square (denote the basepoints of
  $A_i$ and $B_i$ by $a_i$ and $b_i$ and we suppress the arguments of $\gluer$). Now
  $\mapfunc{h\smash k}(\gluer_z)=\gluer_{k(z)}$, so by general groupoid laws we see that the path on
  the bottom is equal to the path on the right, which means we can fill the square.
  \begin{center}
    \begin{tikzcd}
      (f_2(a_2),g_2(g_1(b)))\arrow[r, equals,"1"]
      \arrow[d,equals,"1"] &
      % \arrow[d,equals,"\gluer_{g_2(g_1(b))}\tr\gluer_{g_2(g_1(b_1))}\sy"] &
      (f_2(a_2),g_2(g_1(b)))\arrow[d,equals,"\mapfunc{f_2\smash g_2}(\gluer\tr\gluer\sy)"] \\
      (a_3,g_2(g_1(b))) \arrow[r,equals,"\gluer\tr\gluer\sy"] &
      (a_3,b_3)
    \end{tikzcd}
  \end{center}
  If $x$ is either $\auxl$ or $\auxr$ it is similar but easier. For completeness, we will write down the square we have to fill in the case that $x$ is $\auxr$.
  \begin{center}
    \begin{tikzcd}
      \auxr \arrow[r, equals,"1"]
      \arrow[d,equals,"1"] &
      \auxr \arrow[d,equals,"\mapfunc{f_2\smash g_2}(\gluer_{b_2}\sy)"] \\
      \auxr \arrow[r,equals,"\gluer_{g_2(b_2)}\sy"] &
      (a_3,b_3)
    \end{tikzcd}
  \end{center}

  If $x$ varies over $\gluer_b$, we need to fill the cube below. The front and the back are the
  squares we just filled, the left square is a degenerate square, and the other three squares are
  the squares in the definition of $q$ and $i$ to show that they respect $\gluer_b$ (and on the
  right we apply $f_2\smash g_2$ to that square).
  \begin{center}
    \begin{tikzcd}
      & \auxr \arrow[rr, equals,"1"] \arrow[dd,equals,near start,"1"] & &
      \auxr \arrow[dd,equals,"\mapfunc{f_2\smash g_2}(\gluer_{b_2}\sy)"] \\
      (f_2(a_2),g_2(g_1(b)))\arrow[rr, equals, near start, crossing over, "1"]
      \arrow[dd,equals,"1"] \arrow[ur,equals] & &
      (f_2(a_2),g_2(g_1(b))) \arrow[ur,equals] & \\
      & \auxr \arrow[rr,equals,near start, "\gluer_{g_2(b_2)}\sy"] & & (a_3,b_3) \\
      (a_3,g_2(g_1(b))) \arrow[rr,equals,"\gluer\tr\gluer\sy"] \arrow[ur,equals] & &
      (a_3,b_3) \arrow[from=uu, equals, crossing over, very near start, "\mapfunc{f_2\smash g_2}(\gluer\tr\gluer\sy)"]       \arrow[ur,equals] &
    \end{tikzcd}
  \end{center}
  After canceling applications of
  $\mapfunc{h\smash k}(\gluer_z)=\gluer_{k(z)}$ on various sides of the squares (TODO).


  If $x$ varies over $\gluel_a$ the proof is very similar. Only in the end we need to fill the
  following cube instead (TODO).

  To show that this homotopy is pointed, (TODO)

\end{proof}

\begin{thm}\label{thm:smash-functor-right}
Given pointed types $A$, $B$ and $C$, the functorial action of the smash product induces a map
$$({-})\smash C:(A\pmap B)\pmap(A\smash C\pmap B\smash C)$$
which is natural in $A$, $B$ and dinatural in $C$.
\end{thm}
The naturality and dinaturality means that the following squares commute for $f : A' \to A$ $g:B\to B'$ and $h:C\to C'$.
\begin{center}
\begin{tikzcd}
(A\pmap B) \arrow[r,"({-})\smash C"]\arrow[d,"f\pmap B"] &
(A\smash C\pmap B\smash C)\arrow[d,"f\smash C\pmap B\smash C"] \\
(A'\pmap B) \arrow[r,"({-})\smash C"] &
(A'\smash C\pmap B\smash C)
\end{tikzcd}
\begin{tikzcd}
(A\pmap B) \arrow[r,"({-})\smash C"]\arrow[d,"A\pmap g"] &
(A\smash C\pmap B\smash C)\arrow[d,"A\smash C\pmap g\smash C"] \\
(A\pmap B') \arrow[r,"({-})\smash C"] &
(A\smash C\pmap B'\smash C)
\end{tikzcd}
\begin{tikzcd}[column sep=large]
(A\pmap B) \arrow[r,"({-})\smash C"]\arrow[d,"({-})\smash C'"] &
(A\smash C\pmap B\smash C)\arrow[d,"A\smash C\pmap B\smash h"] \\
(A\smash C'\pmap B\smash C') \arrow[r,"A\smash h\pmap B\smash C'"] &
(A\smash C\pmap B\smash C')
\end{tikzcd}
\end{center}
\begin{proof}
First note that $\lam{f}f\smash C$ preserves the basepoint so that the map is indeed pointed.

Let $k:A\pmap B$. Then as homotopy the naturality in $A$ becomes
$(k\o f)\smash C=k\smash C\o f\smash C$. To prove an equality between pointed maps, we need to give
a pointed homotopy, which is given by interchange. To show that this homotopy is pointed, we need to
fill the following square (after reducing out the applications of function extensinality), which follows from \autoref{lem:smash-coh}.
\begin{center}
\begin{tikzcd}
(0 \o f)\smash C \arrow[r, equals]\arrow[dd,equals] &
(0 \smash C)\o (f \smash C)\arrow[d,equals] \\
& 0 \o (f \smash C)\arrow[d,equals] \\
0\smash C \arrow[r,equals] &
0
\end{tikzcd}
\end{center}
The naturality in $B$ is almost the same: for the underlying homotopy we need to show
$(g \o k)\smash C = g\smash C \o k\smash C$. For the pointedness we need to fill the following
square, which follows from \autoref{lem:smash-coh}.
\begin{center}
\begin{tikzcd}
(g \o 0)\smash C \arrow[r, equals]\arrow[dd,equals] &
(g \smash C)\o (0 \smash C)\arrow[d,equals] \\
& (g\smash C) \o 0\arrow[d,equals] \\
0\smash C \arrow[r,equals] &
0
\end{tikzcd}
\end{center}
The dinaturality in $C$ is a bit harder. For the underlying homotopy we need to show
$B\smash h\o k\smash C=k\smash C'\o A\smash h$. This follows by applying interchange twice:
$$B\smash h\o k\smash C\sim(\idfunc[B]\o k)\smash(h\o\idfunc[C])\sim(k\o\idfunc[A])\smash(\idfunc[C']\o h)\sim k\smash C'\o A\smash h.$$
To show that this homotopy is pointed, we need to fill the following square:
\begin{center}
  \begin{tikzcd}
    B\smash h\o 0\smash C \arrow[r, equals]\arrow[d,equals] &
    (\idfunc[B]\o 0)\smash(h\o\idfunc[C]) \arrow[r, equals]\arrow[d,equals] &
    (0\o\idfunc[A])\smash(\idfunc[C']\o h)\arrow[r, equals]\arrow[d,equals] &
    0\smash C'\o A\smash h\arrow[d,equals] \\
    B\smash h\o 0 \arrow[d,equals] &
    0\smash(h\o\idfunc[C]) \arrow[r, equals]\arrow[d,equals] &
    0\smash(\idfunc[C']\o h) \arrow[d,equals] &
    0\o A\smash h\arrow[d,equals] \\
    B\smash h\o 0 \arrow[r, equals] &
    0 \arrow[r, equals] &
    0 \arrow[r, equals] &
    0
  \end{tikzcd}
\end{center}
The left and the right squares are filled by \autoref{lem:smash-coh}. The squares in the middle
are filled by (corollaries of) \autoref{lem:smash-general}.
\end{proof}

\section{Adjunction}

\begin{lem}
  There is a unit $\eta_{A,B}\equiv\eta:A\pmap B\pmap A\smash B$ natural in $A$ and counit
  $\epsilon_{B,C}\equiv\epsilon : (B\pmap C)\smash B \pmap C$ dinatural in $B$ and natural in $C$.
  These maps satisfy the unit-counit laws:
  $$(A\to\epsilon_{A,B})\o \eta_{A\to B,A}\sim \idfunc[A\to B]\qquad
  \epsilon_{B,B\smash C}\o \eta_{A,B}\smash B\sim\idfunc[A\smash B].$$
\end{lem}
Note: $\eta$ is also dinatural in $B$, but we don't need this.
\begin{proof}
  We define $\eta ab=(a,b)$. Then $\eta a$ respects the basepoint because
  $(a,b_0)=(a_0,b_0)$. Also, $\eta$ itself respects the basepoint. To show this, we need to show
  that $\eta a_0\sim0$. The underlying maps are homotopic, since $(a_0,b)=(a_0,b_0)$. To show that
  this homotopy is pointed, we need to show that the two given proofs of $(a_0,b_0)=(a_0,b_0)$ are
  equal, but they are both equal to reflexivity:
  $$\gluel_{a_0}\tr\gluel_{a_0}\sy=1=\gluer_{b_0}\tr\gluer_{b_0}\sy.$$
  This defines the unit. To define the counit, given $x:(B\pmap C)\smash B$. We construct
  $\epsilon x:C$ by induction on $x$. If $x\jdeq(f,b)$ we set $\epsilon(f,b)\defeq f(b)$. If $x$
  is either $\auxl$ or $\auxr$ then we set $\epsilon x\defeq c_0:C$. If $x$ varies over $\gluel_f$
  then we need to show that $f(b_0)=c_0$, which is true by $f_0$. If $x$ varies over $\gluer_b$ we
  need to show that $0(b)=c_0$ which is true by reflexivity. $\epsilon$ is trivially a pointed map,
  which defines the counit.

  Now we need to show that the unit and counit are (di)natural. (TODO).

  Finally we need to show the unit-counit laws. For the underlying homotopy of the first one, let
  $f:A\to B$. We need to show that $p:\epsilon\o\eta f\sim f$. For the underlying homotopy of $p$,
  let $a:A$, and we need to show that $\epsilon(f,a)=f(a)$, which is true by reflexivity. To show
  that $p$ is a pointed homotopy, we need to show that
  $p(a_0)\tr f_0=\mapfunc{\epsilon}(\eta f)_0\tr \epsilon_0$, which reduces to
  $f_0=\mapfunc{\epsilon}(\gluel_f\tr\gluel_0\sy)$, but we can reduce the right hand side: (note:
  $0_0$ denotes the proof that $0(a_0)=b_0$, which is reflexivity)
  $$\mapfunc{\epsilon}(\gluel_f\tr\gluel_0\sy)=\mapfunc{\epsilon}(\gluel_f)\tr(\mapfunc{\epsilon}(\gluel_0))\sy=f_0\tr 0_0\sy=f_0.$$
  Now we need to show that $p$ itself respects the basepoint of $A\to B$, i.e. that the composite
  $\epsilon\o\eta0\sim\epsilon\o0\sim0$ is equal to $p$ for $f\equiv 0_{A,B}$. The underlying
  homotopies are the same for $a : A$; on the one side we have
  $\mapfunc{\epsilon}(\gluer_{a}\tr\gluer_{a_0}\sy)$ and on the other side we have reflexivity
  (note: this typechecks, since $0_{A,B}a\equiv0_{A,B}a_0$). These paths are equal, since
  $$\mapfunc{\epsilon}(\gluer_{a}\tr\gluer_{a_0}\sy)=\mapfunc{\epsilon}(\gluer_{a})\tr(\mapfunc\epsilon(\gluer_{a_0}))\sy=1\cdot1\sy\equiv1.$$
  Both pointed homotopies are pointed in the same way, which requires some path-algebra, and we skip
  the proof here.

  For the underlying homotopy of the second one, we need to show for $x:A\smash B$ that
  $\epsilon(\eta\smash B(x))=x$, which we prove by induction to $x$. (TODO).

\end{proof}

\begin{defn}
The function $e\jdeq e_{A,B,C}:(A\pmap B\pmap C)\pmap(A\smash B\pmap C)$ is defined as the composite
$$(A\pmap B\pmap C)\lpmap{({-})\smash B}(A\smash B\pmap (B\pmap C)\smash B)\lpmap{A\smash B \pmap\epsilon}(A\smash B\pmap C).$$
\end{defn}

\begin{lem}
  $e$ is invertible, hence gives a pointed equivalence $$(A\pmap B\pmap C)\simeq(A\smash B\pmap C).$$
\end{lem}
\begin{proof}
  Define
  $$\inv{e}_{A,B,C}:(A\smash B\pmap C)\lpmap{B\pmap({-})}((B\pmap A\smash B)\pmap (B\pmap
  C))\lpmap{\eta\pmap(B\pmap C)}(A\pmap B\pmap C).$$ It is easy to show that $e$ and $\inv{e}$ are
  inverses as unpointed maps from the unit-counit laws and naturality of $\eta$ and $\epsilon$.

%   For $f : A\pmap B\pmap C$ we have
%   \begin{align*}
%     \inv{e}(e(f))&\equiv(\eta\pmap(B\pmap C))\o (B\pmap((A\smash B\pmap\epsilon)\of\smash B))\\
%                  &= (\eta\pmap(B\pmap C))\o (B\pmap(A\smash B\pmap\epsilon))\o(B\pmapf\smash B)\\
% %                 &= (\eta\pmap(B\pmap C))\o (B\pmap(A\smash B\pmap\epsilon))\o(B\pmapf\smash B)\\
%   \end{align*}
\end{proof}
\begin{lem}\label{e-natural}
$e$ is natural in $A$, $B$ and $C$.
\end{lem}
\begin{proof}
\textbf{$e$ is natural in $A$}. Suppose that $f:A'\pmap A$. Then the following diagram commutes. The left square commutes by naturality of $({-})\smash B$ in the first argument and the right square commutes because composition on the left commutes with composition on the right.
\begin{center}
\begin{tikzcd}
(A\pmap B\pmap C) \arrow[r,"({-})\smash B"]\arrow[d,"f\pmap B\pmap C"] &
(A\smash B\pmap (B\pmap C)\smash B) \arrow[r,"A\smash B\pmap\epsilon"]\arrow[d,"f\smash B\pmap\cdots"]  &
(A\smash B\pmap C)\arrow[d,"f\smash B\pmap C"] \\
(A'\pmap B\pmap C) \arrow[r,"({-})\smash B"] &
(A'\smash B\pmap (B\pmap C)\smash B) \arrow[r,"A\smash B\pmap\epsilon"] &
(A'\smash B\pmap C)
\end{tikzcd}
\end{center}

\textbf{$e$ is natural in $C$}. Suppose that $f:C\pmap C'$. Then in the following diagram the left square commutes by naturality of $({-})\smash B$ in the second argument (applied to $B\pmap f$) and the right square commutes by applying the functor $A\smash B \pmap({-})$ to the naturality of $\epsilon$ in the second argument.
\begin{center}
\begin{tikzcd}
(A\pmap B\pmap C) \arrow[r]\arrow[d] &
(A\smash B\pmap (B\pmap C)\smash B) \arrow[r]\arrow[d] &
(A\smash B\pmap C)\arrow[d] \\
(A\pmap B\pmap C') \arrow[r] &
(A\smash B\pmap (B\pmap C')\smash B) \arrow[r] &
(A\smash B\pmap C')
\end{tikzcd}
\end{center}

\textbf{$e$ is natural in $B$}. Suppose that $f:B'\pmap B$. Here the diagram is a bit more
complicated, since $({-})\smash B$ is dinatural (instead of natural) in $B$. Then we get the
following diagram. The front square commutes by naturality of $({-})\smash B$ in the second argument
(applied to $f\pmap C$). The top square commutes by naturality of $({-})\smash B$ in the third
argument, the back square commutes because composition on the left commutes with composition on the
right, and finally the right square commutes by applying the functor $A\smash B' \pmap({-})$ to the
naturality of $\epsilon$ in the first argument.
\begin{center}
\begin{tikzcd}[row sep=scriptsize, column sep=-4em]
& (A\smash B\pmap (B\pmap C)\smash B) \arrow[rr] \arrow[dd] & & (A\smash B'\pmap (B\pmap C)\smash B)\arrow[dd] \\
(A\pmap B\pmap C) \arrow[ur] \arrow[rr, crossing over] \arrow[dd] & & (A\smash B'\pmap (B\pmap C)\smash B') \arrow[ur] \\
& (A\smash B\pmap C)\arrow[rr] &  & (A\smash B'\pmap C) \\
(A\pmap B'\pmap C) \arrow[rr] & & (A\smash B'\pmap (B'\pmap C)\smash B') \arrow[ur] \arrow[from=uu, crossing over]
\end{tikzcd}
\end{center}

\end{proof}
\begin{rmk}
  Instead of showing that $e$ is natural, we could instead show that $e^{-1}$ is natural. In
  that case we need to show that the map $A\to({-}):(B\to C)\to(A\to B)\to(A\to C)$ is natural in
  $A$, $B$ and $C$. This might actually be easier, since we don't need to work with any higher
  inductive type to prove that.
\end{rmk}

\section{Symmetric monoidality}
We aim to prove that the smash product is a (1-coherent) symmetric monoidal product [REF: Brunerie] for pointed types, i.e., that
\[(\pType,\, \two,\, \smash,\, \alpha,\, \lambda,\, \rho,\, \gamma)\]
is a symmetric monoidal category, with the type of booleans $\two$ (pointed in $0_\two$) as unit, and for suitable instances of $\alpha$, $\lambda$, $\rho$ and $\gamma$ witnessing associativity, left- and right unitality and the braiding for $\smash$ and satisfying appropriate coherence relations (associativity pentagon; unitors triangle; braiding-unitors triangle; associativity-braiding hexagon; double braiding).

We will make use of the following lemma.
\begin{lem}[Yoneda]\label{lem:yoneda}
Let $A$, $B$ be pointed types, and assume, for all pointed types $X$, a pointed equivalence $\phi_X : (A \to X) \simeq (B \to X)$, natural in $X$, i.e. making the following diagram commute for all $f : X \to X'$:
\begin{center}
\begin{tikzcd}
(A \to X)
	\arrow[r, "\phi_X"]
	\arrow[d, swap, "f \o -"]
& (B \to X)
	\arrow[d, "f \o -"]
\\
(A \to X')
	\arrow[r, swap,"\phi_{X'}"]
& (B \to X')
\end{tikzcd}
\end{center}
Then we have a pointed equivalence $\yoneda_\phi : B \simeq A$.
\end{lem}
\begin{proof}
We define $\yoneda_\phi \defeq \phi_A(\idfunc[A]) : B \to A$ and $\yoneda_\phi\sy \defeq \phi_B\sy(\idfunc[B])$. The given naturality square for $X \defeq A$ and $g \defeq \yoneda_\phi\sy$ yields $\yoneda_\phi\sy \o \phi_A (\idfunc[A]) \judgeq \yoneda_\phi\sy \o \yoneda_\phi \sim \phi_B (\yoneda_\phi\sy \o \idfunc[A]) \judgeq \phi_B (\phi_B\sy (\idfunc[B])) \sim \idfunc[B]$, and similarly for the inverse composition.
\end{proof}

By \autoref{lem:yoneda} we can prove associativity, left- and right unitality and braiding equivalences for the smash product, in the following way.

\begin{defn}\label{def:equiv-precursors}
	The following pointed equivalences are defined for $A$, $B$, $C$ and $X$ pointed types:
	\begin{itemize}
		\item $\alphabar_X : (A \smash (B \smash C) \to X) \simeq ((A \smash B) \smash C \to X)$ as the composition of the equivalences:
			\begin{align*}
			    A \smash (B \smash C)\to X&\simeq A \to B\smash C\to X && (e\sy)\\
			    &\simeq A \to B\to C\to X && (A \to e\sy)\\
			    &\simeq A \smash B\to C\to X && (e)\\
		    	&\simeq (A \smash B)\smash C\to X. && (e)
			\end{align*}
		\item $\lambdabar_X : (B \to X) \simeq (\two \smash B \to X)$, where $\two$ is the type of booleans, as the composition of the equivalences:
			\begin{align*}
				B \to X &\simeq \two \to B \to X && (t\sy)\\
				&\simeq \two \smash B \to X && (e)
			\end{align*}
			with $t : (\two \to X) \simeq X$ the pointed equivalence, natural in $X$, sending $f : \two \to X$ to $f(1_\two) : X$;
		\item $\rhobar_X : (A \to X) \simeq (A \smash \two \to X)$ as the composition of the equivalences:
			\begin{align*}
				A \to X &\simeq A \to \two \to X && (A \to t\sy)\\
				&\simeq A \smash \two \to X && (e)
			\end{align*}
			with $t$ as above;
		\item $\gammabar_X : (B \smash A \to X) \simeq (A \smash B \to X)$ as the composition of the equivalences:
			\begin{align*}
				B \smash A \to X &\simeq B \to A \to X && (e\sy)\\
				&\simeq A \to B \to X && (c)\\
				&\simeq A \smash B \to X && (e)
			\end{align*}
			where $c : (A \to B \to X) \simeq (B \to A \to X)$ is the obvious pointed equivalence, natural in $A$, $B$ and $X$.
	\end{itemize}
\end{defn}

\begin{rmk}
	The equivalences defined in \autoref{def:equiv-precursors} are natural in all their arguments by naturality of $e$ (\autoref{e-natural}), $c$ and $t$. In particular, we will use:
	\begin{align*}
	f \o \alphabar(g) &\sim \alphabar(f \o g) & f \o \lambdabar(g) &\sim \lambdabar(f \o g)\\
	f \o \rhobar(g) &\sim \rhobar(f \o g) & f \o \gammabar(g) &\sim \gammabar(f \o g)
	\end{align*}
\end{rmk}

\begin{defn}\label{def:smash-alrg}
	We define the following equivalences, natural in all their arguments, with inverses provided as in \autoref{lem:yoneda}:
	\begin{itemize}
		\item $\alpha\defeq\alphabar_{A \smash (B \smash C)}(\idfunc) : (A \smash B) \smash C \simeq A \smash (B \smash C)$ (associativity of the smash product), with inverse $\alpha\sy\defeq\alphabar\sy_{(A \smash B) \smash C}(\idfunc)$;
		\item $\lambda \defeq \lambdabar_B(\idfunc) : \two \smash B \simeq B$ and $\rho \defeq \rhobar_A(\idfunc) : A \smash \two \simeq A$ (left- and right unitors for the smash product), with inverses $\lambda\sy\defeq \lambdabar_{\two\smash B}\sy(\idfunc)$ and $\rho\sy\defeq \rhobar_{A\smash \two}\sy(\idfunc)$, respectively;
		\item $\gamma \defeq \gammabar_{B\smash A} (\idfunc) : A \smash B \simeq B \smash A$ (braiding for the smash product), with inverse $\gamma\sy \defeq \gammabar_{A \smash B}\sy (\idfunc)$.
	\end{itemize}
	$\alpha$, $\lambda$, $\rho$ and $\gamma$ are natural in all their arguments, as $\alphabar$, $\lambdabar$, $\rhobar$ and $\gammabar$ are.
\end{defn}

\begin{thm}[Associativity pentagon]\label{thm:smash-associativity-pentagon}
	For $A$, $B$, $C$ and $D$ pointed types, there is a homotopy
	\[\alpha \o \alpha \sim (A \smash \alpha) \o \alpha \o (\alpha \smash D)\]
	making the following diagram commute:
	\begin{center}
	\begin{tikzcd}
		&((A \smash B) \smash (C \smash D))
			\arrow[dr, "\alpha"]
		\\
		(((A \smash B) \smash C) \smash D)
			\arrow[ru, "\alpha"]
			\arrow[d, swap, "\alpha \smash D"]
		&& (A \smash (B \smash (C \smash D)))
		\\
		((A \smash (B \smash C)) \smash D)
			\arrow[rr, swap, "\alpha"]
		&& (A \smash ((B \smash C) \smash D))
			\arrow[u, swap, "A \smash \alpha"]
	\end{tikzcd}
%	\begin{tikzcd}
%		(((A \smash B) \smash C) \smash D)
%			\arrow[rr, "\alpha"]
%			\arrow[d, swap, "\alpha \smash D"]
%		&& ((A \smash B) \smash (C \smash D))
%			\arrow[d, "\alpha"]
%		\\
%		((A \smash (B \smash C)) \smash D)
%			\arrow[r, swap, "\alpha"]
%		& (A \smash ((B \smash C) \smash D))
%			\arrow[r, swap, "A \smash \alpha"]
%		& (A \smash (B \smash (C \smash D)))
%	\end{tikzcd}
	\end{center}
\end{thm}
\begin{proof}
	We articulate the proof in several steps. A map homotopic to both sides of the sought homotopy will be constructed via the equivalence
	\begin{align*}	
		\alphabar^4 : (A \smash (B \smash (C \smash D)) \to X) &\simeq (((A \smash B) \smash C) \smash D \to X)
		\intertext{(natural in all its arguments), defined as the composite:}
		A \smash (B \smash (C \smash D)) \to X
		&\simeq A \to B \smash (C \smash D) \to X && \text{($e\sy$)}\\
		&\simeq A \to B \to C \smash D \to X &&\text{($A \to e\sy$)}\\
		&\simeq A \to B \to C \to D \to X &&\text{($A \to B \to e\sy$)}\\
		&\simeq A \smash B \to C \to D \to X &&\text{($e$)}\\
		&\simeq (A \smash B) \smash C \to D \to X &&\text{($e$)}\\
		&\simeq ((A \smash B) \smash C) \smash D \to X && \text{($e$)}
		\intertext{giving $\alphabar^4(\idfunc) : ((A \smash B) \smash C) \smash D) \simeq A \smash (B \smash (C \smash D))$. Moreover, in order to simplify the expressions of $\alpha \smash D$ and $A \smash \alpha$, we also define:}
		\alphabar^R : ((A \smash (B \smash C)) \smash D \to X) &\simeq (((A \smash B) \smash C) \smash D \to X)
		\intertext{as the composite:}
		(A \smash (B \smash C)) \smash D \to X
		&\simeq A \smash (B \smash C) \to D \to X &&\text{($e\sy$)}\\
		&\simeq (A \smash B) \smash C \to D \to X &&\text{($\alphabar$)}\\
		&\simeq ((A \smash B) \smash C) \smash D \to X &&\text{($e$)}
		\intertext{and}
		\alphabar^L : (A \smash (B \smash (C \smash D)) \to X) &\simeq (A \smash ((B \smash C) \smash D) \to X)
		\intertext{as the composite:}
		A \smash (B \smash (C \smash D)) \to X
		&\simeq A \to B \smash (C \smash D) \to X &&\text{($e\sy$)}\\
		&\simeq A \to (B \smash C) \smash D \to X &&\text{($A \to \alphabar$)}\\
		&\simeq A \smash ((B \smash C) \smash D) \to X &&\text{($e$)}
	\end{align*}
	also natural in their arguments. Evaluating these equivalences to the identity function, we get new arrows that fit in the original diagram:
	\begin{center}
	\begin{tikzcd}
		&((A \smash B) \smash (C \smash D))
			\arrow[dr, "\alpha"]
		\\
		(((A \smash B) \smash C) \smash D)
			\arrow[ru, "\alpha"]
			\arrow[d, swap, "\alpha \smash D"]
			\arrow[d, bend left=40, "\alphabar^R(\idfunc)"]
			\arrow[rr, "\alphabar^4(\idfunc)"]
		&& (A \smash (B \smash (C \smash D)))
		\\
		((A \smash (B \smash C)) \smash D)
			\arrow[rr, swap, "\alpha"]
		&& (A \smash ((B \smash C) \smash D))
			\arrow[u, swap, "A \smash \alpha"]
			\arrow[u, bend left=40, "\alphabar^L(\idfunc)"]
	\end{tikzcd}
	\end{center}
	The theorem is then proved once we show the chain of homotopies:
	\[
	\alpha \o \alpha
	\sim \alphabar^4(\idfunc)
	\sim \alphabar^L(\idfunc) \o \alpha \o \alphabar^R(\idfunc)
	\sim (A \smash \alpha) \o \alpha \o (\alpha \smash D)
	\]
	[CAN'T INSERT NUMBERING HERE]	
	
	To verify the first homotopy in [NUMBER]:
	\begin{align*}
		\alpha \o \alpha
		&\judgeq \alphabar(\idfunc) \o \alphabar(\idfunc)\\
		&\sim (\alphabar \o \alphabar) (\idfunc) &&\text{(naturality of $\alphabar$)}\\
		&\judgeq (e \o e \o (A \to e\sy) \o e\sy \o e \o e \o (A \to e\sy) \o e\sy)(\idfunc)\\
		&\sim (e \o e \o (A \to e\sy) \o e \o (A \to e\sy) \o e\sy)(\idfunc) &&\text{(cancelling)}\\
		&\sim (e \o e \o e \o (B \to A \to e\sy) \o (A \to e\sy) \o e\sy)(\idfunc) &&\text{(naturality of $e$)}\\
		&\judgeq \alphabar^4(\idfunc)
	\end{align*}		

	The second homotopy in [NUMBER] is verified by (right-to-left):
	\begin{align*}
		\alphabar^L(\idfunc) \o \alpha \o \alphabar^R(\idfunc)
		&\judgeq \alphabar^L(\idfunc) \o \alphabar(\idfunc) \o \alphabar^R(\idfunc)\\
		&\sim (\alphabar^R \o \alphabar \o \alphabar^L)(\idfunc) &&\text{(nat. of $\alphabar$ and $\alphabar^R$)}\\
		&\judgeq (e \o \alphabar \o e\sy \o e \o e \o (A \to e\sy) \o e\sy \o e \o (A \to \alphabar) \o e\sy)(\idfunc)\\
		&\sim (e \o \alphabar \o e \o (A \to e\sy) \o (A \to \alphabar) \o e\sy)(\idfunc) &&\text{(cancelling)}\\
		&\sim (e \o \alphabar \o e \o (A \to (e\sy \o \alphabar)) \o e\sy)(\idfunc) &&\text{(funct. of $A\to -$)}\\
		&\judgeq (e \o e \o e \o (A \to e\sy) \o e\sy \o e \\
		&\hspace{3em}\o (A \to (e\sy \o e \o e \o (B \to e\sy) \o e\sy)) \o e\sy)(\idfunc)\\
		&\sim (e \o e \o e \o (A \to ((B \to e\sy) \o e\sy)) \o e\sy)(\idfunc) &&\text{(cancelling)}\\
		&\sim (e \o e \o e \o (B \to A \to e\sy) \o (A \to e\sy) \o e\sy)(\idfunc) &&\text{(funct. of $A \to -$)}\\
		&\judgeq \alphabar^4(\idfunc)
	\end{align*}
	
	In order to prove the last homotopy in [NUMBER], it is sufficient to show that $\alphabar^R(\idfunc) \sim \alpha \smash D$ and that $\alphabar^L(\idfunc) \sim A \smash \alpha$. We have:
	\begin{align*}
		\alphabar^R(\idfunc)
		&\judgeq e(\alphabar (e\sy(\idfunc)))\\
		&\sim e (\alphabar (\eta)) &&\text{(unit-counit)}\\
		&\sim e (\eta \o \alphabar(\idfunc)) &&\text{(naturality of $\alphabar$)}\\
		&\judgeq \epsilon \o (\eta \o \alpha) \smash D\\
		&\sim \epsilon \o (\eta \smash D) \o (\alpha \smash D) &&\text{(distrib. of $\smash$)}\\
		&\sim \alpha \smash D &&\text{(unit-counit)}
	\end{align*}
	and, lastly,
	\begin{align*}
		\alphabar^L(\idfunc)
		&\judgeq e(\alphabar \o e\sy(\idfunc))\\
		&\sim e(\alphabar \o \eta) &&\text{(unit-counit)}\\
		&\sim e((\alpha \to A \smash (B \smash (C \smash D))) \o \eta) &&\text{($\alphabar_X \sim (\alpha \to X)$)}\\
		&\sim e((B \smash (C \smash D) \to A \smash \alpha) \o \eta) &&\text{(dinaturality of $\eta$)}\\
		&\sim (A \smash \alpha) \o e(\eta) &&\text{(naturality of $e$)}\\
		&\sim A \smash \alpha &&\text{(unit-counit)}
	\end{align*}
	thus proving the desired homotopy.
\end{proof}

\begin{thm}[Unitors triangle]\label{thm:smash-unitors-triangle}
	For $A$ and $B$ pointed types, there is a homotopy
	\[(A \smash \lambda) \o \alpha \sim (\rho \smash B)\]
	making the following diagram commute:
	\begin{center}
	\begin{tikzcd}
	((A \smash \two) \smash B)
		\arrow[rr, "\alpha"]
		\arrow[dr, swap, "\rho \smash B"]
	&& (A \smash (\two \smash B))
		\arrow[dl, "A \smash \lambda"]
	\\
	& (A \smash B)
	\end{tikzcd}
	\end{center}
\end{thm}
\begin{proof}
	By an argument similar to the one for $\alphabar^L$ and $\alphabar^R$ in \autoref{thm:smash-associativity-pentagon}, one can verify the homotopies $A \smash \lambda \sim (e \o (A \to \lambdabar) \o e\sy)(\idfunc)$ and $\rho \smash B \sim (e \o \rhobar \o e)(\idfunc)$, simplifying the expressions in the sought homotopy. Then:
	\begin{align*}
		(A \smash \lambda) \o \alpha
		&\sim e(\lambdabar \o e\sy(\idfunc)) \o \alphabar(\idfunc) &&\text{(simplification)}\\
		&\sim \alphabar(e(\lambdabar \o e\sy(\idfunc)) &&\text{(naturality of $\alphabar$)}\\
		&\judgeq e(e(e\sy \o e\sy (e(\lambdabar \o e\sy(\idfunc)))))\\
		&\sim e(e(e\sy \o \lambdabar \o e\sy(\idfunc))) &&\text{(cancelling)}\\
		&\judgeq e(e(e\sy \o e \o t\sy \o e\sy(\idfunc)))\\
		&\sim e(e(t\sy \o e\sy(\idfunc))) &&\text{(cancelling)}\\
		&\judgeq (e \o \rhobar \o e\sy)(\idfunc)\\
		&\sim \rho \smash B &&\text{(simplification)}
	\end{align*}
	gives the desired homotopy.
\end{proof}

\begin{thm}[Braiding-unitors triangle]\label{thm:smash-braiding-unitors}
	For a pointed type $A$, there is a homotopy
	\[\lambda \o \gamma \sim \rho\]
	making the following diagram commute:
	\begin{center}
	\begin{tikzcd}
	(A \smash \two)
		\arrow[rr, "\gamma"]
		\arrow[dr, swap, "\rho"]
	&& (\two \smash A)
		\arrow[dl, "\lambda"]
	\\
	& A
	\end{tikzcd}
	\end{center}
\end{thm}
\begin{proof}
	We have:
	\begin{align*}
		\lambda \o \gamma
		&\judgeq \lambdabar(\idfunc) \o \gammabar(\idfunc)\\
		&\sim (\gammabar \o \lambdabar)(\idfunc) &&\text{(naturality of $\gammabar$)}\\
		&\judgeq (e \o c \o e\sy \o e \o t\sy)(\idfunc)\\
		&\sim (e \o c \o t\sy)(\idfunc) &&\text{(cancelling)}\\
		&\sim (e \o (A \to t\sy))(\idfunc)\\
		&\judgeq \rhobar(\idfunc) \judgeq \rho
	\end{align*}		
	where the last homotopy is given by $(A \to c) \o t \sim c : (\two \to A \to X) \to (A \to X)$.
\end{proof}

\begin{lem}\label{lem:pentagon-c}
	The following diagram commutes, for $A$, $B$, $C$ and $X$ pointed types:
	\begin{center}
	\begin{tikzcd}
		(B \to C \to A \to X)
			\arrow[rr, "B\to c"]
			\arrow[d, swap, "e"]
		&& (B \to A \to C \to X)
			\arrow[d, "c"]
		\\
		(B \smash C \to A \to X)
			\arrow[r, swap, "c"]
		& (A \to B \smash C \to X)
			\arrow[r, swap, "A \to e\sy"]
		& (A \to B \to C \to X)
	\end{tikzcd}
	\end{center}
\end{lem}

\begin{thm}[Associativity-braiding hexagon]\label{thm:smash-associativity-braiding}
	For pointed types $A$, $B$ and $C$, there is a homotopy
	\[\alpha \o \gamma \o \alpha \sim (B \smash \gamma) \o \alpha \o (\gamma \smash C)\]
	making the following diagram commute:
	\begin{center}
	\begin{tikzcd}
		((A \smash B) \smash C)
			\arrow[r, "\alpha"]
			\arrow[d, swap, "\gamma \smash C"]
		&(A \smash (B \smash C))
			\arrow[r, "\gamma"]
		& ((B \smash C) \smash A)
			\arrow[d, "\alpha"]
		\\
		((B \smash A) \smash C))
			\arrow[r, swap, "\alpha"]
		& (B \smash (A \smash C))
			\arrow[r, swap, "B \smash \gamma"]
		& (B \smash (C \smash A))
	\end{tikzcd}
	\end{center}
\end{thm}
\begin{proof}
	The proof is structured similarly to the one for \autoref{thm:smash-associativity-pentagon}: the homotopies
	\begin{align*}
	B \smash \gamma &\sim \gammabar^L(\idfunc) &\text{with\ \ } \gammabar^L &\defeq e \o (B \to \gammabar) \o e\sy\\
	\gamma \smash C &\sim \gammabar^R(\idfunc) &\text{with\ \ } \gammabar^R &\defeq e \o \gammabar \o e\sy
	\end{align*}		
	can be proven in exactly the same way and, using these simplifications, we will show that both sides of the sought homotopy are homotopic to the same equivalence. Indeed we have:
	\begin{align*}
		\alpha \o \gamma \o \alpha
		&\judgeq \alphabar(\idfunc) \o \gammabar(\idfunc) \o \alphabar(\idfunc)\\
		&\sim (\alphabar \o \gammabar \o \alphabar)(\idfunc) &&\text{(naturality of $\gammabar$ and $\alphabar$)}\\
		&\judgeq (e \o e \o (A \to e\sy) \o e\sy \o e \o c \o e\sy \o e \o e \o (B \to e\sy) \o e\sy)(\idfunc)\\
		&\sim (e \o e \o (A \to e\sy) \o c \o e \o (B \to e\sy) \o e\sy)(\idfunc) &&\text{(cancelling)}\\
		&\sim (e \o e \o c \o (B \to c) \o (B \to e\sy) \o e\sy)(\idfunc) &&\text{(\autoref{lem:pentagon-c})}
	\end{align*}
	and
	\begin{align*}
		(B \smash \gamma) \o \alpha \o (\gamma \smash C)
		&\sim \gammabar^L(\idfunc) \o \alphabar \o \gammabar^R(\idfunc) &&\text{(simplification)}\\
		&\sim (\gammabar^R \o \alphabar \o \gammabar^L)(\idfunc) &&\text{(naturality of $\alphabar$ and $\gammabar^R$)}\\
		&\judgeq (e \o \gammabar \o e\sy \o e \o e \o (B \to e\sy) \o e\sy \o e \o (B \to \gammabar) \o e\sy)(\idfunc)\\
		&\sim (e \o \gammabar \o e \o (B \to e\sy) \o (B \to \gammabar) \o e\sy)(\idfunc) &&\text{(cancelling)}\\
		&\sim (e \o \gammabar \o e \o (B \to (e\sy \o \gammabar)) \o e\sy)(\idfunc) &&\text{(funct. of $B \to -$)}\\
		&\judgeq (e \o e \o c \o e\sy \o e \o (B \to (e\sy \o e \o c \o e\sy)) \o e\sy)(\idfunc)\\
		&\sim (e \o e \o c \o (B \to c) \o (B \to e\sy) \o e\sy)(\idfunc) &&\text{(cancelling)}
	\end{align*}
	proving commutativity of the diagram.
\end{proof}

\begin{thm}[Double braiding]\label{thm:smash-double-braiding}
	For $A$ and $B$ pointed types, there is a homotopy
	\[\gamma \o \gamma \sim \idfunc\]
	making the following diagram commute:
	\begin{center}
	\begin{tikzcd}
	(A \smash B)
		\arrow[r, "\gamma"]
		\arrow[dr, equals]
	& (B \smash A)
		\arrow[d, "\gamma"]
	\\
	& (A \smash B)
	\end{tikzcd}
	\end{center}
\end{thm}
\begin{proof}
	Using that $c \o c \sim \idfunc$, we get:
	\begin{align*}
		\gamma \o \gamma
		&\judgeq \gammabar(\idfunc) \o \gammabar(\idfunc)\\
		&\sim (\gammabar \o \gammabar)(\idfunc) &&\text{(naturality of $\gammabar$)}\\
		&\judgeq (e \o c \o e\sy \o e \o c \o e\sy)(\idfunc)\\
		&\sim \idfunc &&\text{(cancelling)}
	\end{align*}
	as desired.
\end{proof}

\begin{cor}
	$(\pType,\, \two,\, \smash,\, \alpha,\, \lambda,\, \rho,\, \gamma)$ has a structure of a symmetric monoidal category, for $\alpha$, $\lambda$, $\rho$ and $\gamma$ as in \autoref{def:smash-alrg}.
\end{cor}
\begin{proof}
	Follows by the theorems in this section.
\end{proof}


\section{Notes on the formalization}

The order of arguments are different in the formalization here and there.
Also, some smashes are commuted. This is because some unfortunate choices have been made in the formalization. Reversing these choices is possible, but probably more work than it's worth (the final result is exactly the same).

\end{document}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{thm}[Associativity]\label{thm:smash-associativity}
  The smash product is associative: there is an equivalence $\alpha : (A \smash B) \smash C \simeq A \smash (B \smash C)$ which is natural in $A$, $B$ and $C$.
\end{thm}
\begin{proof}
  For a pointed type $X$, let $\alphabar_X$ be the composite of the following equivalences:
  \begin{align*}
    A \smash (B \smash C)\to X&\simeq A \to B\smash C\to X && (e\sy)\\
    &\simeq A \to B\to C\to X && (A \to e\sy)\\
    &\simeq A \smash B\to C\to X && (e)\\
    &\simeq (A \smash B)\smash C\to X. && (e)
  \end{align*}
  $\alphabar_X$ is natural in $A,B,C,X$ by repeatedly applying \autoref{e-natural}. Let
  $\alpha\defeq\alphabar_{A \smash (B \smash C)}(\idfunc)$ and
  $\alpha\sy\defeq\alphabar\sy_{(A \smash B) \smash C}(\idfunc)$. These maps are inverses by \autoref{lem:yoneda}; lastly, $\alpha$ is natural in $A$, $B$
  and $C$, since $\alphabar_X$ is.
\end{proof}

\begin{thm}[Unitors]\label{thm:smash-unitors}
	The type of booleans $\two$ is a left- and right unit for the smash product: there are equivalences
	$\lambda : (\two \smash B) \simeq B$ and $\rho : (A \smash \two) \simeq A$, respectively natural in $B$ and in $A$.
\end{thm}
\begin{proof}
	We define $\lambdabar_X$ as the following composition of equivalences:
	\begin{align*}
		B \to X &\simeq \two \to B \to X && (t\sy)\\
			&\simeq \two \smash B \to X && (e)
		\end{align*}
	and, similarly, $\rhobar_X$ as the composition:
	\begin{align*}
		A \to X &\simeq A \to \two \to X && (A \to t\sy)\\
			&\simeq A \smash \two \to X && (e)
	\end{align*}
	for any pointed type $X$, where $t : (\two \to X) \simeq X$ is the pointed equivalence with underlying function sending $f : \two \to X$ to $f(1_\two) : X$. Both $\lambdabar_X$ and $\rhobar_X$ are natural in their arguments by multiple applications of \autoref{e-natural}. By an argument similar to \autoref{thm:smash-associativity}, we can define $\lambda \defeq \lambdabar_B(\idfunc)$ and $\rho \defeq \rhobar_A(\idfunc)$ together with the corresponding inverses, yielding the sought natural equivalences.
\end{proof}

\begin{thm}[Braiding]\label{thm:smash-braiding}
	The smash product is symmetric, i.e. there are equivalences $\gamma : A \smash B \simeq B \smash A$, natural in $A$ and $B$.
\end{thm}
\begin{proof}
	We define $\gammabar_X$, for $X$ a pointed type, as the composition of the following equivalences:
	\begin{align*}
		B \smash A \to X &\simeq B \to A \to X && (e\sy)\\
			&\simeq A \to B \to X && (c)\\
			&\simeq A \smash B \to X && (e)
	\end{align*}
	where $c : (A \to B \to X) \simeq (B \to A \to X)$ is the obvious pointed equivalence, natural in $A$, $B$ and $X$. $\gamma_X$ is then also natural in all its arguments, by myltiple applications of \autoref{e-natural}; then, as in \autoref{thm:smash-associativity}, we can define $\gamma \defeq \gammabar_{B\smash A} (\idfunc)$ and $\gamma\sy \defeq \gammabar_{A \smash B}\sy (\idfunc)$
\end{proof}