michael/type-theory
2
0
Fork 0
Code Issues 21 Pull requests Projects 1 Releases 1 Packages Wiki Activity Actions

update talk

Browse source
This commit is contained in:
Michael Zhang 2024-10-16 17:35:42 -05:00
parent edf2393c2f
commit 55611cdb30
2 changed files with 128 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

152
talks/2024-grads/main.tex
View file

@ -4,9 +4,12 @@
\usepackage[TU,T1]{fontenc}
\usepackage{hyperref}
\usepackage[backend=bibtex,style=numeric-comp,sorting=none]{biblatex}
\usepackage{bussproofs}
\usepackage{geometry}
\addbibresource{references.bib}
\nocite{*}
% \setbeameroption{show notes on second screen=right}
\title{Formalizing mathematics with cubical type theory}
@ -48,9 +51,9 @@
\note[item]{How: lot of different techniques involving model checking / SMT approaches, etc}
\note[item]{I'm going to focus here on proofs of mathematical statements, like $$ x + y = y + x $$}
\item What does the current state of the ecosystem look like?
\item What are some existing theorem provers?
\begin{itemize}
\item Rocq (Coq), Lean, Agda, ...
\item Rocq (Coq), Lean, Agda, F*, Idris, Metamath, HOL, ...
\end{itemize}
\end{itemize}
\end{frame}
@ -62,9 +65,10 @@
\section{Type theory}
\begin{frame}
\frametitle{Curry-Howard Isomorphism, or "proofs are programs"}
\frametitle{Proofs are programs}
\begin{itemize}
\item Curry-Howard isomorphism
\item Hypotheses are free variables
\item Functions are implication
\item Pairs are AND
@ -78,11 +82,8 @@
\frametitle{Important features of Martin-L{\"o}f type theory}
\begin{itemize}
\item Universes: $\mathsf{Type}_0, \mathsf{Type}_1, \mathsf{Type}_2, \dots$
\item Inductive types
\\
For example, $\mathbb{N}$ is defined with one of 2 constructors: $\mathsf{zero}$ and $\mathsf{suc}$.
Its induction principle \footnotemark is:
\item Predicative universes: $\mathsf{Type}_0, \mathsf{Type}_1, \mathsf{Type}_2, \dots$
\item Inductive types: for example, $\mathbb{N}$ is defined with 2 possible constructors: $\mathsf{zero}$ and $\mathsf{suc}$.
\begin{prooftree}
\AxiomC{$ \Gamma \vdash c_0 : C $}
@ -90,17 +91,35 @@
\AxiomC{$ \Gamma \vdash n : \mathbb{N} $}
\TrinaryInfC{$ \Gamma \vdash \mathsf{ind}_{\mathbb{N}} (c_0 , x . y . c_s , n) : C $}
\end{prooftree}
\end{itemize}
\end{frame}
\item \emph{Dependent types}, or $\Pi$-types: $ \mathsf{Vec} : (A : \mathsf{Type}) \rightarrow (n : \mathbb{N}) \rightarrow \mathsf{Type} $
\begin{frame}
\frametitle{Important features of Martin-L{\"o}f type theory}
\begin{itemize}
\item \emph{Dependent types}, or $\Pi$-types:
$$ \mathsf{Vec} : \mathsf{Type} \rightarrow \mathbb{N} \rightarrow \mathsf{Type} $$
$$ \mathsf{append} : \prod_{A : \mathsf{Type}} (\prod_{m, n : \mathbb{N}} (\mathsf{Vec}(A, m) \rightarrow \mathsf{Vec}(A, n) \rightarrow \mathsf{Vec}(A, m + n))) $$
\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}
$$ \mathsf{isEven} : \mathbb{N} \rightarrow \mathsf{Type} $$
$$ \mathsf{Even} : \sum_{n : \mathbb{N}} \mathsf{isEven}(n) $$
\end{itemize}
\footnotetext[1]{This is the non-dependent version of the induction principle}
% \footnotetext[1]{This is the non-dependent version of the induction principle}
\end{frame}
\begin{frame}
\frametitle{Important features of Martin-L{\"o}f type theory}
\begin{itemize}
\item The identity type, $\mathsf{Id}_A(x, y)$, for some $x, y : A$
\item Also written as $x \equiv_A y$, or just $x \equiv y$ if $A$ is obvious
\item Single constructor: $\mathsf{refl}_x : \mathsf{Id}_A(x, x)$
\end{itemize}
\end{frame}
\begin{frame}
@ -117,6 +136,21 @@
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Equivalences}
\begin{itemize}
\item In math, we consider a relation to be an equivalence if it is reflexive, symmetric, and transitive.
\item In HoTT, a homotopy equivalence is a specific notion between two types $A$ and $B$
\begin{itemize}
\item A function $f : A \rightarrow B$
\item A function $g : B \rightarrow A$
\item A proof that $g \circ f$ is homotopic to the identity function $\mathsf{id}_A$
\item A proof that $f \circ g$ is homotopic to the identity function $\mathsf{id}_B$
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Univalence axiom}
@ -141,6 +175,7 @@
\begin{itemize}
\item Unfortunately, univalence does not compute in the "base" version of homotopy type theory, also known as Book HoTT
\item Since $\mathsf{Id}_A$ is an inductive type, the only way you can define it is using the constructor $\mathsf{refl}$.
\end{itemize}
\end{frame}
@ -148,10 +183,15 @@
\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
\item Make paths based on the interval type $I$ which represents $[0, 1]$
\item The interval is a primitive construct
\item Construct squares and cubes to create paths by composition and filling
\item Consequences
\begin{itemize}
\item Transport must become a primitive notion, and path induction defined in terms of transport instead
\item Gives us a way to make the univalence axiom a provable theorem
\item Function extensionality is easy
\end{itemize}
\end{itemize}
\end{frame}
@ -181,8 +221,9 @@
\frametitle{The circle}
\begin{itemize}
\item Constructed as a higher inductive type
\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
\item $\mathsf{loop} : \mathsf{base} \equiv \mathsf{base}$, a path representing the rest of the circle
\end{itemize}
\end{frame}
@ -192,6 +233,7 @@
\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 Some example elements:
\begin{itemize}
\item ...
\item $\mathsf{loop}^{-1} \cdot \mathsf{loop}^{-1}$\
@ -212,17 +254,35 @@
\frametitle{The fundamental group of the circle, core idea}
\begin{itemize}
\item Use a helix to represent both!
\item Need to define functions:
\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 $ f : \pi_1(S^1) \rightarrow \mathbb{Z} $
\item $ g : \pi_1(S^1) \leftarrow \mathbb{Z} $
\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{frame}
\begin{frame}
\frametitle{Homotopy type theory proof}
\frametitle{The fundamental group of the circle, core idea}
\begin{itemize}
\item Need to define the following data to prove the equivalence:
\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 $ (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}
\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
@ -235,19 +295,12 @@
\end{frame}
\begin{frame}
\frametitle{Homotopy type theory proof}
\frametitle{Homotopy type theory proof idea}
\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 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 $\mathsf{transport}^{\mathsf{helix}}(p, 0)$
\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}
\end{frame}
@ -255,12 +308,19 @@
\frametitle{Homotopy type theory proof}
\begin{itemize}
\item
\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:
\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$
\item Inverse: $(p : x \equiv_A y) \rightarrow p \cdot p^{-1} \equiv \mathsf{refl}$
\item Inverse: $(p : x \equiv_A y) \rightarrow p^{-1} \cdot p \equiv \mathsf{refl}$
\item Associativity: $(p : x \equiv_A y) \rightarrow (q : y \equiv_A z) \rightarrow (r : z \equiv_A w) \newline \rightarrow (p \cdot q) \cdot r \equiv p \cdot (q \cdot r)$
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Cubical type theory proof}
\frametitle{Defining $\mathsf{decode}$ with cubes}
\begin{figure}
\centering
@ -270,21 +330,33 @@
\section{Conclusion}
% \begin{frame}
% \frametitle{Other topics in homotopy type theory}
% \begin{itemize}
% \item
% \end{itemize}
% \end{frame}
\begin{frame}
\frametitle{Other type theories}
\frametitle{Current work}
\begin{itemize}
\item Calculus of inductive constructions (Impredicative prop)
\item Re-formalizing results from HoTT book chapter 8
\item Re-formalizing results from Floris van Doorn's dissertation on spectral sequences
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Conclusion}
\frametitle{Conclusion and references}
\begin{itemize}
\item Code: \url{https://git.mzhang.io/michael/type-theory}
\item Cube visualizer: \url{https://mzhang.io/cubeviz}
\end{itemize}
\bigskip
\printbibliography
\end{frame}
\end{document}

16
talks/2024-grads/references.bib Normal file
View file

@ -0,0 +1,16 @@
@Book{hottbook,
author = {The {Univalent Foundations Program}},
title = {Homotopy Type Theory: Univalent Foundations of Mathematics},
publisher = {\url{https://homotopytypetheory.org/book}},
address = {Institute for Advanced Study},
year = 2013}
@article{
Cohen_Coquand_Huber_Mörtberg_2016,
title={Cubical Type Theory: a constructive interpretation of the univalence axiom},
url={http://arxiv.org/abs/1611.02108},
DOI={10.48550/arXiv.1611.02108},
abstractNote={This paper presents a type theory in which it is possible to directly manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky’s univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.}, note={arXiv:1611.02108 [cs, math]}, number={arXiv:1611.02108}, publisher={arXiv}, author={Cohen, Cyril and Coquand, Thierry and Huber, Simon and Mörtberg, Anders},
year={2016},
month=nov
}