demo

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 {!   !}

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-∀
+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

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}