notes yoneda

Notes/smash.tex

@@ -24,7 +24,7 @@
 \newcommand{\gammabar}{\overline{\gamma}}
 \newcommand{\pType}{\mathsf{Type}_\ast}
 \newcommand{\two}{\mathbf{2}}
-\newcommand{\yoneda}{\mathbf{Y}}
+\newcommand{\yoneda}{\psi}
 
 \begin{document}
 
@@ -44,8 +44,8 @@
 \end{itemize}
 \end{defn}
 
-\begin{rmk}
+\begin{rmk}\label{rmk:pointed-types}
-\item All types, maps and homotopies in these notes are pointed, unless explicitly mentioned
+  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
@@ -56,8 +56,12 @@
   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
+  constant map $0\equiv0_{A,B}:A\to B$ which has as underlying function $\lam{a:A}b_0$. We have the homotopies:
-  $0\o g \sim 0$ and $f \o 0 \sim 0$.
+  \begin{align*}
+  s : 0 \o g &\sim 0 & s' : f \o 0 &\sim 0\\
+  q : f \o 1 &\sim f & q' : 1 \o g &\sim g
+  \end{align*}
+  with $s(1) = q(0)$ and $s'(1) = q'(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$.
@@ -67,7 +71,7 @@
   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
+  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'"] \\
@@ -77,6 +81,8 @@
 
 \end{lem}
 
+\section{Naturality and a version of the Yoneda lemma}
+
 \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:
@@ -89,18 +95,18 @@
 			\arrow[d, "\theta_B"]
 		\\
 		G(A)
-			\arrow[r, swap, "F(g)"]
+			\arrow[r, swap, "G(f)"]
 		& 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\]
+		\[p(f) : G(f) \o \theta_A \sim \theta_B \o F(f)\]
 		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\]
+		\[p_0 : G(0) \o \theta_A \sim 0 \o \theta_A \sim 0 \sim \theta_B \o 0 \sim \theta_B \o F(0)\]
-		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.
+		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.
 	\end{itemize}
 \end{defn}
 
@@ -108,6 +114,62 @@
 	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}
 
+\begin{lem}[Yoneda]\label{lem:yoneda}
+	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:
+	\begin{align*}
+		(\psi_\phi \to X)(f) &\judgeq f \o \psi_\phi\\
+		&\sim \phi_X (f \o \idfunc) &&\text{(by $p_\phi(f)(\idfunc)$)}\\
+		&\sim \phi_X (f) &&\text{(by $\mapfunc{\phi_X}(q_f)$)}
+	\end{align*}
+	To show that this is a pointed homotopy, we need to prove that the following diagram commutes:
+	\begin{center}
+	\begin{tikzcd}[column sep=4em]
+		(\psi_\phi \to X)(0)
+			\arrow[rr, equals, "p_\phi(0)(\idfunc)\tr\mapfunc{\phi_X}(q_0)"]
+			\arrow[dr, equals, swap, "s_{\psi_\phi}"]
+		&&\phi_X(0)
+			\arrow[dl, equals, "(\phi_X)_0"]
+		\\
+		&0
+	\end{tikzcd}
+	\end{center}
+	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:
+	\begin{align*}
+	0\o \phi_X(\idfunc)
+	&= 0 &&\text{(by $s_{q_X(\idfunc)}$)}\\
+	&= \phi_X(0) &&\text{(by $(\phi_X)_0\sy$)}\\
+	&= \phi_X(0\o 1) &&\text{(by $(\mapfunc{\phi_X}(s_1))\sy$)}
+	\end{align*}
+	The diagram then commutes by cancellation of inverses and using that $s_1 = q_0$.
+\end{proof}
+
 \section{Smash Product}
 
 \begin{defn}
@@ -460,29 +522,7 @@ We aim to prove that the smash product is a (1-coherent) symmetric monoidal prod
 \[(\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.
+Using \autoref{lem:yoneda} we can prove associativity, left- and right unitality and braiding equivalences for the smash product, in the following way.
-\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:
@@ -499,7 +539,7 @@ By \autoref{lem:yoneda} we can prove associativity, left- and right unitality an
 				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$;
+			with $t : (\two \to X) \simeq X$ the pointed equivalence, pointed 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)\\
@@ -512,12 +552,12 @@ By \autoref{lem:yoneda} we can prove associativity, left- and right unitality an
 				&\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$.
+			where $c : (A \to B \to X) \simeq (B \to A \to X)$ is the obvious pointed equivalence, natural in all its arguments and pointed natural in $X$.
 	\end{itemize}
 \end{defn}
 
-\begin{rmk}
+\begin{rmk}\label{rmk:alrg-pointed-natural}
-	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:
+	The equivalences in \autoref{def:equiv-precursors} are natural in all their arguments and pointed natural in $X$, by (pointed) naturality of $e$ (\autoref{e-natural} and \autoref{e-pointed-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)
@@ -534,6 +574,21 @@ By \autoref{lem:yoneda} we can prove associativity, left- and right unitality an
 	$\alpha$, $\lambda$, $\rho$ and $\gamma$ are natural in all their arguments, as $\alphabar$, $\lambdabar$, $\rhobar$ and $\gammabar$ are.
 \end{defn}
 
+\begin{cor}\label{lem:bar-homotopy}
+	There are pointed homotopies
+	\begin{align*}
+	\alphabar_X &\sim \alpha \to X
+		& \lambdabar_X &\sim \lambda \to X
+	\\
+	\rhobar_X &\sim \rho \to X
+		& \gammabar_X &\sim \gamma \to X
+	\end{align*}
+\end{cor}
+
+\begin{proof}
+	This follows directly from \autoref{lem:yoneda-pointed} and \autoref{rmk:alrg-pointed-natural}.
+\end{proof}
+
 \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)\]
@@ -665,7 +720,7 @@ By \autoref{lem:yoneda} we can prove associativity, left- and right unitality an
 		\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((\alpha \to A \smash (B \smash (C \smash D))) \o \eta) &&\text{(\autoref{cor:bar-homotopy})}\\
 		&\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)}
@@ -738,21 +793,53 @@ By \autoref{lem:yoneda} we can prove associativity, left- and right unitality an
 \begin{lem}\label{lem:pentagon-c}
 	The following diagram commutes, for $A$, $B$, $C$ and $X$ pointed types:
 	\begin{center}
-	\begin{tikzcd}
+	\begin{tikzcd}[column sep=7em]
-		(B \to C \to A \to X)
+		(B \smash C \to A \to X)
-			\arrow[rr, "B\to c"]
+			\arrow[r, "e\sy"]
-			\arrow[d, swap, "e"]
+			\arrow[dd, swap, "c"]
-		&& (B \to A \to C \to X)
+		& (B \to C \to A \to X)
+			\arrow[d, "B \to c"]
+		\\
+		& (B \to A \to C \to X)
 			\arrow[d, "c"]
 		\\
-		(B \smash C \to A \to X)
+		(A \to B \smash C \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{proof}
+	Unfolding the definition of $e\sy$, we get the diagram:
+	\begin{center}
+	\begin{tikzcd}[column sep=6em]
+		(B \smash C \to A \to X)
+			\arrow[rr, bend left=10, "e\sy"]
+			\arrow[r, swap, "C\to -"]
+			\arrow[dd, swap, "c"]
+		& ((C \to B \smash C) \to C \to A \to X)
+			\arrow[r, swap, "\eta \to C \to A \to X"]
+			\arrow[d, swap, "(C \to B \smash C) \to c"]
+		& (B \to C \to A \to X)
+			\arrow[d, "B \to c"]
+		\\
+		& ((C \to B \smash C) \to A \to C \to X)
+			\arrow[r, swap, "\eta \to A \to C \to X"]
+			\arrow[d, swap, "c"]
+		& (B \to A \to C \to X)
+			\arrow[d, "c"]
+		\\
+		(A \to B \smash C \to X)
+			\arrow[rr, swap, bend right=10, "A \to e\sy"]
+			\arrow[r, "A \to (C \to -)"]
+		& (A \to (C \to B \smash C) \to C \to X)
+			\arrow[r, "A \to (\eta \to C \to X)"]
+		& (A \to B \to C \to X)
+	\end{tikzcd}
+	\end{center}
+	where the squares on the right are instances of naturality of $c$, while the commutativity of the pentagon on the left follows easily from the definition of $c$.
+\end{proof}
+
 
 \begin{thm}[Associativity-braiding hexagon]\label{thm:smash-associativity-braiding}
 	For pointed types $A$, $B$ and $C$, there is a homotopy
@@ -789,7 +876,8 @@ By \autoref{lem:yoneda} we can prove associativity, left- and right unitality an
 		&\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})}
+		&\sim (e \o e \o c \o (B \to c) \o e\sy \o e \o (B \to e\sy) \o e\sy)(\idfunc) &&\text{(\autoref{lem:pentagon-c})}\\
+		&\sim (e \o e \o c \o (B \to c) \o (B \to e\sy) \o e\sy)(\idfunc) &&\text{(cancelling)}
 	\end{align*}
 	and
 	\begin{align*}