diff --git a/talks/2024-grads/decodecube.png b/talks/2024-grads/decodecube.png new file mode 100644 index 0000000..b47019f Binary files /dev/null and b/talks/2024-grads/decodecube.png differ diff --git a/talks/2024-grads/main.tex b/talks/2024-grads/main.tex index 389fb99..b6db01a 100644 --- a/talks/2024-grads/main.tex +++ b/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} \ No newline at end of file