From 009304a28d13340837e4c009d9aaaf7fa0445f4b Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Wed, 16 Oct 2024 17:45:16 -0500
Subject: [PATCH] fix incorrect types

---
 talks/2024-grads/main.tex | 37 ++++++++++++++++++++++---------------
 1 file changed, 22 insertions(+), 15 deletions(-)

diff --git a/talks/2024-grads/main.tex b/talks/2024-grads/main.tex
index 17a21c9..7053cbe 100644
--- a/talks/2024-grads/main.tex
+++ b/talks/2024-grads/main.tex
@@ -281,19 +281,6 @@
   \end{itemize}
 \end{frame}
 
-\begin{frame}
-  \frametitle{Homotopy type theory proof idea}
-
-  \begin{itemize}
-    \item For $g : \mathbb{Z} \rightarrow \pi_1(S^1)$, we can just add $\mathsf{loop}$s to $\mathsf{refl}$ inductively
-    \begin{itemize}
-      \item $g(-1 + n) = \mathsf{loop}^{-1} \cdot g(n)$
-      \item $g(0) = \mathsf{refl}$
-      \item $g(n + 1) = g(n) \cdot \mathsf{loop}$
-    \end{itemize}
-  \end{itemize}
-\end{frame}
-
 \begin{frame}
   \frametitle{Homotopy type theory proof idea}
 
@@ -304,11 +291,31 @@
   \end{itemize}
 \end{frame}
 
+\begin{frame}
+  \frametitle{Homotopy type theory proof idea}
+
+  \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$
+    \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}$
+    \end{itemize}
+
+    \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$
+    \end{itemize}
+  \end{itemize}
+\end{frame}
+
 \begin{frame}
   \frametitle{Homotopy type theory proof}
 
   \begin{itemize}
-    \item The homotopies $g \circ f \equiv_{\pi_1(S^1)} \mathsf{id}$ and $f \circ g \equiv_{\mathbb{N}} \mathsf{id}$ 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 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$
@@ -320,7 +327,7 @@
 \end{frame}
 
 \begin{frame}
-  \frametitle{Defining $\mathsf{decode}$ with cubes}
+  \frametitle{Defining $g$ with cubes}
 
   \begin{figure}
     \centering