update

talks/2024-grads/.gitignore

@@ -6,4 +6,6 @@ main.pdf
 *.out
 *.run.xml
 *.snm
-*.toc
+*.toc
+*.bbl
+*.blg

talks/2024-grads/main.tex

@@ -8,12 +8,12 @@
 \usepackage{colortbl}
 \usepackage{geometry}
 
-% \usepackage[backend=bibtex,style=numeric-comp,sorting=none]{biblatex}
-% \addbibresource{references.bib}
-% \nocite{*}
+\usepackage[backend=bibtex,style=numeric-comp,sorting=none]{biblatex}
+\addbibresource{references.bib}
+\nocite{*}
 
 \setbeamercovered{transparent}
-% \setbeameroption{show notes on second screen=right}
+\setbeameroption{show notes on second screen=right}
 
 \title{Formalizing mathematics with cubical type theory}
 \author{Michael Zhang}
@@ -255,9 +255,6 @@
 \begin{frame}
   \frametitle{Homotopy type theory}
 
-  \newcommand{\htcolor}[1]{\textcolor{red}{####1}}
-  \newcommand{\ttcolor}[1]{\textcolor{blue}{####1}}
-
   \begin{itemize}
     \item A homotopy, from algebraic topology, is a way to continuously deform one path into another ($A \times [0, 1] \rightarrow B$)
 
@@ -269,7 +266,7 @@
       \includegraphics[width=0.5\textwidth]{images/homotopy.png}
     \end{figure}
 
-    \note[item]{Interpret \htcolor{paths between points in a space} as the \ttcolor{identity type $\mathsf{Id}$}}
+    \note[item]{Interpret paths between points in a space as the identity type $\mathsf{Id}$}
   \end{itemize}
 \end{frame}
 
@@ -453,6 +450,11 @@
     \item The fundamental group is one metric of identifying spaces
     \note[item]{fundamental group is a special case of a homotopy group}
   \end{itemize}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.5\textwidth]{images/loopspace.jpg}
+  \end{figure}
 \end{frame}
 
 \begin{frame}
@@ -463,7 +465,7 @@
     \pause
     \item Determining fundamental groups of $n$-spheres is a difficult problem in algebraic topology
     \pause
-    \item Fortunately, $\pi_1(S^1)$ is easy
+    \item Fortunately, $\pi_1(S^1)$ has a known solution
   \end{itemize}
 \end{frame}
 
@@ -472,7 +474,10 @@
 
   \begin{itemize}
     \note[item]{glossing over some details, loop space asks about the point base only}
-    \item Fundamental group asks us about the loops in the circle space: $\mathsf{base} \equiv \mathsf{base}$
+    \item Fundamental group asks us about the loops in the circle space
+    \pause
+    \item $\mathsf{base} \equiv \mathsf{base}$ because we don't care about choice of base point
+    \pause
     \item Some example elements:
       \begin{itemize}
         \item ...
@@ -485,6 +490,7 @@
       \end{itemize}
 
 
+    \pause
     \item The fundamental group of the circle space is the integers
     $$ \pi_1(S^1) \simeq \mathbb{Z} $$
   \end{itemize}
@@ -495,15 +501,46 @@
 
   \begin{itemize}
     \item Use a winding helix to represent both!
-    \item Problem: we want multiple loopings to map us to different integers.
-    \item Idea: define a custom type family that takes different number of loops to different "rotations" of the integers!
-    \item Define the encoding:
-      \begin{itemize}
-        \item $\mathsf{code} : S^1 \rightarrow \mathsf{Type}$
-        \item $\mathsf{code}(\mathsf{base}) = \mathbb{Z}$
-        \item $\mathsf{code}(\mathsf{loop}) = \mathsf{ua}(\mathsf{suc})$
-      \end{itemize}
   \end{itemize}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.3\textwidth]{images/winding.png}
+  \end{figure}
+\end{frame}
+
+\begin{frame}
+  \frametitle{The fundamental group of the circle, core idea}
+
+  \begin{itemize}
+    \item Problem: we want multiple loopings to map us to different integers.
+  \end{itemize}
+
+  \pause
+
+  \begin{columns}
+    \begin{column}{.45\textwidth}
+      \begin{itemize}
+        \only<-2>{
+          \item Idea: define a custom type family that takes different number of loops to different "rotations" of the integers!
+        }
+        \only<3>{
+          \item Define the encoding:
+            \begin{itemize}
+              \item $\mathsf{code} : S^1 \rightarrow \mathsf{Type}$
+              \item $\mathsf{code}(\mathsf{base}) = \mathbb{Z}$
+              \item $\mathsf{code}(\mathsf{loop}) = \mathsf{ua}(\mathsf{suc})$
+            \end{itemize}
+        }
+      \end{itemize}
+    \end{column}
+    \begin{column}{.55\textwidth}
+  \begin{figure}
+    \centering
+    \includegraphics[width=\textwidth]{images/encoding.png}
+  \end{figure}
+    \end{column}
+  \end{columns}
 \end{frame}
 
 \begin{frame}
@@ -511,10 +548,12 @@
 
   \begin{itemize}
     \item Need to define the following data to prove the equivalence:
+    $$ (\mathsf{base} \equiv_{S^1} c) \simeq \mathsf{code}(c) $$
+    \pause
+    \item For some $(c : S^1)$ and $(n : \mathbb{N})$ that encodes how many loopings a path to $c$ could take
       \begin{itemize}
-        \item For some $c : S^1$ and $n : \mathbb{N}$ that encodes how many loopings a path to $c$ could take is:
-        \item $ f : \mathsf{base} \equiv_{S^1} c \rightarrow \mathsf{code}(c) $
-        \item $ g : \mathsf{base} \equiv_{S^1} c \leftarrow \mathsf{code}(c) $
+        \item $ f : (\mathsf{base} \equiv_{S^1} c) \rightarrow \mathsf{code}(c) $
+        \item $ g : \mathsf{code}(c) \rightarrow (\mathsf{base} \equiv_{S^1} c) $
         \item $ (g \circ f)(p) \equiv \mathsf{id}_{\mathsf{base} \equiv_{S^1} c} $
         \item $ (f \circ g)(n) \equiv \mathsf{id}_{\mathbb{Z}} $
       \end{itemize}
@@ -525,10 +564,15 @@
   \frametitle{Homotopy type theory proof idea}
 
   \begin{itemize}
-    \item For $f : \mathsf{base} \equiv_{S^1} c \rightarrow \mathbb{Z}$, just use the winding map!
-    \item This allows us to compute using any loop
+    \item For $f : (\mathsf{base} \equiv_{S^1} c) \rightarrow \mathsf{code}(c)$, just use the winding map!
+    \item This allows us to turn any loop into an integer
     \item For some $p : \mathsf{base} \equiv \mathsf{base}$, $\mathsf{transport}^{\mathsf{code}}(p, 0)$ turns 0 into any integer by mapping over the equivalence between integers
   \end{itemize}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.5\textwidth]{images/encode.png}
+  \end{figure}
 \end{frame}
 
 \begin{frame}
@@ -536,17 +580,19 @@
 
   \begin{itemize}
     \item For $g : \mathsf{code}(c) \rightarrow \mathsf{base} \equiv_{S^1} c$,
-    we can iteratively compose $\mathsf{loop}$s to $\mathsf{refl}$ using a function $loop^n$
+    we can iteratively compose $\mathsf{loop}$s to $\mathsf{refl}$ using a function $\mathsf{loop}^n$
     \begin{itemize}
-      \item $loop^{-1 + n} = loop^n \cdot \mathsf{loop}^{-1}$
-      \item $loop^0 = \mathsf{refl}$
-      \item $loop^{n + 1} = loop^n \cdot \mathsf{loop}$
+      \item $\mathsf{loop}^{-1 + n} = \mathsf{loop}^n \cdot \mathsf{loop}^{-1}$
+      \item $\mathsf{loop}^0 = \mathsf{refl}$
+      \item $\mathsf{loop}^{n + 1} = \mathsf{loop}^n \cdot \mathsf{loop}$
     \end{itemize}
 
+    \pause
     \item Then, use this to define $g$
     \begin{itemize}
-      \item $g(c : \mathsf{code}(\mathsf{base})) = loop^c$
-      \item $g(c : \mathsf{code}(\mathsf{loop})) : loop^c \equiv loop^c$
+      \item $g(c : \mathsf{code}(\mathsf{base})) = \mathsf{loop}^c$
+      \item $g(c : \mathsf{code}(\mathsf{loop})) : (\mathsf{loop}^c \equiv^{\lambda x \mapsto \mathsf{code}(x) \rightarrow \mathsf{base} \equiv x}_{\mathsf{loop}} \mathsf{loop}^c)$
+      \item This can be defined in two ways
     \end{itemize}
   \end{itemize}
 \end{frame}
@@ -555,7 +601,7 @@
   \frametitle{Homotopy type theory proof}
 
   \begin{itemize}
-    \item The homotopies $(g \circ f \equiv \mathsf{id}_{(\mathsf{base} \equiv_{S^1} c)})$ and $(f \circ g \equiv \mathsf{id}_{\mathsf{code}(c)})$ can be proven just by applying groupoid laws of paths:
+    \item The homotopies $(g \circ f \equiv \mathsf{id}_{(\mathsf{base} \equiv_{S^1} c)})$ and $(f \circ g \equiv \mathsf{id}_{\mathsf{code}(c)})$ can be proven just by applying path induction and these groupoid laws of paths:
       \begin{itemize}
         \item Identity: $(p : x \equiv_A y) \rightarrow p \cdot \mathsf{refl} \equiv p$
         \item Identity: $(p : x \equiv_A y) \rightarrow \mathsf{refl} \cdot p \equiv p$
@@ -566,12 +612,21 @@
   \end{itemize}
 \end{frame}
 
+\begin{frame}
+  \frametitle{Composition}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.75\textwidth]{images/composition.png}
+  \end{figure}
+\end{frame}
+
 \begin{frame}
   \frametitle{Defining $g$ with cubes}
 
   \begin{figure}
     \centering
-    \includegraphics[width=0.75\textwidth]{./decodecube.png}
+    \includegraphics[width=0.75\textwidth]{images/decodecube.png}
   \end{figure}
 \end{frame}
 
@@ -589,7 +644,7 @@
   \frametitle{Current work}
 
   \begin{itemize}
-    \item Re-formalizing results from HoTT book chapter 8
+    \item Re-formalizing results from HoTT book chapters 7 on $n$-types and 8 on homotopy theory
     \item Re-formalizing results from Floris van Doorn's dissertation on spectral sequences
   \end{itemize}
 \end{frame}
@@ -603,7 +658,7 @@
 
   \bigskip
 
-  % \printbibliography
+  \printbibliography
 \end{frame}
 
 \end{document}