talk

src/CubicalHott/Theorem7-1-11.agda

@@ -12,30 +12,63 @@ open import Cubical.Data.Nat
 open import Data.Unit
 
 lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n)
-lemma zero (A , a , Acontr) (B , b , Bcontr) i = G , g , contr where
-
+lemma zero (A , a , Acontr) (B , b , Bcontr) i = A≡B i , a≡b i , eq where
   eqv1 : A ≃ B
   eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr)
 
-  T = λ { (i = i0) → A ; (i = i1) → B }
-  e = λ { (i = i0) → eqv1 ; (i = i1) → idEquiv B }
+  A≡B : A ≡ B
+  A≡B = ua eqv1
 
-  G = primGlue B T e
-  g = glue {T = T} {e = e} (λ { (i = i0) → a ; (i = i1) → b }) b
+  a≡b : PathP (λ i → A≡B i) a b
+  a≡b j = glue (λ { (j = i0) → a ; (j = i1) → b }) b
 
-  -- at i = i0, y = a
-  -- at i = i1, y = b
+  eq : (y : A≡B i) → a≡b i ≡ y
+  eq y j = {!   !}
+    -- a≡b i ≡ y
+    -- ———— Boundary (wanted) —————————————————————————————————————
+    -- i = i0 ⊢ λ i₁ → Acontr y i₁
+    -- i = i1 ⊢ λ i₁ → Bcontr y i₁
 
-  -- For some arbitrary y : G, prove g ≡ y
-  contr : (y : G) → g ≡ y
-  contr y j = {!   !}
-    -- let p = λ where
-    --   (i = i0) → {!   !} -- Acontr (unglue {A = A} (~ i) {T = T} {e = λ { (i = i0) → idEquiv A }} y) j
-    --   (i = i1) → Bcontr (unglue {A = B} i {T = T} {e = λ { (i = i1) → idEquiv B }} y) j
-    -- in glue p (Bcontr {! g  !} {! j  !})
+  -- z = let
+  --     z1 = λ (y : A≡B i) (j : I) →
+  --       let u = λ k → λ where
+  --         (i = i0) → Acontr y (~ j)
+  --         (i = i1) → Bcontr y j
+  --         (j = i0) → a≡b i
+  --         (j = i1) → {!  y i !}
+  --       in hfill u (inS (a≡b {! j  !})) j
+  --   in {!   !}
 
-    -- unglue i {!   !}
-    -- (glue (λ { (i = i1) → {!   !} }) {!   !})
-    -- (glue (λ { (i = i0) → a ; (i = i1) → b }) b))
-lemma (suc n) x y = {!   !}
+
+lemma (suc zero) (A , A-prop) (B , B-prop) x y i j = {!   !} where
+
+lemma (suc (suc n)) x y = {!   !}
+
+-- lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n)
+-- lemma zero (A , a , Acontr) (B , b , Bcontr) i = G , g , contr where
+
+--   eqv1 : A ≃ B
+--   eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr)
+
+--   T = λ { (i = i0) → A ; (i = i1) → B }
+--   e = λ { (i = i0) → eqv1 ; (i = i1) → idEquiv B }
+
+--   G = primGlue B T e
+--   g = glue {T = T} {e = e} (λ { (i = i0) → a ; (i = i1) → b }) b
+
+--   -- at i = i0, y = a
+--   -- at i = i1, y = b
+
+--   -- For some arbitrary y : G, prove g ≡ y
+--   contr : (y : G) → g ≡ y
+--   contr y j = {!   !}
+--     -- let p = λ where
+--     --   (i = i0) → {!   !} -- Acontr (unglue {A = A} (~ i) {T = T} {e = λ { (i = i0) → idEquiv A }} y) j
+--     --   (i = i1) → Bcontr (unglue {A = B} i {T = T} {e = λ { (i = i1) → idEquiv B }} y) j
+--     -- in glue p (Bcontr {! g  !} {! j  !})
+
+--     -- unglue i {!   !}
+--     -- (glue (λ { (i = i1) → {!   !} }) {!   !})
+--     -- (glue (λ { (i = i0) → a ; (i = i1) → b }) b))
+-- lemma (suc n) x y = {!   !}
  

talks/2024-grads/.gitignore

@@ -0,0 +1 @@
+main.pdf

talks/2024-grads/Demo.agda

@@ -0,0 +1,26 @@
+module 2024-grads.Demo where
+
+open import Data.Nat
+open import Relation.Binary.PropositionalEquality using (module ≡-Reasoning)
+open import Tactic.RingSolver.Core.AlmostCommutativeRing using (AlmostCommutativeRing)
+open import Data.Nat.Tactic.RingSolver
+
+sumTo : ℕ → ℕ
+sumTo zero = zero 
+sumTo (suc n) = (suc n) + (sumTo n)
+
+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))
+    ≡⟨ {!  solve-∀ !} ⟩
+        (suc n) * ((suc n) + 1)
+    ∎

talks/2024-grads/Makefile

@@ -0,0 +1,2 @@
+main.pdf: main.tex
+	tectonic $<

talks/2024-grads/main.tex

@@ -0,0 +1,83 @@
+\documentclass{beamer}
+\usetheme{Darmstadt}
+\usepackage{bussproofs}
+
+\setbeameroption{show notes on second screen=right}
+
+\title{Formalizing mathematics with cubical type theory}
+\author{Michael Zhang}
+% \institute{Overleaf}
+% \date{2021}
+
+\begin{document}
+
+\frame{\titlepage}
+
+\section{Theorem prover intro}
+
+\begin{frame}
+  \frametitle{Intro}
+
+  \begin{itemize}
+    \item Why formalize proofs?
+    \note[item]{Why: Would be nice to get computers to check our work for us}
+
+    \item What can we formalize?
+    \note[item]{What: Program properties, compiler optimizations, correctness}
+    \note[item]{Notably, can NOT prove some things, Rice's theorem}
+
+    \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 What does the current state of the ecosystem look like?
+    \begin{itemize}
+      \item Coq, Lean, Agda, ...
+    \end{itemize}
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Demo}
+\end{frame}
+
+\section{Homotopy type theory}
+
+\begin{frame}
+  \frametitle{Curry-Howard Isomorphism, or "proofs are programs"}
+
+  \begin{tabular}{c|c}
+    Logic & Programming \\
+    \hline
+    c & d \\
+  \end{tabular}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Martin-L{\"o}f type theory}
+
+  \begin{itemize}
+    \item Inductive types
+    \\
+    For example, $\mathbb{N}$ is defined with one of 2 constructors: $\mathsf{zero}$ and $\mathsf{suc}$.
+    Its induction principle \footnotemark is:
+
+    \begin{prooftree}
+      \AxiomC{$ \Gamma \vdash c_0 : 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 $}
+    \end{prooftree}
+
+    \item \emph{Dependent types}:
+    $$ \mathsf{Vec} : (A : \mathsf{Type}) \rightarrow (n : \mathbb{N}) \rightarrow \mathsf{Type} $$
+  \end{itemize}
+
+  \footnotetext[1]{This is the non-dependent version of the induction principle}
+\end{frame}
+
+\section{Fundamental group of a circle}
+
+\begin{frame} \end{frame}
+
+\end{document}

type-theory.agda-lib

@@ -1,2 +1,2 @@
-include: src src/ThesisWork
-depend: standard-library cubical agda-unimath
+include: src src/ThesisWork talks
+depend: standard-library cubical