From 1aeebb0c392736989a98d650443af4e8c73f74c7 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Fri, 18 Oct 2024 10:51:15 -0500 Subject: [PATCH] demo --- talks/2024-grads/Demo.agda | 40 ------------------ talks/2024-grads/Demo1.agda | 26 +++++++++--- talks/2024-grads/main.tex | 82 ++++++++++++++++++------------------- 3 files changed, 60 insertions(+), 88 deletions(-) diff --git a/talks/2024-grads/Demo.agda b/talks/2024-grads/Demo.agda index c3c6ab0..02d32a5 100644 --- a/talks/2024-grads/Demo.agda +++ b/talks/2024-grads/Demo.agda @@ -10,43 +10,3 @@ 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-∀ - -theorem : ∀ (n : ℕ) → 2 * sumTo n ≡ (n * (n + 1)) -theorem zero = refl -theorem (suc n) = - let IH = theorem n in - begin - 2 * (sumTo (suc n)) - ≡⟨⟩ - 2 * ((suc n) + (sumTo n)) - ≡⟨ *-distribˡ-+ 2 (suc n) (sumTo n) ⟩ - 2 * (suc n) + 2 * (sumTo n) - ≡⟨ cong (2 * (suc n) +_) IH ⟩ - 2 * (suc n) + (n * (n + 1)) - ≡⟨ lemma n ⟩ - (suc n) * ((suc n) + 1) - ∎ - -data Vec (A : Set) (n : ℕ) : Set where - -z = let z1 = Vec in {! !} \ No newline at end of file diff --git a/talks/2024-grads/Demo1.agda b/talks/2024-grads/Demo1.agda index 8222437..9210ea5 100644 --- a/talks/2024-grads/Demo1.agda +++ b/talks/2024-grads/Demo1.agda @@ -1,11 +1,27 @@ module 2024-grads.Demo1 where open import Data.Nat +open import Data.Nat.Properties +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 Relation.Binary.PropositionalEquality as Eq +open import Data.Bool +open import Data.Bool.Properties +open ≡-Reasoning -_ : 1 + 1 ≡ 2 -_ = refl +isEven : ℕ → Bool +isEven zero = true +isEven (suc x) = not (isEven x) -commutativity : (m n : ℕ) → m + n ≡ n + m -commutativity = solve-∀ \ No newline at end of file +example1 : isEven 5 ≡ false +example1 = refl + +z = not-involutive + +eee : ∀ (m n : ℕ) → isEven m ≡ true → isEven n ≡ true → isEven (m + n) ≡ true +eee zero n m-is-even n-is-even = n-is-even +eee (2+ m) n m-is-even n-is-even = + let helper = not-involutive (isEven m) in + let IH = eee m n (trans (sym helper) m-is-even) n-is-even in + trans (not-involutive (isEven (m + n))) IH diff --git a/talks/2024-grads/main.tex b/talks/2024-grads/main.tex index 1cf686d..d01a5bf 100644 --- a/talks/2024-grads/main.tex +++ b/talks/2024-grads/main.tex @@ -12,7 +12,7 @@ \addbibresource{references.bib} \nocite{*} -\setbeamercovered{transparent} +% \setbeamercovered{transparent} \setbeameroption{show notes on second screen=right} \title{Formalizing mathematics with cubical type theory} @@ -88,12 +88,6 @@ -\begin{frame} - \frametitle{Set theory} - - Talk about set theory -\end{frame} - \begin{frame} \frametitle{Introducing the type} @@ -403,41 +397,6 @@ \end{itemize} \end{frame} -\begin{frame} - \frametitle{Cubical type theory} - - \begin{itemize} - \item Make paths based on the interval type $I$ which represents $[0, 1]$ - \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 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} - \section{Fundamental group of a circle} \begin{frame} @@ -448,6 +407,7 @@ (i.e donuts and coffee mugs are different from a solid sphere) \pause \item The fundamental group is one metric of identifying spaces + \item The fundamental group measures the "loop space" \note[item]{fundamental group is a special case of a homotopy group} \end{itemize} @@ -458,7 +418,7 @@ \end{frame} \begin{frame} - \frametitle{Revisiting the circle} + \frametitle{The fundamental group of the circle} \begin{itemize} \item The circle ($S^1$) is an example of a simple but non-trivial space because of the loop @@ -612,6 +572,42 @@ \end{itemize} \end{frame} +\begin{frame} + \frametitle{Cubical type theory} + + \begin{itemize} + \item Make paths based on the interval type $I$ which represents $[0, 1]$ + \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 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} + + \begin{frame} \frametitle{Composition}