\[\two : (\bool\to X)\simeq X\] where $\bool$ is the type of booleans (pointed in $0_\bool$) with underlying map defined with $\two(f)\defeq f(1_\bool)$, and
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').$$
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:
\item\textbf{pointed (strong) naturality} will refer to the same pointed homotopy, with the additional condition that $p_\theta(0)=(p_\theta)_0$, where
is the canonical proof of the pointed homotopy $G(0)\o\theta_A \sim\theta_B \o F(0)$, whereas \textbf{pointed weak naturality} will refer to the corresponding non-pointed condition.
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.
Let $A$, $B$ be pointed types, and assume, for all pointed types $X$, a pointed equivalence $\phi_X : (B \to X)\simeq(A \to X)$, natural in $X$, i.e. for all $f : X \to X'$ there is a homotopy \[ p_\phi(f) : (A \to f)\o\phi_X \sim\phi_X' \o(B \to f)\]
% making the following diagram commute for all $f : X \to X'$:
% \begin{center}
% \begin{tikzcd}
% (B \to X)
% \arrow[r, "\phi_X"]
% \arrow[d, swap, "f \o -"]
% & (A \to X)
% \arrow[d, "f \o -"]
% \\
% (B \to X')
% \arrow[r, swap,"\phi_{X'}"]
% & (A \to X')
% \end{tikzcd}
% \end{center}
Then there exists a pointed equivalence $\psi_\phi : A \simeq B$.
\end{lem}
\begin{proof}
We define $\psi_\phi\defeq\phi_B(\idfunc[B]) : A \to B$ and $\psi_\phi\sy\defeq\phi_A\sy(\idfunc[A])$. The given naturality square for $X \defeq B$ and $g \defeq\psi_\phi\sy$ yields $\psi_\phi\sy\o\phi_B (\idfunc[B])\judgeq\psi_\phi\sy\o\psi_\phi\sim\phi_A (\psi_\phi\sy\o\idfunc[B])\judgeq\phi_A (\phi_A\sy(\idfunc[A]))\sim\idfunc[A]$, and similarly for the inverse composition.
\end{proof}
\begin{lem}\label{lem:yoneda-pointed}
Assume $A$, $B$, $\phi_X$ and $p$ as in \autoref{lem:yoneda}, and assume moreover that $\phi_X$ is pointed natural. Then there is a pointed homotopy $(\psi_\phi\to X)\sim\phi_X$.
\end{lem}
\begin{proof}
Let $f : B \to X$. The underlying homotopy is obtained by:
where the top-left expression is definitionally equal to $0\o\phi_X(\idfunc)$, the horizontal path comes from the underlying homotopy and $(\phi_X)_0$ is the canonical path from $\phi_X(0)$ to $0$. Since $\phi_X$ is pointed natural, we have that
$p_{\phi_X}(0)(\idfunc)=(p_{\phi_X})_0(\idfunc)$, which, in this case, is:
functions is the identity function. Moreover, if $p:f\sim f'$ and $q:g\sim g'$ then $p\smsh q:f\smsh g\sim f'\smsh g'$; this operation preserves reflexivities, symmetries and transitivies. We will write $p \smsh g$ or $f \smsh q$ if one of the homotopies is reflexivity.
Let us denote the basepoints of $A_i$ and $B_i$ with $a_i$ and $b_i$ respectively. We first apply induction on the paths that all the maps in the statement respect the basepoint. We verify the underlying homotopy of $i$ by induction on terms $x$ of the domain $A_1\smsh B_1$ of the two maps; this can be defined on point constructors $(a,b)$, $\auxl$ and $\auxr$ to be the identity path. If $x$ varies over $\gluel_a$, we need to fill the following square:
Since we assumed that ${(g_1)}_0$ and ${(g_2)}_0$ are the identity path, the claim is easily verified. The case for $x$ varying over $\gluer_b$ is entirely analogous, giving the square:
The resulting homotopy is pointed, as $i(a_1,b_1)\judgeq1$ and the proofs that the two maps respect the basepoint are assumed to be the identity path.
\end{proof}
\begin{lem}\label{lem:smash-zero}
There are homotopies
\begin{align*}
t_g : 0\smsh g\sim 0 && t'_f : f\smsh0\sim0
\end{align*}
such that the following diagrams
commute for given homotopies $p : g\sim g'$ and $q : f\sim f'$.
\begin{equation}\label{eq:t-triangles}
\begin{tikzcd}
0\smsh g
\arrow[rr, equals,"1\smsh p"]
\arrow[dr,equals,swap,"t_g"]
&& 0\smsh g'\arrow[dl,equals,"t_{g'}"]
&f\smsh 0
\arrow[rr, equals,"q\smsh 1"]
\arrow[dr,equals,swap, "t'_f"]
&& f'\smsh 0\arrow[dl,equals,"t'_{f'}"]
\\
& 0
&&& 0
\end{tikzcd}
% \qquad\qquad
% \begin{tikzcd}
% f\smsh 0
% \arrow[rr, equals,"q\smsh 1"]
% \arrow[dr,equals,swap, "t'_f"]
% && f'\smsh 0\arrow[dl,equals,"t'_{f'}"]
% \\
% & 0
% \end{tikzcd}
\end{equation}
\end{lem}
\begin{proof}
We will define the homotopy $t_g : 0\smsh g$, with $0 : A_1\to A_2$ and $g : B_1\to B_2$ (with the notational convention for the basepoints as in \autoref{lem:interchange}); the definition for $t'_f$ is analogous. First, we apply induction on the path that $g$ respects the basepoint. The underlying homotopy of $t_g$ is given by induction on terms $x : A_1\smsh B_1$. On point constructors, we define:
The squares in (\ref{eq:t-gluel}) and (\ref{eq:t-gluer}) can both be filled by simple path algebra. The resulting homotopy is pointed, as $t_g(a_1,b_1)$ is equal to the identity path and the proof that $g$ respects the basepoint is also assumed to be the identity path. Finally, for $p : g \sim g'$, the diagram on the left in (\ref{eq:t-triangles}) commutes by induction on $p$.
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)\smsh(g_2\o g_1)\sim0$, one which uses the interchange law and one which does not. These two homotopies are equal. Specifically, the following two diagrams commute:
$x\equiv(a,b)$ for $a:A_1$ and $b:B_1$. With the notational convention for basepoints as in \autoref{lem:interchange}, we have to fill the square (we use that the paths that the maps respect the basepoints are reflexivity):
Now $\mapfunc{h\smsh 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. For the other point constructors, the squares to fill are similar: if $x \judgeq\auxl$, we have:
which we can fill, as the path on the bottom is definitionally equal to $\gluel_{a_3}\sy$ (as we applied path induction on the path that $f_2$ respects the basepoint) and the path on the right also reduces to $\gluel_{a_3}\sy$ using that $\mapfunc{h\smsh k}(\gluel_z)=\gluel_{h(z)}$. Similarly, we can fill the square for $x \judgeq\auxr$, which is:
If $x$ varies over $\gluel_a$, after some reductions, we need to fill the following cube, where the front and the back are the squares in (\ref{eq:pent-left-ab}) for $(a,b_1)$ and (\ref{eq:pent-left-auxl}) respectively; the left square is degenerate; the other three sides are the squares in the definition of $i$ and $t$ to show that they respect $\gluel_a$ (given in (\ref{eq:i-gluel}) and (\ref{eq:t-gluel}) respectively), where we also apply $f_2\smsh g_2$ to the square on the right. We suppress in the diagram the arguments of $\gluer$ in $\gluer\tr\gluer\sy$ (which match, so the concatenation results equal to the identity path).
Similarly, if $x$ varies over $\gluer_b$, we need to fill the cube below: the front and the back are the squares in (\ref{eq:pent-left-ab}) for $(a_1,b)$ and (\ref{eq:pent-left-auxr}) respectively; the left square is again degenerate; the other three sides come from the fact that $i$ and $t$ respect $\gluer_b$ (given in (\ref{eq:i-gluer}) and (\ref{eq:t-gluer}) respectively). Again, we omit the arguments of $\gluer$ in $\gluer\tr\gluer\sy$ (in this case, not a priori judgementally equal).
In order to fill the cubes in (\ref{eq:pent-left-gluel}) and (\ref{eq:pent-left-gluer}), we generalize the paths and fill the cubes by path induction. The cube in (\ref{eq:pent-left-gluel}) can be generalized to a cube:
\begin{center}
\begin{tikzcd}[column sep=3em]
& h(y)
\arrow[rr, equals,"1"]
\arrow[dd, swap, equals, near end,"1"]
&& h(y)
\arrow[dd,equals,"\mapfunc{h}(p_l\sy)"]
\\
h(x)
\arrow[rr, equals, near end, crossing over, "1"]
\arrow[dd, swap, equals, "1"]
\arrow[ur, equals, "q_l"]
&& h(x)
\arrow[ur, equals, near start, "\mapfunc{h}(p_l)"]
\\
& h(y)
\arrow[rr, swap, equals, near start, "q_l\sy"]
&& h(x)
\\
h(x)
\arrow[rr, swap, equals,"q_r\tr q_r\sy"]
\arrow[ur, equals, "q_l"]
&& h(x)
\arrow[from=uu, equals, crossing over, near start, "\mapfunc{h}(p_r\tr p_r\sy)"]
\arrow[ur, swap, equals, "1"]
\end{tikzcd}
\end{center}
for $X$ and $X'$ pointed types; a map $h : X \to X'$; terms $x$, $y$$z : X$; paths $p_l : x = y$, $p_r : x = z$, $q_l : h(x)= h(y)$, $q_r : h(x)= h(z)$; and 2-paths $s_l : \mapfunc{h}(p_l)= q_l$ (for the back and the top) and $s_r : \mapfunc{h}(p_r)= q_r$ (for the right side). This cube is filled by path induction on $s_l$, $s_r$, $p_l$ and $p_r$. The cube in (\ref{eq:pent-left-gluer}) can be generalized to a similar cube:
for paths $p_l : x = y$, $p_b : y = z$, $q_l : h(x)= h(y)$, $q_b : h(y)= h(z)$ and for 2-paths $s_l : \mapfunc{h}(p_l)= q_l$ (for the top) and $s_b : \mapfunc{h}(p_b)= q_b$ (for the back).
To show that this naturality is pointed, we need to show that if $g=0$ then this homotopy is the same as the concatenation of the following pointed homotopies:
$$q:({-})\smsh C \circ(A \to0)\sim({-})\smsh C \circ0\sim0\sim0\circ({-})\smsh C\sim0\smsh B \circ({-})\smsh C.$$
To show that the underlying homotopies are the same, we need to show that $i(0,f,\idfunc[C],\idfunc[C])$ is equal to the following concatenation of pointed homotopies
$$q(f):(0\circ f)\smsh C\sim0\smsh C \sim0\sim0\circ f\smsh C\sim0\smsh B \circ f\smsh C,$$
which is the right pentagons in \autoref{lem:smash-coh}.
To show that these pointed homotopies respect the basepoint in the same way, we need to show that (TODO)
``$R\mathrel\square(0\smsh C \circ t)\cdot q_0=L$ where $L$ and $R$ are the left and right pentagons applied to $0$ and $\square$ is whiskering.''
We define $\eta ab=(a,b)$. We define the path that $\eta a$ respects the basepoint as
$$(\eta a)_0\defeq\gluel_a\tr\gluel_{a_0}\sy:(a,b_0)=(a_0,b_0).$$ Also, $\eta$ itself respects the basepoint. To show this, we need to give $\eta_0:\eta(a_0)\sim0$. The underlying maps are homotopic, by $$\eta_0b\defeq\gluer_b\cdot\gluer_{b_0}\sy:(a_0,b)=(a_0,b_0).$$ To show that
This defines the unit. To show that it is natural in $A$, we need to give the following pointed homotopy $p_\eta(f)$ for $f:A\to A'$.
\begin{center}
\begin{tikzcd}
A \arrow[r,"\eta"]\arrow[d,"f"]&
(B\pmap A \smsh B)\arrow[d,"B\to f\smsh B"]\\
A' \arrow[r,"\eta"]&
(B\pmap A'\smsh B)
\end{tikzcd}
\end{center}
We may assume that $f_0$ is reflexivity. For the underlying homotopy we need to define for $a:A$ that $p_\eta(f,a):\eta(fa)\sim f\smsh B \circ\eta a$, which is another pointed homotopy. For $b:B$ we have $\eta(fa,b)\equiv(fa,b)\equiv(f\smsh B)(\eta ab).$
The homotopy $p_\eta(f,a)$ is pointed, since $$(f\smsh B \circ\eta a)_0=\apfunc{f\smsh B}(\gluel_a\cdot\gluel_{a_0}\sy)=\gluel_{fa}\cdot\gluel_{a_0'}\sy=(\eta(fa))_0.$$
Now we need to show that $p_\eta(f)$ is pointed, for which we need to fill the following diagram.
$f:A\to B$. We need to show that $p_f:\epsilon\o\eta f\sim f$. We define $p_f(a)=1:\epsilon(f,a)=f(a)$. To show that $p_f$ is a pointed homotopy, we need to show that
$p_f(a_0)\tr f_0=\mapfunc{\epsilon}(\eta f)_0\tr\epsilon_0$, which reduces to
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 unit-counit law, we need to show for $x:A\smsh B$ that
$q(x):\epsilon((\eta\smsh B)x)=x$, which we prove by induction to $x$. If $x\equiv(a,b)$ then we can define $q(a,b)\defeq1_{(a,b)}$. If $x$ is $\auxl$ or $\auxr$ then the left-hand side reduces to $(a_0,b_0)$, so we can define $q(\auxl)\defeq\gluel_{a_0}$ and $q(\auxr)\defeq\gluer_{b_0}$. The following computation shows that $q$ respects $\gluel_a$:
To show that $q$ is a pointed homotopy, we need to show that $(\epsilon\circ\eta\smsh B)_0=1$, For this we compute $$(\epsilon\circ\eta\smsh B)_0=\apfunc{\epsilon({-},b_0)}(\eta_0)=\eta_0b_0=\gluer_{b_0}\cdot\gluer_{b_0}\sy=1.$$
\textbf{Naturality of $e$ in $A$}. Suppose that $f:A'\pmap A$. Then the following diagram commutes. The left square commutes by naturality of $({-})\smsh 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,"({-})\smsh B"]\arrow[d,"f\pmap B\pmap C"]&
(A\smsh B\pmap (B\pmap C)\smsh B) \arrow[r,"A\smsh B\pmap\epsilon"]\arrow[d,"f\smsh B\pmap\cdots"]&
(A\smsh B\pmap C)\arrow[d,"f\smsh B\pmap C"]\\
(A'\pmap B\pmap C) \arrow[r,"({-})\smsh B"]&
(A'\smsh B\pmap (B\pmap C)\smsh B) \arrow[r,"A\smsh B\pmap\epsilon"]&
\textbf{Naturality of $e$ in $C$}. Suppose that $f:C\pmap C'$. Then in the following diagram the left square commutes by naturality of $({-})\smsh B$ in the second argument (applied to $B\pmap f$) and the right square commutes by applying the functor $A\smsh 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\smsh B\pmap (B\pmap C)\smsh B) \arrow[r]\arrow[d]&
is a symmetric monoidal category, with the type of booleans $\bool$ (pointed in $0_\bool$) as unit, and for suitable instances of $\alpha$, $\lambda$, $\rho$ and $\gamma$ witnessing associativity, left- and right unitality and the braiding for $\smsh$ and satisfying appropriate coherence relations (associativity pentagon; unitors triangle; braiding-unitors triangle; associativity-braiding hexagon; double braiding).
Using \autoref{lem:yoneda} (Yoneda) we can prove associativity, left- and right unitality and braiding equivalences for the smash product, in the following way.
The equivalences in \autoref{def:equiv-precursors} are natural in all their arguments and pointed natural in $X$, by (pointed) naturality of $e$ (\autoref{lem:e-natural} and \autoref{lem:e-pointed-natural}), $c$ and $t$. In particular, we will use:
\item$\alpha\defeq\alphabar_{A \smsh(B \smsh C)}(\idfunc) : (A \smsh B)\smsh C \simeq A \smsh(B \smsh C)$ (associativity of the smash product), with inverse $\alpha\sy\defeq\alphabar\sy_{(A \smsh B)\smsh C}(\idfunc)$;
\item$\lambda\defeq\lambdabar_B(\idfunc) : \bool\smsh B \simeq B$ and $\rho\defeq\rhobar_A(\idfunc) : A \smsh\bool\simeq A$ (left- and right unitors for the smash product), with inverses $\lambda\sy\defeq\lambdabar_{\bool\smsh B}\sy(\idfunc)$ and $\rho\sy\defeq\rhobar_{A\smsh\bool}\sy(\idfunc)$, respectively;
\item$\gamma\defeq\gammabar_{B\smsh A}(\idfunc) : A \smsh B \simeq B \smsh A$ (braiding for the smash product), with inverse $\gamma\sy\defeq\gammabar_{A \smsh B}\sy(\idfunc)$.
&\simeq A \smsh B \to C \to D \to X &&\text{($e$)}\\
&\simeq (A \smsh B) \smsh C \to D \to X &&\text{($e$)}\\
&\simeq ((A \smsh B) \smsh C) \smsh D \to X &&\text{($e$)}
\intertext{giving $\alphabar^4(\idfunc) : ((A \smsh B)\smsh C)\smsh D)\simeq A \smsh(B \smsh(C \smsh D))$. Moreover, in order to simplify the expressions of $\alpha\smsh D$ and $A \smsh\alpha$, we also define:}
\alphabar^R : ((A \smsh (B \smsh C)) \smsh D \to X) &\simeq (((A \smsh B) \smsh C) \smsh D \to X)
In order to prove the last homotopy in (\ref{eq:alphafour}), it is sufficient to show that $\alphabar^R(\idfunc)\sim\alpha\smsh D$ and that $\alphabar^L(\idfunc)\sim A \smsh\alpha$. We have:
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 \smsh\lambda\sim(e \o(A \to\lambdabar)\o e\sy)(\idfunc)$ and $\rho\smsh B \sim(e \o\rhobar\o e)(\idfunc)$, simplifying the expressions in the sought homotopy. Then:
where the squares on the right are instances of naturality of $\twist$, while the commutativity of the pentagon on the left follows easily from the definition of $\twist$.
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:
$(\type^*,\,\bool,\,\smsh,\,\alpha,\,\lambda,\,\rho,\,\gamma)$ has a structure of a symmetric monoidal category, for $\alpha$, $\lambda$, $\rho$ and $\gamma$ as in \autoref{def:smash-alrg}.
Many results in \autoref{sec:smash} about $({-})\smsh B$ can be generalized to arbitrary pointed $\infty$-functors $\type^*\to\type^*$. Internally in HoTT we cannot talk about $\infty$-categories and $\infty$-functors (as far as we know), and therefore we cannot express this internally. But we only need finitely many coherences, so that we can formulate these results internally for arbitrary functors with enough coherences. However, when we tried this, we run into the problem that we needed all (or at least, some) coherences in the definition of a tricategory and functor for tricategories, which are harder to check than the result we wanted to prove. Here we sketch this argument.
$\type^*$ is a pointed $(\infty,1)$-category meaning it has an zero object $\unit$, which is an object that is both (homotopy-)initial and (homotopy-)terminal. Given two pointed $(\infty,1)$-categories $\mc{A}$ and $\mc{B}$, we call a map $F:\mc{A}\to\mc{B}$ a 1-coherent functor if it satisfies all the coherences of a functor (i.e. an action on morphisms and a 2-cell stating that $F$ respects compositions and identities), a 2-coherent functor if it satisfies all the coherences of a bifunctor (a functor between bicategories) and a 3-coherent functor if it satisfies all the coherences of a trifunctor (a functor between tricategories).
We call $F:\mc{A}\to\mc{B}$ pointed if it preserves the zero object, i.e. if $F\unit=\unit$. If $F$ is a pointed 1-coherent functor, we can then show that $F(0_{A,B})=0_{FA,FB}$, where $0_{A,B}$ is the zero morphism (the canonical morphism $A\to\unit\to B$).
If $F$ is a pointed 2-coherent functor (or more precisely a 1-coherent functor which a coherence for the associativity 2-cell), then we can show that \autoref{lem:smash-coh} holds for $F$. We can show that the two pentagons have the same filler if $F$ is a 3-coherent functor.
Now we can also show \autoref{thm:smash-functor-right} more generally, but we will only formulate that for functors between pointed types. If $F:\type^*\to\type^*$ is a 2-coherent pointed functor, then it induces a map
$(A\to B)\to(FA\to FB)$ which is natural in $A$ and $B$. Moreover, if $F$ is 3-coherent then this is a pointed natural transformation in $B$.
The smash product is associative: there is an equivalence $\alpha : (A \smsh B)\smsh C \simeq A \smsh(B \smsh C)$ which is natural in $A$, $B$ and $C$.
for any pointed type $X$, where $t : (\bool\to X)\simeq X$ is the pointed equivalence with underlying function sending $f : \bool\to X$ to $f(1_\bool) : X$. Both $\lambdabar_X$ and $\rhobar_X$ are natural in their arguments by multiple applications of \autoref{lem: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.
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{lem:e-natural}; then, as in \autoref{thm:smash-associativity}, we can define $\gamma\defeq\gammabar_{B\smsh A}(\idfunc)$ and $\gamma\sy\defeq\gammabar_{A \smsh B}\sy(\idfunc)$
