changes

src/CubicalHott/Theorem7-1-11.agda

@@ -22,15 +22,17 @@ lemma zero (A , a , Acontr) (B , b , Bcontr) i = A≡B i , a≡b i , λ y j →
   a≡b : PathP (λ i → A≡B i) a b
   a≡b j = glue (λ { (j = i0) → a ; (j = i1) → b }) b
 
-  eqv2 : ((y : A) → a ≡ y) ≡ ((y : B) → b ≡ y)
-  eqv2 = λ i → (y : A≡B i) → a≡b i ≡ y
+  -- eqv2 : ((y : A) → a ≡ y) ≡ ((y : B) → b ≡ y)
+  -- eqv2 = λ i → (y : A≡B i) → a≡b i ≡ y
 
-  T1 = λ { (i = i0) → ((y : A) → a ≡ y) ; (i = i1) → ((y : B) → b ≡ y) }
-  e1 = λ { (i = i0) → pathToEquiv eqv2 ; (i = i1) → idEquiv ((y : B) → b ≡ y) }
-  Uhh = primGlue ((y : B) → b ≡ y) T1 e1
+  -- T1 = λ { (i = i0) → ((y : A) → a ≡ y) ; (i = i1) → ((y : B) → b ≡ y) }
+  -- e1 = λ { (i = i0) → pathToEquiv eqv2 ; (i = i1) → idEquiv ((y : B) → b ≡ y) }
+  -- Uhh = primGlue ((y : B) → b ≡ y) T1 e1
       
-  uhh : Uhh
-  uhh = glue {T = T1} {e = e1} (λ { (i = i0) → Acontr ; (i = i1) → Bcontr }) λ y j → {! Bcontr y j  !}
+  -- uhh : Uhh
+  -- uhh = glue {T = T1} {e = e1} (λ { (i = i0) → Acontr ; (i = i1) → Bcontr }) λ y j → {! Bcontr y j  !}
+
+  Acontr-is-Prop : isProp ((y : A) → a ≡ y)
 
   wtf : PathP (λ i → (y : A≡B i) → a≡b i ≡ y) Acontr Bcontr
   wtf = λ i y j → {!   !}

talks/2024-grads/.gitignore

@@ -1 +1,9 @@
 main.pdf
+*-blx.bib
+*.aux
+*.log
+*.nav
+*.out
+*.run.xml
+*.snm
+*.toc

talks/2024-grads/Demo.agda

@@ -6,12 +6,28 @@ open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.PropositionalEquality using (module ≡-Reasoning)
 open import Tactic.RingSolver.Core.AlmostCommutativeRing using (AlmostCommutativeRing)
 open import Data.Nat.Tactic.RingSolver
+open import Data.Bool
+open import Data.Bool.Properties
 open ≡-Reasoning
 
 sumTo : ℕ → ℕ
 sumTo zero = zero 
 sumTo (suc n) = (suc n) + (sumTo n)
 
+isEven : ℕ → Bool
+isEven zero = true
+isEven (suc x) = not (isEven x)
+
+example1 : isEven 5 ≡ false
+example1 = refl
+
+eee : ∀ (m n : ℕ) → isEven m ≡ true → isEven n ≡ true → isEven (m + n) ≡ true
+eee zero n m-even n-even = n-even
+eee (2+ m) n m-even n-even =
+  let IH = eee m n (trans (sym (not-involutive (isEven m))) m-even) n-even in
+  trans (not-involutive (isEven (m + n))) IH
+
+
 lemma : ∀ (n : ℕ) → 2 * suc n + n * (n + 1) ≡ suc n * (suc n + 1)
 lemma = solve-∀
 
@@ -30,3 +46,7 @@ theorem (suc n) =
     ≡⟨ lemma n ⟩
         (suc n) * ((suc n) + 1)
     ∎
+
+data Vec (A : Set) (n : ℕ) : Set where
+   
+z = let z1 = Vec in {!   !}

talks/2024-grads/Makefile

@@ -1,7 +1,11 @@
-.PHONY: watch
+.PHONY: watch clean
 
 main.pdf: main.tex
-	tectonic $<
+	make clean
+	pdflatex main.tex
 
 watch:
-	watchexec -e tex,bib make main.pdf
+	watchexec -e tex,bib -r --stop-timeout 0 make main.pdf
+
+clean:
+	rm -f *-blx.bib *.aux *.log *.nav *.out *.run.xml *.snm *.toc *.pdf

talks/2024-grads/main.tex

@@ -1,15 +1,18 @@
-\documentclass[a4paper,xcolor={dvipsnames}]{beamer}
+\documentclass[a4paper]{beamer}
 \useoutertheme{miniframes}
 % \usetheme{Darmstadt}
 
 \usepackage[TU,T1]{fontenc}
-\usepackage{hyperref}
-\usepackage[backend=bibtex,style=numeric-comp,sorting=none]{biblatex}
+% \usepackage{hyperref}
 \usepackage{bussproofs}
+\usepackage{colortbl}
 \usepackage{geometry}
 
-\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}
 
 \title{Formalizing mathematics with cubical type theory}
@@ -42,19 +45,20 @@
   \begin{itemize}
     \item Why formalize proofs?
     \note[item]{Why: Would be nice to get computers to check our work for us}
+    \pause
 
     \item What can we formalize?
     \note[item]{What: Program properties, compiler optimizations, correctness}
-    \note[item]{Notably, can NOT prove some things, Rice's theorem}
+    \pause
 
-    \note[item]{Talk about proofs vs. testing}
-    \item How to formalize proofs?
-    \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 How to formalize proofs?
+    % \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 $$}
+    % \pause
 
     \item What are some existing theorem provers?
     \begin{itemize}
-      \item Rocq (Coq), Lean, Agda, F*, Idris, Metamath, HOL, ...
+      \item Rocq (Coq), Lean, Agda
     \end{itemize}
   \end{itemize}
 \end{frame}
@@ -66,16 +70,19 @@
 \section{Type theory}
 
 \begin{frame}
-  \frametitle{Proofs are programs}
+  \frametitle{Set theory}
 
   \begin{itemize}
-    \item Curry-Howard isomorphism
-    \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
+    \item Math is built upon sets
+    \pause
+
+    \item We often operate at a much higher level
+    \pause
+
+    \item Skip the details
+    \pause
+
+    \item We can't do this for mechanized systems!
   \end{itemize}
 \end{frame}
 
@@ -87,19 +94,85 @@
   Talk about set theory
 \end{frame}
 
+\begin{frame}
+  \frametitle{Introducing the type}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.75\textwidth]{images/type.png}
+  \end{figure}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Proofs are programs}
+
+  \begin{table}[]
+    \begin{tabular}{c|c}
+    \hline
+    Logic side                     & Programming side              \\ \hline \hline
+    formula                        & type                          \\ \hline
+    proof                          & term                          \\ \hline
+    formula is true                & type has an element           \\ \hline
+    formula is false               & type does not have an element \\ \hline
+    logical constant $\top$ (truth)     & unit type                     \\ \hline
+    logical constant $\bot$ (falsehood) & empty type                    \\ \hline
+    implication                    & function type                 \\ \hline
+    conjunction                    & product type                  \\ \hline
+    disjunction                    & sum type                      \\ \hline \onslide<+(1)->
+    universal quantification       & dependent product type        \\ \hline
+    existential quantification     & dependent sum type            \\ \hline
+    \end{tabular}
+  \end{table}
+\end{frame}
+
 \begin{frame}
   \frametitle{Important features of Martin-L{\"o}f type theory}
 
   \begin{itemize}
-    \item Types instead of sets
-    \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}$.
+    \pause
+    \item Stratified universes: $\mathsf{Type}_0, \mathsf{Type}_1, \mathsf{Type}_2, \dots$
 
+    \pause
+    \item Inductive types, defined by type former, constructors, eliminators, and computation rules
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Important features of Martin-L{\"o}f type theory}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.5\textwidth]{images/nat.png}
+  \end{figure}
+  \pause
+
+  \begin{itemize}
+    \item
+    For example, $\mathbb{N}$ is defined with 2 possible constructors: $\mathsf{zero}$ and $\mathsf{suc}$.
+
+    \begin{columns} 
+      \begin{column}{.3\textwidth}
+        \begin{prooftree}
+          \AxiomC{}
+          \UnaryInfC{$\Gamma \vdash \mathsf{zero} : \mathbb{N}$}
+        \end{prooftree}
+      \end{column}
+      \begin{column}{.3\textwidth}
+        \begin{prooftree}
+          \AxiomC{$\Gamma \vdash n : \mathbb{N}$}
+          \UnaryInfC{$\Gamma \vdash \mathsf{suc}(n) : \mathbb{N}$}
+        \end{prooftree}
+      \end{column}
+    \end{columns}
+
+    \pause
+    \item
+    Elimination rule for $\mathbb{N}$:
     \begin{prooftree}
-      \AxiomC{$ \Gamma \vdash c_0 : C $}
-      \AxiomC{$ \Gamma , x : \mathbb{N} , y : C \vdash c_s : C $}
+      \AxiomC{$ \Gamma \vdash c_z : C $}
+      \AxiomC{$ \Gamma , (x : \mathbb{N}) , (y : C) \vdash (c_s : C) $}
       \AxiomC{$ \Gamma \vdash n : \mathbb{N} $}
-      \TrinaryInfC{$ \Gamma \vdash \mathsf{ind}_{\mathbb{N}} (c_0 , x . y . c_s , n) : C $}
+      \TrinaryInfC{$ \Gamma \vdash \mathsf{ind}_{\mathbb{N}} (c_z , x . y . c_s , n) : C $}
     \end{prooftree}
   \end{itemize}
 \end{frame}
@@ -108,61 +181,162 @@
   \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
-
-    $$ \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}
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.7\textwidth]{images/sigma.png}
+  \end{figure}
+
+  \pause
+  \begin{columns}
+    \begin{column}{.3\textwidth}
+      $$ \mathsf{isEven} : \mathbb{N} \rightarrow \mathsf{Type} $$
+    \end{column}
+    \begin{column}{.3\textwidth}
+      $$ \mathsf{Even} : \sum_{n : \mathbb{N}} \mathsf{isEven}(n) $$
+    \end{column}
+  \end{columns}
 \end{frame}
 
 \begin{frame}
   \frametitle{Important features of Martin-L{\"o}f type theory}
 
+  \begin{itemize}
+    \item \emph{Dependent functions}, or $\Pi$-types
+    \pause
+    
+    \begin{equation*}
+    \begin{aligned}
+      \mathsf{List} &: \mathsf{Type} \rightarrow \mathsf{Type} \\
+      \onslide<+(1)->
+      \mathsf{Vec} &: \mathsf{Type} \rightarrow \mathbb{N} \rightarrow \mathsf{Type}
+    \end{aligned}
+    \end{equation*}
+
+  \end{itemize}
+
+  \pause
+  $$ \mathsf{append} : \prod_{A : \mathsf{Type}} \left( \prod_{m, n : \mathbb{N}} \left( \mathsf{Vec}(A, m) \rightarrow \mathsf{Vec}(A, n) \rightarrow \mathsf{Vec}(A, m + n) \right) \right) $$
+
+\end{frame}
+
+\begin{frame}
+  \frametitle{Important features of Martin-L{\"o}f type theory}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.5\textwidth]{images/id.png}
+  \end{figure}
+
   \begin{itemize}
     \item The identity type, $\mathsf{Id}_A(x, y)$, for some $x, y : A$
+    \pause
     \item Also written as $x \equiv_A y$, or just $x \equiv y$ if $A$ is obvious
+    \pause
     \item Single constructor: $\mathsf{refl}_x : \mathsf{Id}_A(x, x)$
   \end{itemize}
 \end{frame}
 
+\begin{frame}
+  \frametitle{Important features of Martin-L{\"o}f type theory}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.5\textwidth]{images/id2.png}
+  \end{figure}
+
+  \begin{itemize}
+    \item There can be multiple paths between points!
+  \end{itemize}
+\end{frame}
+
 \begin{frame}
   \frametitle{Homotopy type theory}
 
-  \newcommand{\htcolor}[1]{\textcolor{Melon}{####1}}
-  \newcommand{\ttcolor}[1]{\textcolor{Periwinkle}{####1}}
+  \newcommand{\htcolor}[1]{\textcolor{red}{####1}}
+  \newcommand{\ttcolor}[1]{\textcolor{blue}{####1}}
 
   \begin{itemize}
-    \item A \htcolor{"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 \ttcolor{$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 \htcolor{paths between points in a space} as the \ttcolor{identity type $\mathsf{Id}$}
+    \item A 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 consider two functions $f, g : A \rightarrow B$ as being homotopic if we can inhabit $h : (x : A) \rightarrow f(x) \equiv g(x)$
+    % \item Note: assume all functions are continuous.
+
+    \begin{figure}
+      \centering
+      \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}$}}
   \end{itemize}
 \end{frame}
 
 \begin{frame}
-  \frametitle{Equivalences}
+  \frametitle{Homotopy type theory}
 
-  \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{figure}
+    \centering
+    \includegraphics[width=0.8\textwidth]{images/paths.png}
+  \end{figure}
+
+  \note[item]{We consider these "paths" to be our identities}
+  \note[item]{The continuousness is important because it means that we can't just connect any two elements, they still have to be constructed uniformly}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Isomorphism}
+
+  \begin{columns}
+    \begin{column}{0.5\textwidth}
       \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{column}
+    \begin{column}{0.5\textwidth}
+      \begin{figure}
+        \centering
+        \includegraphics[width=0.8\textwidth]{images/maps.png}
+      \end{figure}
+    \end{column}
+  \end{columns}
+
+
+  \begin{columns}
+    \begin{column}{0.5\textwidth}
+      \begin{itemize}
+        \item $\prod_{(a: A)} g(f(a)) \equiv a$
+        \item $\prod_{(b: B)} f(g(b)) \equiv b$
+      \end{itemize}
+    \end{column}
+    \begin{column}{0.5\textwidth}
+      \begin{figure}
+        \centering
+        \includegraphics[width=0.8\textwidth]{images/mapsid.png}
+      \end{figure}
+    \end{column}
+  \end{columns}
+
+  \note[item]{Equivalence is sort of like an upgraded isomorphism}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Univalence}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.7\textwidth]{images/ua.png}
+  \end{figure}
+
+  \begin{itemize}
+    \item Equivalences \emph{are} identities
   \end{itemize}
 \end{frame}
 
 \begin{frame}
-  \frametitle{Univalence axiom}
+  \frametitle{Univalence}
 
   \begin{itemize}
     \item Equivalences \emph{are} identities
@@ -172,20 +346,63 @@
     \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
 
+    \pause
     \item Importantly, there can be multiple inhabitants of $A \equiv B$
-    \begin{itemize} \item Booleans! \end{itemize}
+    \begin{itemize}
+      \item Booleans! \\ 
+      $\mathsf{ua}(\mathsf{id})$ and $\mathsf{ua}(\mathsf{not})$ are different elements of $\mathsf{Bool} \equiv \mathsf{Bool}$
+    \end{itemize}
 
+    \pause
     \item
     Transport allows you to use $A$ and $B$ interchangeably
   \end{itemize}
+
+    $$ \mathsf{transport} : (P : (X : \mathsf{Type}) \rightarrow \mathsf{Type}) \rightarrow (p : x \equiv_X y) \rightarrow P(x) \rightarrow P(y) $$
 \end{frame}
 
 \begin{frame}
   \frametitle{Univalence axiom?}
 
   \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}$.
+    \item Unfortunately, univalence does not compute in Book HoTT
+    \pause
+    \item Assume the functions we want as axioms
+  \end{itemize}
+
+  $$
+    \mathsf{ua} : (A \simeq B) \rightarrow (A \equiv B)
+  $$
+\end{frame}
+
+\begin{frame}
+  \frametitle{Higher inductive types}
+
+  \note[item]{Another way to inject paths into a type}
+
+  \begin{itemize}
+    \item Normally inductive types give us ways to construct \emph{points}
+    \pause
+    \item Higher inductive types give us ways to construct \emph{paths}
+  \end{itemize}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.5\textwidth]{images/zquot.png}
+  \end{figure}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Circle ($S^1$)}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.4\textwidth]{images/s1.png}
+  \end{figure}
+
+  \begin{itemize}
+    \item $\mathsf{base} : S^1$, some arbitrary base point
+    \item $\mathsf{loop} : \mathsf{base} \equiv \mathsf{base}$, a path representing the rest of the circle
   \end{itemize}
 \end{frame}
 
@@ -194,13 +411,32 @@
 
   \begin{itemize}
     \item Make paths based on the interval type $I$ which represents $[0, 1]$
-    \item The interval is a primitive construct
+    \item The interval is a primitive construct!
+  \end{itemize}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.4\textwidth]{images/interval.png}
+  \end{figure}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Cubical type theory}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.3\textwidth]{images/box.png}
+  \end{figure}
+
+  \begin{itemize}
+    \note[item]{I'll get into \emph{how} to construct squares and paths later}
     \item Construct squares and cubes to create paths by composition and filling
+    \pause
     \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
+        \item Transport is a primitive notion
+        % \item Path induction defined in terms of transport instead
+        \item Makes the univalence "axiom" definable
       \end{itemize}
   \end{itemize}
 \end{frame}
@@ -211,29 +447,23 @@
   \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)
+    \item One central idea of algebraic topology: identify which spaces are different from each other
+    (i.e donuts and coffee mugs are different from a solid sphere)
+    \pause
+    \item The fundamental group is one metric of identifying spaces
+    \note[item]{fundamental group is a special case of a homotopy group}
   \end{itemize}
 \end{frame}
 
 \begin{frame}
-  \frametitle{The circle}
+  \frametitle{Revisiting 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 Constructed as a higher inductive type
-    \item $\mathsf{base} : S^1$, some arbitrary base point
-    \item $\mathsf{loop} : \mathsf{base} \equiv \mathsf{base}$, a path representing the rest of the circle
+    \item The circle ($S^1$) is an example of a simple but non-trivial space because of the loop
+    \pause
+    \item Determining fundamental groups of $n$-spheres is a difficult problem in algebraic topology
+    \pause
+    \item Fortunately, $\pi_1(S^1)$ is easy
   \end{itemize}
 \end{frame}
 
@@ -373,7 +603,7 @@
 
   \bigskip
 
-  \printbibliography
+  % \printbibliography
 \end{frame}
 
 \end{document}