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

update

Browse source
This commit is contained in:
Michael Zhang 2024-10-20 18:02:02 -05:00
parent 2b9e0402bf
commit fd5b32c47f
2 changed files with 14 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
talks/2024-grads/Demo.agda
View file

@ -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

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

@ -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}