\[\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').$$
A (1-coherent) \emph{functor}$F$ between pointed types is a function $F_0:\type^*\to\type^*$ with an action of morphisms $F_1 : (A \to^* B)\to(FA \to^* FB)$ such that $F_1(g \o f)\sim F_1g \o F_1 f$ and $F_1\idfunc[A]\sim\idfunc[F_0A]$. We will write both $F_0$ and $F_1$ as $F$. A functor $F$ is \emph{pointed} if $F\unit$ is contractible. In this case $F0_{A,B}\sim0_{FA,FB}$.
Let $F$, $G$ be functors of pointed types. Suppose that we have a transformation $\theta_X : F(X)\to G(X)$ for all pointed types $X$.
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: naturality implies weak naturality, 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 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 pointed homotopy \[ p_\phi(f) : (A \to f)\o\phi_X \sim\phi_{X'}\o(B \to f)\]
We define $\psi_\phi\defeq\phi_B(\idfunc[B]) : A \to B$ and $\psi_\phi\sy\defeq\phi_A\sy(\idfunc[A]):B\to A$. The given naturality square for $f \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.
Assume $A$, $B$, $\phi_X$ and $p$ as in \autoref{lem:yoneda}, and assume moreover that $\phi$ is pointed natural. Then there is a pointed homotopy $(\psi_\phi\to X)\sim\phi_X$.
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
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 $q_0$ of the following pointed homotopies:
$$({-})\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
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 square on the top right is by \autoref{lem:composition-pointed}, the square on the bottom right is naturality of $\twist$. The commutativity of the pentagon on the left is TODO (it is a diagram of a 1-coherent symmetric closed category).
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$.
\item An algebraic theory of tricategories, Nick Gurski
\item Closed Categories, Samuel Eilenberg and G. Max Kelly (Chapter 2, Theorem 5.3, 1-categorical account of getting a monoidal category from a enriched adjunction in a closed category)
\item Permutative categories, multicategories, and algebraic K-theory, A D Elmendorf and M A Mandell (Lemma 4.20 gives a 1-categorical account that if C is a symmetric monoidal closed bicomplete 1-category, then the category of pointed objects is a symmetric monoidal closed bicomplete 1-category).
\item On embedding closed categories, B.J. Day and M.L. Laplaza (definition of symmetric closed category).
\item Maybe: Handbook of Categorical Algebra 2 Categories and Structures, F Borceux. (Bjorn used it to look things up about symmetric monoidal closed categories)
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)$
