diff --git a/Notes/smash.tex b/Notes/smash.tex index f8c2c02..2eb340d 100644 --- a/Notes/smash.tex +++ b/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} -\item All types, maps and homotopies in these notes are pointed, unless explicitly mentioned +\begin{rmk}\label{rmk:pointed-types} + 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 - $0\o g \sim 0$ and $f \o 0 \sim 0$. + constant map $0\equiv0_{A,B}:A\to B$ which has as underlying function $\lam{a:A}b_0$. We have the homotopies: + \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\] - 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. + \[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 $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. -\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. +Using \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} - 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{rmk}\label{rmk:alrg-pointed-natural} + 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} - (B \to C \to A \to X) - \arrow[rr, "B\to c"] - \arrow[d, swap, "e"] - && (B \to A \to C \to X) + \begin{tikzcd}[column sep=7em] + (B \smash C \to A \to X) + \arrow[r, "e\sy"] + \arrow[dd, swap, "c"] + & (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) - \arrow[r, swap, "c"] - & (A \to B \smash C \to X) + (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*}