diff --git a/Notes/smash.tex b/Notes/smash.tex
index b32c5de..7c6ccee 100644
--- a/Notes/smash.tex
+++ b/Notes/smash.tex
@@ -12,6 +12,10 @@
 \renewcommand{\epsilon}{\varepsilon}
 \newcommand{\tr}{\cdot}
 \renewcommand{\o}{\ensuremath{\circ}}
+\newcommand{\auxl}{\mathsf{auxl}}
+\newcommand{\auxr}{\mathsf{auxr}}
+\newcommand{\gluel}{\mathsf{gluel}}
+\newcommand{\gluer}{\mathsf{gluer}}
 
 \begin{document}
 
@@ -43,9 +47,7 @@
   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$. In these
-  notes we will not use $0$ for the empty type (since that is not pointed, we will not use the empty
-  type).
+  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$.
 \end{rmk}
 
 \begin{lem}
@@ -65,17 +67,35 @@
 
 \section{Smash Product}
 
-
-\begin{lem}\mbox{}
+\begin{lem}\mbox{}\label{lem:smash-general}
   \begin{itemize}
+  \item The smash of $A$ and $B$ is the HIT generated by point constructor
+    $({-},{-}):A\to B \to A\smash B$ and two auxilliary points $\auxl,\auxr:A\smash B$ and path
+    constructors $\gluel:\prd{a:A}(a,b_0)=\auxl$ and $\gluer:\prd{b:B}(a_0,b)=\auxr$ (the
+    constructors are given as unpointed maps). $A\smash B$ is pointed with point $(a_0,b_0)$.
   \item The smash is functorial: if $f:A\pmap A'$ and $g:B\pmap B'$ then
     $f\smash g:A\smash B\pmap A'\smash B'$. We write $A\smash g$ or $f\smash B$ if one of the
     functions is the identity function.
   \item Smash preserves composition, which gives rise to the interchange law:
-    $(f' \o f)\smash (g' \o g) \sim f' \smash g' \o f \smash g$
+    $i:(f' \o f)\smash (g' \o g) \sim f' \smash g' \o f \smash g$
   \item If $p:f\sim f'$ and $q:g\sim g'$ then $p\smash q:f\smash g\sim f'\smash g'$. This operation
     preserves reflexivities, symmetries and transitivies.
-  \item $f\smash0\sim0$ and $0\smash g\sim 0$.
+  \item There are homotopies $f\smash0\sim0$ and $0\smash g\sim 0$ such that the following diagrams
+    commute for given homotopies $p : f\sim f'$ and $q : g\sim g'$.
+    \begin{center}
+\begin{tikzcd}
+f\smash 0 \arrow[rr, equals,"p\smash1"]\arrow[dr,equals] & &
+f'\smash 0\arrow[dl,equals] \\
+& 0 &
+\end{tikzcd}
+\qquad
+\begin{tikzcd}
+0\smash g\arrow[rr, equals,"1\smash q"]\arrow[dr,equals] & &
+0\smash g'\arrow[dl,equals] \\
+& 0 &
+\end{tikzcd}
+\end{center}
+
   \end{itemize}
 \end{lem}
 
@@ -87,8 +107,8 @@
 \begin{center}
 \begin{tikzcd}
 (f_2 \o f_1)\smash (g_2 \o 0) \arrow[r, equals]\arrow[dd,equals] &
-(f_2 \smash g_1)\o (f_1 \smash 0)\arrow[d,equals] \\
-& (f_2 \smash g_1)\o 0\arrow[d,equals] \\
+(f_2 \smash g_2)\o (f_1 \smash 0)\arrow[d,equals] \\
+& (f_2 \smash g_2)\o 0\arrow[d,equals] \\
 (f_2 \o f_1)\smash 0 \arrow[r,equals] &
 0
 \end{tikzcd}
@@ -104,8 +124,24 @@
 
 \end{lem}
 \begin{proof}
-We will only do the case where $g_1\jdeq 0$, the other case is similar (but slightly easier). In this case, we need to show that the following diagram commutes.
-Proof to do.
+  We will only do the case where $g_1\jdeq 0$, i.e. fill the diagram on the left. The other case is
+  similar (but slightly easier). First apply induction on the paths that $f_2$, $f_1$ and $g_2$
+  respect the basepoint. In this case $g_2\o0$ is definitionally equal to $0$, and the canonical
+  proof that $g_2\o 0~0$ is (definitionally) equal to reflexivity. This means that the homotopy
+  $(f_2 \o f_1)\smash (g_2 \o 0)~(f_2 \o f_1)\smash 0$ is also equal to reflexivity.
+
+  For the underlying homotopy, take $x : A_1\smash B_1$. We apply induction on $x$.
+  Suppose $x\equiv(a,b)$ for $a:A_1$ and $b:B_1$. Then we have to fill the square (denote the basepoints of $A_i$ and $B_i$ by $a_i$ and $b_i$)
+  
+  \begin{center}
+    \begin{tikzcd}
+      (f_2(f_1(a)),g_2(b_2))\arrow[r, equals,"1"]\arrow[dd,equals,"1"] &
+      (f_2(f_1(a)),g_2(b_2))\arrow[d,equals] \\
+      & (f_2(a_2),g_2(b_2))\o (f_1 \smash g_1)\arrow[d,equals] \\
+      (f_2(f_1(a)),y_0) \arrow[r,equals,"1"] &
+      (x_0,y_0)
+    \end{tikzcd}
+  \end{center}
 \end{proof}
 
 \begin{thm}\label{thm:smash-functor-right}
@@ -138,8 +174,9 @@ which is natural in $A$, $B$ and $C$. (note: $(A\smash C\pmap B\smash C)$ is bot
 \end{tikzcd}
 \end{center}
 Let $k:A\pmap B$. Then as homotopy the naturality in $A$ becomes
-$(k\o f)\smash C=k\smash C\o f\smash C$. To prove an equality between pointed maps, we need to give a pointed homotopy, which is given by interchange. To show that this homotopy
-is pointed, we need to fill the following square, which follows from \autoref{lem:smash-coh}.
+$(k\o f)\smash C=k\smash C\o f\smash C$. To prove an equality between pointed maps, we need to give
+a pointed homotopy, which is given by interchange. To show that this homotopy is pointed, we need to
+fill the following square (after reducing out the applications of function extensinality), which follows from \autoref{lem:smash-coh}. 
 \begin{center}
 \begin{tikzcd}
 (0 \o f)\smash C \arrow[r, equals]\arrow[dd,equals] &
@@ -161,20 +198,28 @@ square, which follows from \autoref{lem:smash-coh}.
 0
 \end{tikzcd}
 \end{center}
-The naturality in $C$ is harder. For the underlying homotopy we need to show
-$B\smash h\o g\smash C=g\smash C'\o A\smash h$. This follows by applying interchange twice:
-$$B\smash h\o g\smash C\sim(\idfunc[B]\o g)\smash(h\o\idfunc[C])\sim(g\o\idfunc[A])\smash(\idfunc[C']\o h)\sim g\smash C'\o A\smash h.$$
+The naturality in $C$ is a bit harder. For the underlying homotopy we need to show
+$B\smash h\o k\smash C=k\smash C'\o A\smash h$. This follows by applying interchange twice:
+$$B\smash h\o k\smash C\sim(\idfunc[B]\o k)\smash(h\o\idfunc[C])\sim(k\o\idfunc[A])\smash(\idfunc[C']\o h)\sim k\smash C'\o A\smash h.$$
 To show that this homotopy is pointed, we need to fill the following square:
-% \begin{center}
-% \begin{tikzcd}
-% (B\smash h\o g\smash C) \arrow[r, equals]\arrow[dd,equals] &
-% (g \smash C)\o (0 \smash C)\arrow[d,equals] \\
-% & (g\smash C) \o 0\arrow[d,equals] \\
-% 0\smash C \arrow[r,equals] &
-% 0
-% \end{tikzcd}
-% \end{center}
-
+\begin{center}
+  \begin{tikzcd}
+    B\smash h\o 0\smash C \arrow[r, equals]\arrow[d,equals] & 
+    (\idfunc[B]\o 0)\smash(h\o\idfunc[C]) \arrow[r, equals]\arrow[d,equals] &
+    (0\o\idfunc[A])\smash(\idfunc[C']\o h)\arrow[r, equals]\arrow[d,equals] &
+    0\smash C'\o A\smash h\arrow[d,equals] \\
+    B\smash h\o 0 \arrow[d,equals] & 
+    0\smash(h\o\idfunc[C]) \arrow[r, equals]\arrow[d,equals] &
+    0\smash(\idfunc[C']\o h) \arrow[d,equals] &
+    0\o A\smash h\arrow[d,equals] \\
+    B\smash h\o 0 \arrow[r, equals] & 
+    0 \arrow[r, equals] &
+    0 \arrow[r, equals] &
+    0
+  \end{tikzcd}
+\end{center}
+The left and the right squares are filled by \autoref{lem:smash-coh}. The squares in the middle
+are filled by (corollaries of) \autoref{lem:smash-general}.
 \end{proof}
 
 \section{Adjunction}