From fd5b32c47fd6c58167c71881362fc88585596357 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Sun, 20 Oct 2024 18:02:02 -0500
Subject: [PATCH] update

---
 talks/2024-grads/Demo.agda | 12 ++++++++++++
 talks/2024-grads/main.tex  |  4 ++--
 2 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/talks/2024-grads/Demo.agda b/talks/2024-grads/Demo.agda
index 02d32a5..69d7361 100644
--- a/talks/2024-grads/Demo.agda
+++ b/talks/2024-grads/Demo.agda
@@ -10,3 +10,15 @@ open import Data.Bool
 open import Data.Bool.Properties
 open ≡-Reasoning
 
+isEven : ℕ → Bool
+isEven zero = true 
+isEven (suc n) = not (isEven n)
+
+example : isEven 5 ≡ false
+example = refl
+
+e+e≡e : ∀ (m n : ℕ) → isEven m ≡ true → isEven n ≡ true → isEven (m + n) ≡ true
+e+e≡e zero n m-even n-even = n-even
+e+e≡e (2+ m) n m-even n-even =
+  let IH = e+e≡e m n (trans (sym (not-involutive (isEven m))) m-even) n-even in
+  trans (not-involutive (isEven (m + n))) IH 
\ No newline at end of file
diff --git a/talks/2024-grads/main.tex b/talks/2024-grads/main.tex
index d01a5bf..1be8535 100644
--- a/talks/2024-grads/main.tex
+++ b/talks/2024-grads/main.tex
@@ -1,4 +1,4 @@
-\documentclass[a4paper]{beamer}
+\documentclass[handout,a4paper]{beamer}
 \useoutertheme{miniframes}
 % \usetheme{Darmstadt}
 
@@ -13,7 +13,7 @@
 \nocite{*}
 
 % \setbeamercovered{transparent}
-\setbeameroption{show notes on second screen=right}
+% \setbeameroption{show notes on second screen=right}
 
 \title{Formalizing mathematics with cubical type theory}
 \author{Michael Zhang}