work

src/CubicalHott/Chapter3.agda

@@ -1,51 +1,51 @@
-{-# OPTIONS --cubical #-}
-module CubicalHott.Chapter3 where
-
-open import CubicalHott.Prelude
-open import CubicalHott.Chapter2
-open import Cubical.Data.Bool
-open import Cubical.Data.Equality using (id; ap)
-
-private
-  variable
-    l : Level
-
-module example319 where
-  lemma : ¬ isSet (Type l)
-  lemma {l} p = remark2126.lemma fatal where
-    not* : Bool* {l} → Bool* {l}
-    not* (lift false) = lift true
-    not* (lift true) = lift false
-
-    notnot* : (x : Bool* {l}) → not* (not* x) ≡ x
-    notnot* (lift true) = refl
-    notnot* (lift false) = refl
-
-    notIso* : Iso (Bool* {l}) (Bool* {l})
-    Iso.fun notIso* = not*
-    Iso.inv notIso* = not*
-    Iso.rightInv notIso* = notnot*
-    Iso.leftInv notIso* = notnot*
-
-    notEquiv* : Bool* {l} ≃ Bool* {l}
-    notEquiv* = not* , isoToIsEquiv notIso*
-
-    fPath : Bool* {ℓ = l} ≡ Bool* {ℓ = l}
-    fPath = ua notEquiv*
-
-    getFunc : Bool* ≡ Bool* → Bool* → Bool*
-    getFunc path = pathToEquiv path .fst
-    
-    left : getFunc fPath ≡ not*
-    left = cong fst (pathToEquiv-ua notEquiv*)
-
-    right : getFunc fPath ≡ id
-    right = cong getFunc (helper ∙ sym uaIdEquiv) ∙ cong fst (pathToEquiv-ua (idEquiv Bool*)) where
-      helper : fPath ≡ refl
-      helper = p Bool* Bool* fPath refl
-
-    bogus : not* ≡ id
-    bogus = sym left ∙ right
-
-    fatal : true ≡ false
+{-# OPTIONS --cubical #-}
+module CubicalHott.Chapter3 where
+
+open import CubicalHott.Prelude
+open import CubicalHott.Chapter2
+open import Cubical.Data.Bool
+open import Cubical.Data.Equality using (id; ap)
+
+private
+  variable
+    l : Level
+
+module example319 where
+  lemma : ¬ isSet (Type l)
+  lemma {l} p = remark2126.lemma fatal where
+    not* : Bool* {l} → Bool* {l}
+    not* (lift false) = lift true
+    not* (lift true) = lift false
+
+    notnot* : (x : Bool* {l}) → not* (not* x) ≡ x
+    notnot* (lift true) = refl
+    notnot* (lift false) = refl
+
+    notIso* : Iso (Bool* {l}) (Bool* {l})
+    Iso.fun notIso* = not*
+    Iso.inv notIso* = not*
+    Iso.rightInv notIso* = notnot*
+    Iso.leftInv notIso* = notnot*
+
+    notEquiv* : Bool* {l} ≃ Bool* {l}
+    notEquiv* = not* , isoToIsEquiv notIso*
+
+    fPath : Bool* {ℓ = l} ≡ Bool* {ℓ = l}
+    fPath = ua notEquiv*
+
+    getFunc : Bool* ≡ Bool* → Bool* → Bool*
+    getFunc path = pathToEquiv path .fst
+    
+    left : getFunc fPath ≡ not*
+    left = cong fst (pathToEquiv-ua notEquiv*)
+
+    right : getFunc fPath ≡ id
+    right = cong getFunc (helper ∙ sym uaIdEquiv) ∙ cong fst (pathToEquiv-ua (idEquiv Bool*)) where
+      helper : fPath ≡ refl
+      helper = p Bool* Bool* fPath refl
+
+    bogus : not* ≡ id
+    bogus = sym left ∙ right
+
+    fatal : true ≡ false
     fatal = cong (λ f → lower (f (lift true))) (sym bogus) 

src/CubicalHott/Chapter6.agda

@@ -1,103 +1,103 @@
-{-# OPTIONS --cubical #-}
-module CubicalHott.Chapter6 where
-
-open import CubicalHott.Prelude
-open import CubicalHott.Chapter3
-open import Cubical.Data.Equality.Conversion
-open import Cubical.HITs.Susp
-open import Cubical.HITs.S1
-open import Cubical.Data.Int
-open import Cubical.Data.Nat
-open import Cubical.Data.Bool
-
-private
-  variable
-    l l2 : Level
-
--- Equation 6.2.2
-
-dep-path : {A : Type} → (P : A → Type) → {x y : A} → (p : x ≡ y) → (u : P x) → (v : P y) → Type
-dep-path P p u v = subst P p u ≡ v
-
-syntax dep-path P p u v = u ≡[ P , p ] v
-
--- Lemma 6.2.5
-
-module lemma625 where
-  f : {A : Type} {a : A} {p : a ≡ a} → S¹ → A
-  f {a = a} base = a 
-  f {p = p} (loop i) = p i
-
--- Lemma 6.2.8
-
--- module lemma628 where
---   lemma : {A : Type}
---     → (f g : S¹ → A)
---     → (p : f base ≡ g base)
---     → (q : cong f loop ≡[ (λ x → x ≡ x) , p ] cong g loop)
---     → (x : S¹) → f x ≡ g x
---   lemma f g p q base i = p i 
---   lemma f g p q (loop j) i = {!   !}
-
--- Interval
-
-data [0,1] : Type where
-  ii0 : [0,1]
-  ii1 : [0,1]
-  seg : ii0 ≡ ii1
-
--- Lemma 6.3.1
-
-module lemma631 where
-  lemma : isContr [0,1]
-  lemma = ii0 , f where
-    f : (y : [0,1]) → ii0 ≡ y
-    f ii0 = refl 
-    f ii1 = seg
-    f (seg i) j = seg (i ∧ j) 
-    
--- Lemma 6.3.2
-
-module lemma632 where
-  lemma : {A B : Type}
-    → (f g : A → B)
-    → ((x : A) → f x ≡ g x)
-    → f ≡ g
-  lemma {A} {B} f g p i = q (seg i) where
-    p̃ : (x : A) → [0,1] → B
-    p̃ x ii0 = f x
-    p̃ x ii1 = g x
-    p̃ x (seg i) = p x i
-
-    q : [0,1] → (A → B)
-    q i x = p̃ x i
-    
--- Lemma 6.4.1
-
--- module lemma641 where
---   lemma : loop ≢ refl
---   lemma loop≡refl = example319.lemma g where
---     goal : {A : Type l} {x : A} {p : x ≡ x} → (q' : x ≡ x) → refl ≡ q'
---     goal {A = A} {x} {p} q' = z1 ∙ {!   !} ∙ z3 where
---       f : S¹ → A
---       f base = x
---       f (loop i) = q' i
-
---       z1 : refl ≡ cong f refl
---       z1 = refl
---       z2 : cong f refl ≡ cong f loop
---       z2 = cong (cong f) loop≡refl
---       z3 : cong f loop ≡ q'
---       z3 = refl
-    
---     g : isSet Type
---     g x y p q = J (λ y' p' → (q' : x ≡ y') → p' ≡ q') goal p q
-
--- Corollary 6.10.13
-
-module corollary61013 where
-  p^ : {A : Type l} {a : A} {p : a ≡ a} → (n : ℤ) → a ≡ a
-  p^ (pos zero) = refl
-  p^ {p = p} (pos (suc x)) = p^ {p = p} (pos x) ∙ p
-  p^ {p = p} (negsuc zero) = p^ {p = p} (pos zero) ∙ sym p
-  p^ {p = p} (negsuc (suc n)) = p^ {p = p} (negsuc n) ∙ sym p ∙ sym p
+{-# OPTIONS --cubical #-}
+module CubicalHott.Chapter6 where
+
+open import CubicalHott.Prelude
+open import CubicalHott.Chapter3
+open import Cubical.Data.Equality.Conversion
+open import Cubical.HITs.Susp
+open import Cubical.HITs.S1
+open import Cubical.Data.Int
+open import Cubical.Data.Nat
+open import Cubical.Data.Bool
+
+private
+  variable
+    l l2 : Level
+
+-- Equation 6.2.2
+
+dep-path : {A : Type} → (P : A → Type) → {x y : A} → (p : x ≡ y) → (u : P x) → (v : P y) → Type
+dep-path P p u v = subst P p u ≡ v
+
+syntax dep-path P p u v = u ≡[ P , p ] v
+
+-- Lemma 6.2.5
+
+module lemma625 where
+  f : {A : Type} {a : A} {p : a ≡ a} → S¹ → A
+  f {a = a} base = a 
+  f {p = p} (loop i) = p i
+
+-- Lemma 6.2.8
+
+-- module lemma628 where
+--   lemma : {A : Type}
+--     → (f g : S¹ → A)
+--     → (p : f base ≡ g base)
+--     → (q : cong f loop ≡[ (λ x → x ≡ x) , p ] cong g loop)
+--     → (x : S¹) → f x ≡ g x
+--   lemma f g p q base i = p i 
+--   lemma f g p q (loop j) i = {!   !}
+
+-- Interval
+
+data [0,1] : Type where
+  ii0 : [0,1]
+  ii1 : [0,1]
+  seg : ii0 ≡ ii1
+
+-- Lemma 6.3.1
+
+module lemma631 where
+  lemma : isContr [0,1]
+  lemma = ii0 , f where
+    f : (y : [0,1]) → ii0 ≡ y
+    f ii0 = refl 
+    f ii1 = seg
+    f (seg i) j = seg (i ∧ j) 
+    
+-- Lemma 6.3.2
+
+module lemma632 where
+  lemma : {A B : Type}
+    → (f g : A → B)
+    → ((x : A) → f x ≡ g x)
+    → f ≡ g
+  lemma {A} {B} f g p i = q (seg i) where
+    p̃ : (x : A) → [0,1] → B
+    p̃ x ii0 = f x
+    p̃ x ii1 = g x
+    p̃ x (seg i) = p x i
+
+    q : [0,1] → (A → B)
+    q i x = p̃ x i
+    
+-- Lemma 6.4.1
+
+-- module lemma641 where
+--   lemma : loop ≢ refl
+--   lemma loop≡refl = example319.lemma g where
+--     goal : {A : Type l} {x : A} {p : x ≡ x} → (q' : x ≡ x) → refl ≡ q'
+--     goal {A = A} {x} {p} q' = z1 ∙ {!   !} ∙ z3 where
+--       f : S¹ → A
+--       f base = x
+--       f (loop i) = q' i
+
+--       z1 : refl ≡ cong f refl
+--       z1 = refl
+--       z2 : cong f refl ≡ cong f loop
+--       z2 = cong (cong f) loop≡refl
+--       z3 : cong f loop ≡ q'
+--       z3 = refl
+    
+--     g : isSet Type
+--     g x y p q = J (λ y' p' → (q' : x ≡ y') → p' ≡ q') goal p q
+
+-- Corollary 6.10.13
+
+module corollary61013 where
+  p^ : {A : Type l} {a : A} {p : a ≡ a} → (n : ℤ) → a ≡ a
+  p^ (pos zero) = refl
+  p^ {p = p} (pos (suc x)) = p^ {p = p} (pos x) ∙ p
+  p^ {p = p} (negsuc zero) = p^ {p = p} (pos zero) ∙ sym p
+  p^ {p = p} (negsuc (suc n)) = p^ {p = p} (negsuc n) ∙ sym p ∙ sym p

src/CubicalHott/Lemma3-11-4.agda

@@ -0,0 +1,8 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma3-11-4 where
+
+open import Cubical.Foundations.Prelude
+
+lemma : {A : Type} → isProp (isContr A)
+lemma (x , px) (y , py) i = px y i , {!   !}

src/CubicalHott/Prelude.agda

@@ -1,18 +1,18 @@
-{-# OPTIONS --cubical #-}
-module CubicalHott.Prelude where
-
-open import Agda.Primitive using (Level) public
-open import Cubical.Foundations.Equiv public
-open import Cubical.Foundations.Isomorphism public
-open import Cubical.Foundations.Prelude public
-open import Cubical.Foundations.Univalence public
-open import Cubical.Foundations.Function public
-open import Cubical.Relation.Nullary public
-open import Cubical.Data.Equality using (id) public
-
-private
-  variable
-    l : Level
-
-_≢_ : ∀ {A : Type l} → A → A → Type l
+{-# OPTIONS --cubical #-}
+module CubicalHott.Prelude where
+
+open import Agda.Primitive using (Level) public
+open import Cubical.Foundations.Equiv public
+open import Cubical.Foundations.Isomorphism public
+open import Cubical.Foundations.Prelude public
+open import Cubical.Foundations.Univalence public
+open import Cubical.Foundations.Function public
+open import Cubical.Relation.Nullary public
+open import Cubical.Data.Equality using (id) public
+
+private
+  variable
+    l : Level
+
+_≢_ : ∀ {A : Type l} → A → A → Type l
 a ≢ b = ¬ a ≡ b

src/CubicalHott/Theorem2-7-2.agda

@@ -1,55 +1,55 @@
-{-# OPTIONS --cubical #-}
-
-module CubicalHott.Theorem2-7-2 where
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.Equiv
-open import Cubical.Foundations.Isomorphism
-open import Cubical.Data.Sigma
-
-theorem : {A : Type} {P : A → Type} {w w' : Σ A P}
-  → (w ≡ w') ≃ Σ (fst w ≡ fst w') (λ p → PathP (λ i → P (p i)) (snd w) (snd w'))
-theorem {P = P} {w = w} {w' = w'} =
-  isoToEquiv (iso f g fg gf) where
-    f : w ≡ w' → Σ (fst w ≡ fst w') (λ p → PathP (λ i → P (p i)) (snd w) (snd w'))
-    f x = cong fst x , cong snd x
-
-    g : Σ (fst w ≡ fst w') (λ p → PathP (λ i → P (p i)) (snd w) (snd w')) → w ≡ w'
-    g x i = fst x i , snd x i
-
-    fg : section f g
-    fg b = refl
-
-    gf : retract f g
-    gf b = refl
-
-
--- theorem : {A : Type} {P : A → Type} {w w' : Σ A P}
---   → (w ≡ w') ≃ Σ (fst w ≡ fst w') (λ p → subst P p (snd w) ≡ snd w')
--- theorem {P = P} {w = w} {w' = w'} =
---   isoToEquiv (iso f g {!   !} {!   !}) where
---     f : w ≡ w' → Σ (fst w ≡ fst w') (λ p → subst P p (snd w) ≡ snd w')
---     f = J (λ y' p' → Σ (fst w ≡ fst y') (λ q → subst P q (snd w) ≡ snd y'))
---       (refl , transportRefl (snd w))
---       -- subst P (λ _ → fst w) (snd w) ≡ w .snd
---     -- x = (λ i → fst (x i)) , J (λ y' p' → {!   !}) {!   !} x where
---       -- subst P (λ i → fst (x i)) (snd w) ≡ snd w'
---       -- P (fst w')
---       -- ———— Boundary (wanted) —————————————————————————————————————
---       -- i = i0 ⊢ transp (λ i₁ → P (fst (x i₁))) i0 (snd w)
---       -- i = i1 ⊢ snd w'
-
---     g : Σ (fst w ≡ fst w') (λ p → subst P p (snd w) ≡ snd w') → w ≡ w'
---     g x i = fst x i , {!   !}
---     -- helper i where
---       -- helper : PathP (λ i → P (fst x i)) (snd w) (snd w')
---       -- helper i =
---       --   let u = λ j → λ where
---       --     (i = i0) → {!   !}
---       --     (i = i1) → {!   !}
---       --   -- let u = λ j → λ where
---       --   --   (i = i0) → transportRefl (snd w) j
---       --   --   (i = i1) → snd w'
---       --   in hcomp u {! snd x ? !}
-
-    
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem2-7-2 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Data.Sigma
+
+theorem : {A : Type} {P : A → Type} {w w' : Σ A P}
+  → (w ≡ w') ≃ Σ (fst w ≡ fst w') (λ p → PathP (λ i → P (p i)) (snd w) (snd w'))
+theorem {P = P} {w = w} {w' = w'} =
+  isoToEquiv (iso f g fg gf) where
+    f : w ≡ w' → Σ (fst w ≡ fst w') (λ p → PathP (λ i → P (p i)) (snd w) (snd w'))
+    f x = cong fst x , cong snd x
+
+    g : Σ (fst w ≡ fst w') (λ p → PathP (λ i → P (p i)) (snd w) (snd w')) → w ≡ w'
+    g x i = fst x i , snd x i
+
+    fg : section f g
+    fg b = refl
+
+    gf : retract f g
+    gf b = refl
+
+
+-- theorem : {A : Type} {P : A → Type} {w w' : Σ A P}
+--   → (w ≡ w') ≃ Σ (fst w ≡ fst w') (λ p → subst P p (snd w) ≡ snd w')
+-- theorem {P = P} {w = w} {w' = w'} =
+--   isoToEquiv (iso f g {!   !} {!   !}) where
+--     f : w ≡ w' → Σ (fst w ≡ fst w') (λ p → subst P p (snd w) ≡ snd w')
+--     f = J (λ y' p' → Σ (fst w ≡ fst y') (λ q → subst P q (snd w) ≡ snd y'))
+--       (refl , transportRefl (snd w))
+--       -- subst P (λ _ → fst w) (snd w) ≡ w .snd
+--     -- x = (λ i → fst (x i)) , J (λ y' p' → {!   !}) {!   !} x where
+--       -- subst P (λ i → fst (x i)) (snd w) ≡ snd w'
+--       -- P (fst w')
+--       -- ———— Boundary (wanted) —————————————————————————————————————
+--       -- i = i0 ⊢ transp (λ i₁ → P (fst (x i₁))) i0 (snd w)
+--       -- i = i1 ⊢ snd w'
+
+--     g : Σ (fst w ≡ fst w') (λ p → subst P p (snd w) ≡ snd w') → w ≡ w'
+--     g x i = fst x i , {!   !}
+--     -- helper i where
+--       -- helper : PathP (λ i → P (fst x i)) (snd w) (snd w')
+--       -- helper i =
+--       --   let u = λ j → λ where
+--       --     (i = i0) → {!   !}
+--       --     (i = i1) → {!   !}
+--       --   -- let u = λ j → λ where
+--       --   --   (i = i0) → transportRefl (snd w) j
+--       --   --   (i = i1) → snd w'
+--       --   in hcomp u {! snd x ? !}
+
+    

src/CubicalHott/Theorem7-1-10.agda

@@ -0,0 +1,14 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem7-1-10 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Data.Nat
+
+z = isContr
+
+theorem : {X : Type} → (n : ℕ) → isProp (isOfHLevel n X)
+theorem zero x y i = snd x (fst y) i , let z = snd x (fst y) i in λ y' j → {!   !}
+theorem (suc zero) x y = {!   !} 
+theorem (suc (suc n)) x y = {!   !}

src/CubicalHott/Theorem7-1-9.agda

@@ -1,31 +1,31 @@
-{-# OPTIONS --cubical #-}
-
-module CubicalHott.Theorem7-1-9 where
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.HLevels
-open import Cubical.Foundations.Equiv
-open import Cubical.Functions.FunExtEquiv
-open import Data.Nat
-
-theorem : {A : Type} {B : A → Type}
-  → (n : ℕ)
-  → ((a : A) → isOfHLevel n (B a))
-  → isOfHLevel n ((x : A) → B x)
-theorem {A = A} {B = B} zero prf = (λ x → fst (prf x)) , helper where
-  helper : (f' : (x : A) → B x) → (λ x → fst (prf x)) ≡ f'
-  helper f' i x =
-    let given = snd (prf x) in
-    given (f' x) i
-theorem (suc zero) prf f1 f2 i x =
-  let result = prf x (f1 x) (f2 x) in
-  result i
-theorem {A = A} {B = B} (2+ n) prf f1 f2 =
-  subst (isOfHLevel (suc n)) funExtPath (theorem (suc n) λ a → prf a (f1 a) (f2 a))
-  -- goal1 where
-  -- goal1 : isOfHLevel (suc n) (f1 ≡ f2)
-  -- goal2 : isOfHLevel (suc n) ((a : A) → f1 a ≡ f2 a)
-  -- goal1 = subst (λ x → isOfHLevel (suc n) x) funExtPath goal2
-
-  -- IH = theorem {A = A} {B = λ a → f1 a ≡ f2 a} (suc n) λ a → prf a (f1 a) (f2 a)
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem7-1-9 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Equiv
+open import Cubical.Functions.FunExtEquiv
+open import Data.Nat
+
+theorem : {A : Type} {B : A → Type}
+  → (n : ℕ)
+  → ((a : A) → isOfHLevel n (B a))
+  → isOfHLevel n ((x : A) → B x)
+theorem {A = A} {B = B} zero prf = (λ x → fst (prf x)) , helper where
+  helper : (f' : (x : A) → B x) → (λ x → fst (prf x)) ≡ f'
+  helper f' i x =
+    let given = snd (prf x) in
+    given (f' x) i
+theorem (suc zero) prf f1 f2 i x =
+  let result = prf x (f1 x) (f2 x) in
+  result i
+theorem {A = A} {B = B} (2+ n) prf f1 f2 =
+  subst (isOfHLevel (suc n)) funExtPath (theorem (suc n) λ a → prf a (f1 a) (f2 a))
+  -- goal1 where
+  -- goal1 : isOfHLevel (suc n) (f1 ≡ f2)
+  -- goal2 : isOfHLevel (suc n) ((a : A) → f1 a ≡ f2 a)
+  -- goal1 = subst (λ x → isOfHLevel (suc n) x) funExtPath goal2
+
+  -- IH = theorem {A = A} {B = λ a → f1 a ≡ f2 a} (suc n) λ a → prf a (f1 a) (f2 a)
   -- goal2 = IH

src/ThesisWork/Pi3S2/LES.agda

@@ -90,4 +90,10 @@ LES-edge {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) (n ,
 --     -- z : ∥ typ X ∥₂
 --     -- z : ∥ typ X ∥₂
 -- LES-edge f n_ | (n , suc zero) = λ z → {!   !}       
--- LES-edge f n_ | (n , suc (suc zero)) = λ z → {!   !} 
+-- LES-edge f n_ | (n , suc (suc zero)) = λ z → {!   !} 
+
+LES-is-exact : ∀ {l : Level} → {X∙ Y∙ : Pointed l}
+  → (f∙ : X∙ →∙ Y∙)
+  → (n : ℕ × Fin 3)
+  → {!   !}
+LES-is-exact f∙ (n , k) = {!   !} 

src/ThesisWork/Pi3S2/Lemma4-1-5.agda

@@ -89,4 +89,4 @@ lemma {A∙ = A∙ @ (A , a0)} {B∙ = B∙ @ (B , b0)} f∙ @ (f , f-eq) = eqv
           f-eq ∙ (sym f-eq ∙ a) ≡⟨ assoc f-eq (sym f-eq) a ⟩
           (f-eq ∙ sym f-eq) ∙ a ≡⟨ cong (_∙ a) (rCancel f-eq) ⟩
           refl ∙ a ≡⟨ sym (lUnit a) ⟩
-          a ∎
+          a ∎

src/ThesisWork/README.md

@@ -1,3 +1,3 @@
-# Notes
-
-- Already some existing work by Felix Cherubini (@felixwellen) about spectra here: https://github.com/agda/cubical/pull/723
+# Notes
+
+- Already some existing work by Felix Cherubini (@felixwellen) about spectra here: https://github.com/agda/cubical/pull/723

talks/2024-grads/Demo1.agda

@@ -0,0 +1,11 @@
+module 2024-grads.Demo1 where
+
+open import Data.Nat
+open import Data.Nat.Tactic.RingSolver
+open import Relation.Binary.PropositionalEquality as Eq
+
+_ : 1 + 1 ≡ 2
+_ = refl
+
+commutativity : (m n : ℕ) → m + n ≡ n + m
+commutativity = solve-∀

talks/2024-grads/main.tex

@@ -47,6 +47,7 @@
     \note[item]{What: Program properties, compiler optimizations, correctness}
     \note[item]{Notably, can NOT prove some things, Rice's theorem}
 
+    \note[item]{Talk about proofs vs. testing}
     \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 $$}
@@ -78,10 +79,19 @@
   \end{itemize}
 \end{frame}
 
+
+
+\begin{frame}
+  \frametitle{Set theory}
+
+  Talk about set theory
+\end{frame}
+
 \begin{frame}
   \frametitle{Important features of Martin-L{\"o}f type theory}
 
   \begin{itemize}
+    \item Types instead of sets
     \item Predicative universes: $\mathsf{Type}_0, \mathsf{Type}_1, \mathsf{Type}_2, \dots$
     \item Inductive types: for example, $\mathbb{N}$ is defined with 2 possible constructors: $\mathsf{zero}$ and $\mathsf{suc}$.
 

talks/2024-grads/references.bib

@@ -1,16 +1,16 @@
-@Book{hottbook,
-  author =    {The {Univalent Foundations Program}},
-  title =     {Homotopy Type Theory: Univalent Foundations of Mathematics},
-  publisher = {\url{https://homotopytypetheory.org/book}},
-  address =   {Institute for Advanced Study},
-  year =      2013}
-
-@article{
-  Cohen_Coquand_Huber_Mörtberg_2016,
-  title={Cubical Type Theory: a constructive interpretation of the univalence axiom},
-  url={http://arxiv.org/abs/1611.02108},
-  DOI={10.48550/arXiv.1611.02108},
-  abstractNote={This paper presents a type theory in which it is possible to directly manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky’s univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.}, note={arXiv:1611.02108 [cs, math]}, number={arXiv:1611.02108}, publisher={arXiv}, author={Cohen, Cyril and Coquand, Thierry and Huber, Simon and Mörtberg, Anders},
-  year={2016},
-  month=nov
-}
+@Book{hottbook,
+  author =    {The {Univalent Foundations Program}},
+  title =     {Homotopy Type Theory: Univalent Foundations of Mathematics},
+  publisher = {\url{https://homotopytypetheory.org/book}},
+  address =   {Institute for Advanced Study},
+  year =      2013}
+
+@article{
+  Cohen_Coquand_Huber_Mörtberg_2016,
+  title={Cubical Type Theory: a constructive interpretation of the univalence axiom},
+  url={http://arxiv.org/abs/1611.02108},
+  DOI={10.48550/arXiv.1611.02108},
+  abstractNote={This paper presents a type theory in which it is possible to directly manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky’s univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.}, note={arXiv:1611.02108 [cs, math]}, number={arXiv:1611.02108}, publisher={arXiv}, author={Cohen, Cyril and Coquand, Thierry and Huber, Simon and Mörtberg, Anders},
+  year={2016},
+  month=nov
+}