more work on the talk

talks/2024-grads/main.tex

@@ -1,8 +1,14 @@
-\documentclass{beamer}
-\usetheme{Darmstadt}
-\usepackage{bussproofs}
 
-\setbeameroption{show notes on second screen=right}
+\documentclass[a4paper]{beamer}
+\useoutertheme{miniframes}
+% \usetheme{Darmstadt}
+
+\usepackage[TU,T1]{fontenc}
+\usepackage{hyperref}
+\usepackage{bussproofs}
+\usepackage{geometry}
+
+% \setbeameroption{show notes on second screen=right}
 
 \title{Formalizing mathematics with cubical type theory}
 \author{Michael Zhang}
@@ -11,9 +17,22 @@
 
 \begin{document}
 
+\section{Introduction}
+
 \frame{\titlepage}
 
-\section{Theorem prover intro}
+% \begin{frame}
+%   \frametitle{About me}
+
+%   \begin{itemize}
+%     \item Third-year master's student with \textbf{Favonia}
+%     \item Worked several years as a software engineer at Epic, Amazon, Swoop
+%     \item Binary analysis researcher at defense contractor SIFT
+%     \item Previously officer of GopherHack, UMN, SASE
+%   \end{itemize}
+% \end{frame}
+
+\section{Theorem provers}
 
 \begin{frame}
   \frametitle{Intro}
@@ -41,16 +60,19 @@
   \frametitle{Demo}
 \end{frame}
 
-\section{Homotopy type theory}
+\section{Type theory}
 
 \begin{frame}
   \frametitle{Curry-Howard Isomorphism, or "proofs are programs"}
 
-  \begin{tabular}{c|c}
-    Logic & Programming \\
-    \hline
-    c & d \\
-  \end{tabular}
+  \begin{itemize}
+    \item Hypotheses are free variables
+    \item Functions are implication
+    \item Pairs are AND
+    \item Unions are OR
+    \item Universal quantification ($\forall$) is dependent types
+    \item Existential quantification ($\exists$) is dependent sums
+  \end{itemize}
 \end{frame}
 
 \begin{frame}
@@ -69,15 +91,191 @@
       \TrinaryInfC{$ \Gamma \vdash \mathsf{ind}_{\mathbb{N}} (c_0 , x . y . c_s , n) : C $}
     \end{prooftree}
 
-    \item \emph{Dependent types}:
+    \item \emph{Dependent types}, or $\Pi$-types:
     $$ \mathsf{Vec} : (A : \mathsf{Type}) \rightarrow (n : \mathbb{N}) \rightarrow \mathsf{Type} $$
+
+    \item \emph{Dependent sums}, or $\Sigma$-types
+    \item The identity type, $\mathsf{Id}_A(x, y)$, for some $x, y : A$
+      \begin{itemize}
+        \item Also written as $x \equiv_A y$, or just $x \equiv y$ if $A$ is obvious
+      \end{itemize}
   \end{itemize}
 
   \footnotetext[1]{This is the non-dependent version of the induction principle}
 \end{frame}
 
+\begin{frame}
+  \frametitle{Homotopy type theory}
+
+  \begin{itemize}
+    \item A \textcolor{orange}{"homotopy"}, from algebraic topology, is a way to continuously deform one path into another ($A \times [0, 1] \rightarrow B$)
+    \item In type theory, we can imagine two functions \textcolor{blue}{$f, g : A \rightarrow B$} as being homotopic if we can inhabit $h : (x : A) \rightarrow \mathsf{Id}_B (f(x), g(x))$
+    \item Note: assume all functions are continuous.
+    \item Interpret \textcolor{orange}{paths between points in a space} as the \textcolor{blue}{identity type $\mathsf{Id}$}
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Univalence axiom}
+
+  \begin{itemize}
+    \item Equivalences \emph{are} identities
+    $$ (A \simeq B) \simeq (A \equiv B) $$
+
+    \note[item]{Essentially, if you can prove a way to go back and forth between $A$ and $B$, then $A$ and $B$ can be identified}
+    \item 
+    Intuitively, if you wanted to use a $B$ where you wanted to use an $A$, just convert it and then convert it back later
+
+    \item Importantly, there can be multiple inhabitants of $A \equiv B$
+    \begin{itemize} \item Booleans! \end{itemize}
+
+    \item
+    Transport allows you to use $A$ and $B$ interchangeably
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Univalence axiom?}
+
+  \begin{itemize}
+    \item Unfortunately, univalence does not compute
+    \item Neither does function extensionality
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Cubical type theory}
+
+  \begin{itemize}
+    \item Make the interval type a primitive construct
+    \item Construct $n$-cubes to create paths by composition and filling
+    \item Gives us a way to make the univalence axiom a provable theorem
+    \item Have to re-formulate some of the constructions
+  \end{itemize}
+\end{frame}
+
 \section{Fundamental group of a circle}
 
-\begin{frame} \end{frame}
+\begin{frame}
+  \frametitle{The fundamental group $\pi_1$}
+
+  \begin{itemize}
+    \item Main idea of algebraic topology: identify which spaces are different from each other
+    \item The fundamental group is one metric of identifying spaces (i.e donuts and coffee mugs would have the same group)
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{The circle}
+
+  \begin{itemize}
+    \item The circle ($S^1$) is an example of a simple but non-trivial space
+    \note[item]{it's called $S^1$ because it generalizes into higher dimensions}
+    
+    \item Finding fundamental groups of $n$-spheres is one of the interesting problems in algebraic topology
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{The circle}
+
+  \begin{itemize}
+    \item $\mathsf{base} : S^1$, some arbitrary base point
+    \item $\mathsf{loop} : \mathsf{base} \equiv \mathsf{base}$, a generic way of constructing the rest of the circle
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{The fundamental group of the circle}
+
+  \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}$
+      \begin{itemize}
+        \item ...
+        \item $\mathsf{loop}^{-1} \cdot \mathsf{loop}^{-1}$\
+        \item $\mathsf{loop}^{-1}$
+        \item $\mathsf{refl}$
+        \item $\mathsf{loop}$
+        \item $\mathsf{loop} \cdot \mathsf{loop}$
+        \item ...
+      \end{itemize}
+
+
+    \item The fundamental group of the circle space is the integers
+    $$ \pi_1(S^1) \simeq \mathbb{Z} $$
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{The fundamental group of the circle, core idea}
+
+  \begin{itemize}
+    \item Use a helix to represent both!
+    \item Need to define functions:
+      \begin{itemize}
+        \item $ f : \pi_1(S^1) \rightarrow \mathbb{Z} $
+        \item $ g : \pi_1(S^1) \leftarrow \mathbb{Z} $
+      \end{itemize}
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Homotopy type theory proof}
+
+  \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}
+
+  \begin{itemize}
+    \item For $f : \pi_1(S^1) \rightarrow \mathbb{Z}$, use univalence!
+    \item The increment function $\mathsf{suc}$ is actually an equivalence between $\mathbb{Z}_{0}$ and $\mathbb{Z}_{+1}$
+    \item Define the helix:
+      \begin{itemize}
+        \item $\mathsf{helix} : S^1 \rightarrow \mathsf{Type}$
+        \item $\mathsf{helix}(\mathsf{base}) = \mathbb{Z}$
+        \item $\mathsf{helix}(\mathsf{loop}) = \mathsf{ua}(\mathsf{suc})$
+      \end{itemize}
+    \item This allows us to compute using any loop
+    \item $\mathsf{transport}^{\mathsf{helix}}(p, 0)$
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Homotopy type theory proof}
+
+  \begin{itemize}
+    \item
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Cubical type theory proof}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.75\textwidth]{./decodecube.png}
+  \end{figure}
+\end{frame}
+
+\section{Conclusion}
+
+\begin{frame}
+  \frametitle{Conclusion}
+
+  \begin{itemize}
+    \item Code: \url{https://git.mzhang.io/michael/type-theory}
+    \item Cube visualizer: \url{https://mzhang.io/cubeviz}
+  \end{itemize}
+\end{frame}
 
 \end{document}