add discussion to notes smash

Notes/smash.tex

@@ -3,6 +3,7 @@
 \input{preamble-articles}
 
 \title{Notes on the smash product}
+\author{Floris van Doorn \and Stefano Piceghello}
 \date{\today}
 \usepackage{fullpage}
 \newcommand{\pmap}{\to}
@@ -27,6 +28,7 @@
 \newcommand{\oneh}{\mathsf{u}}
 \newcommand{\two}{\mathsf{t}}
 \newcommand{\twist}{\mathsf{c}}
+\newcommand{\mc}{\mathcal}
 
 \begin{document}
 
@@ -179,7 +181,7 @@
 	The diagram then commutes by cancellation of inverses and using that $\zeroh_{\idfunc} = \oneh_0$.
 \end{proof}
 
-\section{Smash Product}
+\section{Smash Product}\label{sec:smash}
 
 \begin{defn}
   The smash of $A$ and $B$ is the HIT generated by the point constructor $(a,b)$ for $a:A$ and $b:B$
@@ -940,10 +942,25 @@ Using \autoref{lem:yoneda} (Yoneda) we can prove associativity, left- and right
 	Follows by the theorems in this section.
 \end{proof}
 
+\section{Discussion}
 
-\section{Notes on the formalization}
+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.
 
-%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).
+$\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).
+% Add reference:
+% @article{gurski2006algebraic,
+% title={An algebraic theory of tricategories},
+% author={Gurski, Nick},
+% year={2007},
+% url={http://gauss.math.yale.edu/~mg622/tricats.pdf}
+% }
+
+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$.
 
 \end{document}
 
@@ -997,4 +1014,4 @@ Using \autoref{lem:yoneda} (Yoneda) we can prove associativity, left- and right
 			&\simeq A \smsh 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{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)$
-\end{proof}
+\end{proof}