wip

.ignore

@@ -1,2 +1,4 @@
 .git
 .DS_Store
+resources/
+src/HoTTEST/

notes/HLevels.md

@@ -0,0 +1,27 @@
+# Properties
+
+- Theorem 7.1.4:
+  - IF: $X$ is an $n$ type
+  - IF: $X \rightarrow Y$ is a retraction (has a left-inverse)
+  - THEN: $Y$ is an $n$ type
+- Corollary 7.1.5:
+  - IF: $X \simeq Y$
+  - IF: $X$ is an $n$ type
+  - THEN: $Y$ is an $n$ type
+- Theorem 7.1.7:
+  - IF: $X$ is an $n$ type
+  - THEN: it is also an $(n + 1)$ type
+- Theorem 7.1.8:
+  - IF: $A$ is an $n$ type
+  - IF: $B(a)$ is an $n$ type for all $a : A$
+  - THEN: $\sum_{(x : A)} B(x)$ is an $n$ type
+
+## -2: Contractible
+
+## -1: Mere props
+
+- If $A$ and $B$ are mere props, so is $A \times B$
+
+- If $B(a)$ is a prop for any $a:A$, then $\prod_{(x:A)} B(x)$ is a prop
+
+-

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/Corollary7-1-5.agda

@@ -10,7 +10,7 @@ open import Cubical.Data.Nat
 
 open import CubicalHott.Theorem7-1-4 renaming (theorem to theorem7-1-4)
 
-corollary : {X Y : Type} → (n : ℕ)
+corollary : {l : Level} → {X Y : Type l} → (n : ℕ)
   → X ≃ Y → isOfHLevel n X → isOfHLevel n Y
 corollary n eqv prf =
   theorem7-1-4 (fst eqv) (invIsEq (snd eqv))

src/CubicalHott/Corollary7-2-3.agda

@@ -0,0 +1,14 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Corollary7-2-3 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Relation.Nullary
+
+open import CubicalHott.Lemma7-2-4 renaming (lemma to lemma7-2-4)
+
+corollary : {X : Type}
+  → ((x y : X) → ¬ ¬ (x ≡ y) → x ≡ y)
+  → isSet X
+corollary {X} prf x y p q = {!   !} where
+  wtf = let z = prf x y (λ r → r p) in {!   !}

src/CubicalHott/Example3-6-2.agda

@@ -0,0 +1,10 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Example3-6-2 where
+
+open import Cubical.Foundations.Prelude
+
+example : {l l2 : Level} → {A : Type l} → {B : A → Type l2}
+  → ((x : A) → isProp (B x))
+  → isProp ((x : A) → B x)
+example B-x-prop fx fy = λ i z → B-x-prop z (B-x-prop z (fx z) (fy z) i) (B-x-prop z (fx z) (fy z) i) i

src/CubicalHott/Exercise3-5.agda

@@ -0,0 +1,23 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Exercise3-5 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+
+exercise : {A : Type} → isProp A ≃ (A → isContr A)
+exercise {A} = isoToEquiv (iso f g fg gf) where
+  f : isProp A → A → isContr A
+  f isPropA a = a , (λ y → isPropA a y)
+
+  g : (A → isContr A) → isProp A
+  g p x y =
+    let z = snd (p x) in
+    sym (z x) ∙ z y
+
+  fg : section f g
+  fg ff = funExt λ x → isPropIsContr (f (g ff) x) (ff x)
+
+  gf : retract f g
+  gf prop = funExt (λ x → funExt (λ y → isProp→isSet prop x y (g (f prop) x y) (prop x y)))

src/CubicalHott/HLevels.agda

@@ -0,0 +1,46 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.HLevels where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
+open import Data.Nat
+
+isOfHLevel' : ∀ {ℓ : Level} → ℕ → Type ℓ → Type ℓ
+isOfHLevel' 0 A = isContr A
+isOfHLevel' (suc n) A = (x y : A) → isOfHLevel' n (x ≡ y)
+
+TypeOfHLevel' : ∀ ℓ → HLevel → Type (ℓ-suc ℓ)
+TypeOfHLevel' ℓ n = TypeWithStr ℓ (isOfHLevel' n)
+
+1Prop : {l : Level} → (T : Type l) → isOfHLevel' 1 T → isProp T
+1Prop T T1 x y = let z = T1 x y in fst z
+
+Prop1 : {l : Level} → (T : Type l) → isProp T → isOfHLevel' 1 T
+Prop1 T Tp x y = (Tp x y) , λ q → isProp→isSet Tp x y (Tp x y) q
+
+isOfHLevel→isOfHLevel' : ∀ {l : Level} → (n : ℕ) → (A : Type l)
+  → isOfHLevel n A → isOfHLevel' n A
+isOfHLevel→isOfHLevel' zero A z = z
+isOfHLevel→isOfHLevel' (suc zero) A z =
+  λ x y → (z x y) , λ q → isProp→isSet z x y (z x y) q
+isOfHLevel→isOfHLevel' (suc (suc n)) A z =
+  λ x y p q → isOfHLevel→isOfHLevel' (suc n) (x ≡ y) (z x y) p q
+
+isOfHLevel'→isOfHLevel : ∀ {l : Level} → (n : ℕ) → (A : Type l)
+  → isOfHLevel' n A → isOfHLevel n A
+isOfHLevel'→isOfHLevel zero A z = z 
+isOfHLevel'→isOfHLevel (suc zero) A z =
+  λ x y → let z1 = z x y in fst z1 
+isOfHLevel'→isOfHLevel (suc (suc n)) A z =
+  λ x y →
+    let IHf = λ p q → z x y p q in
+    let IH = isOfHLevel'→isOfHLevel (suc n) (x ≡ y) IHf in
+    IH
+
+TypeOfHLevel→TypeOfHLevel' : ∀ (l : Level) → (n : ℕ) → TypeOfHLevel l n → TypeOfHLevel' l n
+TypeOfHLevel→TypeOfHLevel' l n (T , T-n-type) = T , isOfHLevel→isOfHLevel' n T T-n-type
+
+TypeOfHLevel'→TypeOfHLevel : ∀ (l : Level) → (n : ℕ) → TypeOfHLevel' l n → TypeOfHLevel l n
+TypeOfHLevel'→TypeOfHLevel l n (T , T-n-type) = T , isOfHLevel'→isOfHLevel n T T-n-type

src/CubicalHott/Lemma2-4-3.agda

@@ -6,7 +6,7 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Homotopy.Base
 
 postulate
-  lemma : {A B : Type} → (f g : A → B) → (H : f ∼ g) → {x y : A} → (p : x ≡ y)
+  lemma : {l : Level} → {A B : Type l} → (f g : A → B) → (H : f ∼ g) → {x y : A} → (p : x ≡ y)
     → H x ∙ cong g p ≡ cong f p ∙ H y
 -- lemma f g H {x} {y} p i j =
 --   -- B

src/CubicalHott/Lemma3-11-3.agda

@@ -0,0 +1,5 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma3-11-3 where
+
+open import Cubical.Foundations.Prelude

src/CubicalHott/Lemma3-11-4.agda

@@ -0,0 +1,35 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma3-11-4 where
+
+open import Cubical.Foundations.Prelude
+open import CubicalHott.Example3-6-2 renaming (example to example3-6-2)
+
+lemma : {l : Level} → {A : Type l} → isProp (isContr A)
+lemma {A = A} A-contr-x @ (x , px) (y , py) i =
+  px y i , goal i where
+    A-is-set = isProp→isSet (isContr→isProp A-contr-x)
+
+    helper2 : px y i ≡ y
+    helper2 = sym (py (px y i))
+
+    helper1 : isProp ((z : A) → px y i ≡ z)
+    helper1 = example3-6-2 (λ z → isContr→isProp (helper2 ∙ py z , λ q → A-is-set (px y i) z (helper2 ∙ py z) q))
+
+    wtf : (z : A) → sym (px z) ∙∙ px y ∙∙ py z ≡ refl {x = z}
+    wtf z = A-is-set z z (sym (px z) ∙∙ px y ∙∙ py z) refl
+
+    helper3 : (z : A) → PathP (λ i → px z i ≡ py z i) (px y) (sym (px z) ∙∙ px y ∙∙ py z)
+    helper3 z = doubleCompPath-filler (sym (px z)) (px y) (py z)
+
+    helper5 : (z : A) → PathP (λ i → px z i ≡ py z i) (px y) (refl {x = z})
+    helper5 z = helper3 z ▷ wtf z
+
+    goal2 : (z : A) → PathP (λ i → px y i ≡ z) (px z) (py z)
+    goal2 z i j = helper5 z j i
+
+    goal : PathP (λ i → (z : A) → px y i ≡ z) px py
+    goal i z j = funExt (λ z → goal2 z i) j z
+
+
+  -- λ y' j → isProp→isSet (isContr→isProp A-contr-x) (px y i) y' {!   !} {!   !} j i  

src/CubicalHott/Lemma3-5-1.agda

@@ -0,0 +1,48 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma3-5-1 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Data.Sigma
+
+lemma : {l l2 : Level} → {A : Type l} → {P : A → Type l2}
+  → ((x : A) → isProp (P x))
+  → (u v : Σ A P)
+  → (fst u ≡ fst v)
+  → u ≡ v
+lemma {P = P} Px-isProp u v p i = p i , goal i where
+  goal : PathP (λ i → P (p i)) (snd u) (snd v)
+  goal = toPathP (Px-isProp (fst v) (subst P p (snd u)) (snd v))
+  
+corollary : {l : Level} → {A B : Type l}
+  → (f g : A ≃ B)
+  → fst f ≡ fst g
+  → f ≡ g
+corollary f g p = lemma isPropIsEquiv f g p
+
+-- corollary-equiv : {l : Level} → {A B : Type l}
+--   → (f g : A ≃ B)
+--   → (fst f ≡ fst g) ≃ (f ≡ g)
+-- corollary-equiv f g = isoToEquiv (iso (corollary f g) (cong fst) fg gf) where
+--   helper : (f≡g : f ≡ g) → subst (λ x → isEquiv (fst x)) f≡g (snd f) ≡ snd g
+--   helper f≡g = isPropIsEquiv (fst g) (subst (λ x → isEquiv (fst x)) f≡g (snd f)) (snd g)
+
+--   helper2 : (f≡g : f ≡ g) → PathP (λ i → isEquiv (fst (f≡g i))) (snd f) (snd g)
+--   helper2 f≡g = toPathP (helper f≡g)
+
+--   fg : section (corollary f g) (cong fst)
+--   -- Trying to prove that producing full f ≡ g after discarding the second half still produces the original
+--   -- However, no matter what the original is, the isEquiv part is a mere prop
+--   fg f≡g i j = fst (f≡g j) , {!   !} where
+--     -- isEquiv (fst (f≡g j))
+--     -- ———— Boundary (wanted) —————————————————————————————————————
+--     -- j = i0 ⊢ f .snd
+--     -- j = i1 ⊢ g .snd
+--     -- i = i0 ⊢ CubicalHott.Lemma3-5-1.goal isPropIsEquiv f g
+--     --          (cong (λ r → fst r) f≡g) j j
+--     -- i = i1 ⊢ f≡g j .snd
+
+--   gf : retract (corollary f g) (cong fst)
+--   gf x = refl

src/CubicalHott/Lemma6-10-2.agda

@@ -3,6 +3,7 @@
 module CubicalHott.Lemma6-10-2 where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
 open import Cubical.Functions.Surjection
 open import Cubical.HITs.SetQuotients
 open import Cubical.HITs.PropositionalTruncation
@@ -14,4 +15,9 @@ private
 lemma : (A : Type l) (R : A → A → Type l)
   → (q : A → A / R)
   → isSurjection q
-lemma {l} A R q x = {!   !}
+lemma {l} A R q x = elimProp f1 f2 x where
+  f1 : (z : A / R) → isProp ∥ fiber q x ∥₁
+  f1 z x y = {!   !}
+
+  f2 : (a : A) → ∥ fiber q x ∥₁
+  f2 a = ∣ (a , {!   !}) ∣₁

src/CubicalHott/Lemma7-2-4.agda

@@ -0,0 +1,13 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma7-2-4 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Relation.Nullary
+open import Cubical.Data.Sigma
+open import Cubical.Data.Empty
+open import Data.Sum
+
+lemma : (A : Type) → (A ⊎ ¬ A) → (¬ ¬ A → A)
+lemma A (inj₁ x) p = x 
+lemma A (inj₂ y) p = elim (p y) 

src/CubicalHott/Lemma7-2-8.agda

@@ -0,0 +1,13 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma7-2-8 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Data.Nat
+
+lemma : {n : ℕ} → {X : Type}
+  → ((x : X) → isOfHLevel (suc n) X)
+  → isOfHLevel (suc n) X
+lemma {zero} {X} f x y = f x x y 
+lemma {suc n} {X} f x y = f x x y

src/CubicalHott/Lemma7-3-1.agda

@@ -0,0 +1,16 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma7-3-1 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Data.Unit
+open import Cubical.HITs.Truncation
+open import Cubical.Data.Nat
+
+lemma : {A : Type} → (n : ℕ) → isOfHLevel n (∥ A ∥ n)
+lemma {A} zero = tt* , helper where
+  helper : (y : ∥ A ∥ zero) → tt* ≡ y
+  helper tt* = refl
+lemma {A} (suc zero) x y = {!   !}
+lemma {A} (suc (suc n)) = {!   !}

src/CubicalHott/Lemma8-3-1.agda

@@ -14,12 +14,13 @@ open import Cubical.Homotopy.Loopspace
 open import Cubical.HITs.SetTruncation
 
 
-helper : ∀ {l : Level} → (n : ℕ) → (A∙ @ (A , a) : Pointed l)
+helper : ∀ {l : Level} → (n : ℕ)
+  → (A∙ @ (A , a) : Pointed l)
   → isOfHLevel (suc n) A → isOfHLevel n (typ (Ω A∙))
-helper zero A∙@(A , a) prf = refl , (λ y j i → {!   !})
+helper zero A∙@(A , a) prf = refl , {!   !}
 helper (suc zero) A∙@(A , a) prf = {!   !}
 helper (suc (suc n)) A∙@(A , a) prf = {!   !}
 
--- lemma : ∀ {l} → (A∙ @ (A , a) : Pointed l)
---   → (n : ℕ) → hLevelTrunc n A → (k : ℕ) → π (k + n) (A , a) ≡ Lift Unit
--- lemma A∙ @ (A , a) n x k i = {!   !} where  
+lemma : ∀ {l} → (A∙ @ (A , a) : Pointed l)
+  → (n : ℕ) → hLevelTrunc n A → (k : ℕ) → π (k + n) (A , a) ≡ Lift Unit
+lemma A∙ @ (A , a) n x k = {!   !} 

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 : {l l2 : Level} → {A : Type l} → {P : A → Type l2} → {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/Theorem3-2-2.agda

@@ -0,0 +1,24 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem3-2-2 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Relation.Nullary
+open import Cubical.Data.Nat
+open import Cubical.Data.Bool
+
+-- Trying to give a cubical interpretation of this
+
+theorem : ¬ ((A : Type) → (¬ (¬ A) → A))
+theorem f = {!   !} where
+  apdfp : PathP (λ i → ¬ ¬ notEq i → notEq i) (f Bool) (f Bool)
+  apdfp = congP (λ i A → {! ¬ ¬ A → A  !}) notEq
+
+  u : ¬ ¬ Bool
+  u = λ p → p true
+
+  -- foranyu : PathP (λ i → {!   !}) (fbool u) (fbool u)
+  -- foranyu i = {!  apdfp i u !}
+  

src/CubicalHott/Theorem7-1-10.agda

@@ -0,0 +1,16 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem7-1-10 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Data.Nat
+
+open import CubicalHott.Lemma3-11-4 renaming (lemma to lemma3-11-4)
+
+theorem : {l : Level} → {X : Type l} → (n : ℕ) → isProp (isOfHLevel n X)
+theorem zero = lemma3-11-4
+theorem (suc zero) isProp1 isProp2 i x y j = isProp→isSet isProp1 x y (isProp1 x y) (isProp2 x y) i j
+theorem {X = X} (suc (suc n)) isHLevel1 isHLevel2 =
+  let IH = λ (x y : X) → theorem {X = x ≡ y} (suc n) in
+  funExt (λ x → funExt (λ y → IH x y (isHLevel1 x y) (isHLevel2 x y)))

src/CubicalHott/Theorem7-1-11.agda

@@ -2,73 +2,201 @@
 
 module CubicalHott.Theorem7-1-11 where
 
+open import Agda.Primitive using (lzero ; lsuc)
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 open import Cubical.Core.Glue
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Isomorphism
+open import Cubical.Data.Sigma
+open import Cubical.Functions.Embedding
 open import Cubical.Foundations.Univalence
 open import Cubical.Data.Nat
 open import Data.Unit
 
+open import CubicalHott.Lemma3-5-1 renaming (lemma to lemma3-5-1; corollary to corollary3-5-1)
+open import CubicalHott.Theorem7-1-6 renaming (theorem to theorem7-1-6)
+open import CubicalHott.Theorem7-1-8 renaming (theorem to theorem7-1-8)
+open import CubicalHott.Theorem7-1-10 renaming (theorem to theorem7-1-10)
+open import CubicalHott.HLevels
+
+helper : ∀ {l : Level} → (n : HLevel) → isOfHLevel' {ℓ = lsuc l} (suc n) (TypeOfHLevel l n)
+helper {l = l} zero = goal1 where
+  eqv : (x y : TypeOfHLevel l zero) → fst x ≡ fst y
+  eqv x y = ua (isoToEquiv (iso (λ _ → fst (snd y)) (λ _ → fst (snd x)) (snd (snd y)) (snd (snd x))))
+
+  goal2 : isProp (TypeOfHLevel l zero)
+  goal2 x y = lemma3-5-1 (λ _ → theorem7-1-10 zero) x y (eqv x y)
+
+  goal1 : (x y : TypeOfHLevel l zero) → isContr (x ≡ y)
+  goal1 = Prop1 (TypeOfHLevel l zero) goal2
+
+  -- A≡B i , goal i where
+  --   -- isContr (A≡B i)
+  --   -- Acontr ≡ Bcontr
+
+  --   -- A≡B i , a≡b i , λ y j → wtf i y j where
+  --   eqv1 : A ≃ B
+  --   eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr)
+
+  --   A≡B : A ≡ B
+  --   A≡B = ua eqv1
+
+  --   a≡b : PathP (λ i → A≡B i) a b
+  --   a≡b j = glue (λ { (j = i0) → a ; (j = i1) → b }) b
+
+  --   helper3 : (x : B) → isProp ((y : B) → x ≡ y)
+  --   helper3 x f1 f2 =
+  --     let helper = isProp→isSet (isContr→isProp (b , Bcontr)) in
+  --     funExt (λ (y : B) → helper x y (f1 y) (f2 y))
+
+  --   helper2 : subst isContr A≡B (a , Acontr) ≡ (b , Bcontr)
+  --   helper2 = lemma3-5-1 helper3 (subst isContr A≡B (a , Acontr)) (b , Bcontr) (fromPathP a≡b)
+
+  --   goal : PathP (λ i → isContr (A≡B i)) (a , Acontr) (b , Bcontr)
+  --   goal = toPathP helper2
+
+helper {l = l} (suc n) (X , px) (Y , py) p q = isOfHLevel→isOfHLevel' n (p ≡ q) goal4 where
+  goal1 : {n : ℕ} → ((X , px) : TypeOfHLevel l n) → ((Y , py) : TypeOfHLevel l n)
+    → ((X , px) ≡ (Y , py)) ≃ (X ≃ Y)
+  goal1 {n = n} (X , px) (Y , py) =
+    (X , px) ≡ (Y , py) ≃⟨ isoToEquiv (iso f g (λ _ → refl) gf) ⟩
+    X ≡ Y ≃⟨ univalence ⟩
+    X ≃ Y ■ where
+      f : (X , px) ≡ (Y , py) → X ≡ Y
+      f = cong fst
+
+      g : X ≡ Y → (X , px) ≡ (Y , py)
+      g p = lemma3-5-1 (λ x → theorem7-1-10 n) (X , px) (Y , py) p
+
+      ,snd, : (p : (X , px) ≡ (Y , py)) → PathP {ℓ = l} (λ i → isOfHLevel n (cong fst p i)) px py
+      ,snd, p = J (λ y' p' → PathP (λ i → isOfHLevel n (cong fst p' i)) px (snd y')) refl p
+
+      gf : retract f g
+      gf p i j = {! goal i j  !} where
+        goal : SquareP (λ i j → isOfHLevel {ℓ = lsuc l} n (cong {!   !} p i)) refl refl {! g (f p)   !} λ i → {!  snd (p i) !}
+
+        prop-helper : isProp (isOfHLevel n Y)
+        prop-helper = theorem7-1-10 n
+
+        thm : transport {ℓ = l} (λ i → isOfHLevel {ℓ = l} n (fst (p i))) px ≡ py
+        thm = prop-helper (transport (λ i → isOfHLevel n (fst (p i))) px) py
+  
+  goal2 : isEmbedding {A = X ≃ Y} {B = X → Y} fst
+  goal2 x≃y1 x≃y2 = isoToIsEquiv (iso (cong fst) g (λ _ → refl) gf) where
+    g : fst x≃y1 ≡ fst x≃y2 → x≃y1 ≡ x≃y2
+    g = lemma3-5-1 isPropIsEquiv x≃y1 x≃y2
+
+    gf : retract (cong fst) g
+    gf p i j = fst (p j) , {!   !}
+      -- Goal here is to use toPathP, convert them both
+
+      -- isEquiv (fst (p j))
+      -- ———— Boundary (wanted) —————————————————————————————————————
+      -- j = i0 ⊢ x≃y1 .snd
+      -- j = i1 ⊢ x≃y2 .snd
+      -- i = i0 ⊢ CubicalHott.Lemma3-5-1.goal isPropIsEquiv x≃y1 x≃y2
+      --          (cong (λ r → fst r) p) j j
+      -- i = i1 ⊢ p j .snd
+
+    -- toPathP {A = {!   !}} z j where
+      -- z : transport (λ i → isEquiv (fst (p i))) (snd x≃y1) ≡ snd x≃y2
+      -- z = isPropIsEquiv (fst x≃y2) (subst (λ x → isEquiv (fst x)) p (snd x≃y1)) (snd x≃y2)
+
+  goal3 : isOfHLevel n (X → Y)
+  goal3 = theorem7-1-6 {!   !} goal2 {! suc n  !} {!   !} {!   !}
+
+  goal4 : isOfHLevel n (p ≡ q)
+  goal4 =
+    let IH = helper n in
+    isOfHLevel'→isOfHLevel n {!   !} {! IH p q  !}
+
+
 lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n)
-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)
+lemma {l = l} n = isOfHLevel'→isOfHLevel (suc n) (TypeOfHLevel l n) (helper n)
 
-  A≡B : A ≡ B
-  A≡B = ua eqv1
+--     -- -- eqv2 : ((y : A) → a ≡ y) ≡ ((y : B) → b ≡ y)
+--     -- -- eqv2 = λ i → (y : A≡B i) → a≡b i ≡ y
 
-  a≡b : PathP (λ i → A≡B i) a b
-  a≡b j = glue (λ { (j = i0) → a ; (j = i1) → b }) b
+--     -- -- T1 = λ { (i = i0) → ((y : A) → a ≡ y) ; (i = i1) → ((y : B) → b ≡ y) }
+--     -- -- e1 = λ { (i = i0) → pathToEquiv eqv2 ; (i = i1) → idEquiv ((y : B) → b ≡ y) }
+--     -- -- Uhh = primGlue ((y : B) → b ≡ y) T1 e1
+        
+--     -- -- uhh : Uhh
+--     -- -- uhh = glue {T = T1} {e = e1} (λ { (i = i0) → Acontr ; (i = i1) → Bcontr }) λ y j → {! Bcontr y j  !}
 
-  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₁
+--     -- Acontr-is-Prop : isProp ((y : A) → a ≡ y)
 
-  -- 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 {!   !}
+--     -- wtf : PathP (λ i → (y : A≡B i) → a≡b i ≡ y) Acontr Bcontr
+--     -- wtf = λ i y j → {!   !}
 
 
-lemma (suc zero) (A , A-prop) (B , B-prop) x y i j = {!   !} where
+--     --   -- a≡b i ≡ y
+--     --   -- ———— Boundary (wanted) —————————————————————————————————————
+--     --   -- i = i0 ⊢ λ i₁ → Acontr y i₁
+--     --   -- i = i1 ⊢ λ i₁ → Bcontr y i₁
 
-lemma (suc (suc n)) x y = {!   !}
+--     -- 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 {!   !}
 
--- lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n)
--- lemma zero (A , a , Acontr) (B , b , Bcontr) i = G , g , contr where
+lemma {l = l} (suc zero) (A , A-prop) (B , B-prop) p q i j = {!   !} , {!   !} where
+  z1 = let z = lemma {l = l} zero in {!   !}
+  -- overall goal is p ≡ q
+  -- p : (A , A-prop) ≡ (B , B-prop) where both are type Σ Type isProp
+  -- q : (A , A-prop) ≡ (B , B-prop)
 
---   eqv1 : A ≃ B
---   eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr)
+  -- cong_fst(p) : A ≡ B
 
---   T = λ { (i = i0) → A ; (i = i1) → B }
---   e = λ { (i = i0) → eqv1 ; (i = i1) → idEquiv B }
+--   -- we know that A ≡ B in two different ways
+--   -- if A is a prop, then (x y : A) → x ≡ y
+--   -- if A is empty, then B is also empty
+--   -- but we can't choose a contractible center (no AOC)
+  
+--   -- "for any two proofs that A ≡ B and that A-prop ≡ B-prop"
+--   -- p : (A , A-prop) ≡ (B , B-prop)
+--   -- p = λ i → <something s.t at i=0, returns A , A-prop>
+--   -- so (p i0) : Σ Type isProp = (A , A-prop)
+--   -- p ≡_{Σ Type isProp} q
+--   -- through lemma 3.5.1, if the isProp is a prop for every type, then we only have to compare the Type
+--   -- 
+--   {!   !}
 
---   G = primGlue B T e
---   g = glue {T = T} {e = e} (λ { (i = i0) → a ; (i = i1) → b }) b
+-- lemma (suc (suc n)) x y p q =
+--   let IH = lemma (suc n) in
+--   {!   !}
 
---   -- at i = i0, y = a
---   -- at i = i1, y = b
+-- -- lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n)
+-- -- lemma zero (A , a , Acontr) (B , b , Bcontr) i = G , g , contr where
 
---   -- 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  !})
+-- --   eqv1 : A ≃ B
+-- --   eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr)
 
---     -- unglue i {!   !}
---     -- (glue (λ { (i = i1) → {!   !} }) {!   !})
---     -- (glue (λ { (i = i0) → a ; (i = i1) → b }) b))
--- lemma (suc n) x y = {!   !}
+-- --   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 = {!   !}
  

src/CubicalHott/Theorem7-1-4.agda

@@ -12,21 +12,21 @@ open import Cubical.Data.Nat
 
 open import CubicalHott.Lemma2-4-3 renaming (lemma to lemma2-4-3)
 
-theorem : {X Y : Type}
+theorem : {l : Level} → {X Y : Type l}
   → (p : X → Y)
   → (s : Y → X)
   → retract s p
   → (n : ℕ)
   → isOfHLevel n X
   → isOfHLevel n Y
-theorem {X} {Y} p s r zero (x0 , xContr) = p x0 , λ y → cong p (xContr (s y)) ∙ r y
-theorem {X} {Y} p s r (suc zero) xHlevel a b =
+theorem {X = X} {Y = Y} p s r zero (x0 , xContr) = p x0 , λ y → cong p (xContr (s y)) ∙ r y
+theorem {X = X} {Y = Y} p s r (suc zero) xHlevel a b =
   let
     step1 = xHlevel (s a) (s b)
     step2 = cong p step1
     step3 = (sym (r a)) ∙ step2 ∙ r b
   in step3
-theorem {X} {Y} p s r (suc (suc n)) xHlevel a b =
+theorem {X = X} {Y = Y} p s r (suc (suc n)) xHlevel a b =
   theorem (λ q → sym (r a) ∙ cong p q ∙ r b) (cong s) f (suc n) (xHlevel (s a) (s b)) where
     f : retract (cong s) (λ q → sym (r a) ∙ cong p q ∙ r b)
     f q =  cong (sym (r a) ∙_) helper ∙ assoc (sym (r a)) (r a) q ∙ cong (_∙ q) (lCancel (r a)) ∙ sym (lUnit q) where

src/CubicalHott/Theorem7-1-6.agda

@@ -9,7 +9,7 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Functions.Embedding
 open import Data.Nat
 
-theorem : {X Y : Type}
+theorem : {l : Level} → {X Y : Type l}
   → (f : X → Y) → isEmbedding f
   → (n : HLevel)
   → isOfHLevel (suc n) Y → isOfHLevel (suc n) X

src/CubicalHott/Theorem7-1-7.agda

@@ -6,17 +6,17 @@ open import Data.Nat
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 
-theorem : {X : Type} {n : ℕ}
+theorem : {l : Level} → {X : Type l} → {n : ℕ}
   → isOfHLevel n X → isOfHLevel (suc n) X
-theorem {X} {zero} X-n-type x y = sym (snd X-n-type x) ∙ snd X-n-type y
-theorem {X} {suc zero} X-n-type x y p q j i =
+theorem {X = X} {n = zero} X-n-type x y = sym (snd X-n-type x) ∙ snd X-n-type y
+theorem {X = X} {n = suc zero} X-n-type x y p q j i =
   let u = λ k → λ where
     (i = i0) → X-n-type x x k
     (i = i1) → X-n-type x y k
     (j = i0) → X-n-type x (p i) k
     (j = i1) → X-n-type x (q i) k
   in hcomp u x 
-theorem {X} {2+ n} X-n-type = λ x y p q →
+theorem {X = X} {n = 2+ n} X-n-type = λ x y p q →
   let known = X-n-type x y in
   let IH = theorem {X = x ≡ y} {n = suc n} known p q in
   IH

src/CubicalHott/Theorem7-1-8.agda

@@ -12,11 +12,11 @@ open import Data.Nat
 open import CubicalHott.Theorem2-7-2 renaming (theorem to theorem2-7-2)
 open import CubicalHott.Corollary7-1-5 renaming (corollary to corollary7-1-5)
 
-theorem : {A : Type} {B : A → Type} {n : ℕ}
+theorem : {l l2 : Level} → {A : Type l} → {B : A → Type l2} → {n : ℕ}
   → isOfHLevel n A
   → ((a : A) → isOfHLevel n (B a))
   → isOfHLevel n (Σ A B)
-theorem {A} {B} {zero} A-n-type @ (a , a-contr) B-n-type =
+theorem {A = A} {B} {zero} A-n-type @ (a , a-contr) B-n-type =
   let b = fst (B-n-type a) in
   let b-contr = snd (B-n-type a) in
   (a , b) , λ y i → a-contr (fst y) i , 
@@ -25,11 +25,11 @@ theorem {A} {B} {zero} A-n-type @ (a , a-contr) B-n-type =
     -- using path induction, both of them are a
     let helper = J (λ a' p' → (b' : B a') → PathP (λ i → B (p' i)) b b') (λ b' j → b-contr b' j ) (a-contr (fst y)) (snd y) in
     helper i
-theorem {A} {B} {suc zero} A-n-type B-n-type x @ (xa , xb) y @ (ya , yb) =
+theorem {A = A} {B} {suc zero} A-n-type B-n-type x @ (xa , xb) y @ (ya , yb) =
   λ i → A-n-type xa ya i ,
     let helper = J (λ a' p' → (ba' : B a') → PathP (λ i' → B (p' i')) xb ba') (λ ba' i' → B-n-type xa xb ba' i') (A-n-type xa ya) yb in
     helper i 
-theorem {A} {B} {2+ n} A-n-type B-n-type x @ (xa , xb) y @ (ya , yb) =
+theorem {A = A} {B} {2+ n} A-n-type B-n-type x @ (xa , xb) y @ (ya , yb) =
   let eqv = theorem2-7-2 {w = x} {w' = y} in
   let eqv2 = (fst invEquivEquiv) eqv in
   let

src/CubicalHott/Theorem7-1-9.agda

@@ -1,31 +1,32 @@
-{-# 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 : {l l2 : Level} → {A : Type l} {B : A → Type l2}
+  → (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/CubicalHott/Theorem7-2-2.agda

@@ -2,13 +2,19 @@
 
 module CubicalHott.Theorem7-2-2 where
 
+open import Agda.Primitive hiding (Prop)
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
 open import Cubical.Data.Sigma
 
-theorem : {X : Type}
-  → (R : X → X → Type)
-  → ((x : X) → R x x → x ≡ x)
-  → ((x y : X) → (R x y) → x ≡ y)
+Prop : (l : Level) → Type (lsuc l)
+Prop l = TypeWithStr l isProp
+
+theorem : {l l2 : Level} → {X : Type l}
+  → (R : X → X → Prop l2)
+  → ((x : X) → {! R x x !} → {!   !})
+  → ((x y : X) → {! R x y  !} → x ≡ y)
   → isSet X
-theorem R r f x y p q = {!   !}
+theorem R f1 f2 x y p q = {!   !}

src/CubicalHott/Theorem7-2-7.agda

@@ -0,0 +1,17 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem7-2-7 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
+open import Cubical.Homotopy.Loopspace
+open import Data.Nat
+
+open import CubicalHott.Lemma7-2-8 renaming (lemma to lemma7-2-8)
+
+theorem : {n : ℕ} → {X : Type}
+  → ((x : X) → isOfHLevel (suc n) (typ (Ω (X , x))))
+  → isOfHLevel (suc (suc n)) X
+theorem {n} {X} f x y =
+  lemma7-2-8 λ p → J (λ y' p' → isOfHLevel (suc n) (x ≡ y')) (f x) p

src/CubicalHott/Theorem7-2-9.agda

@@ -0,0 +1,20 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem7-2-9 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Structure
+open import Cubical.Homotopy.Loopspace
+open import Cubical.Data.Nat
+
+open import CubicalHott.Exercise3-5 renaming (exercise to exercise3-5)
+open import CubicalHott.Theorem7-2-1 renaming (forwards to theorem7-2-1)
+
+theorem : {n : ℕ} → {A : Type}
+  → ((a : A) → isContr (typ ((Ω^ suc (suc n)) (A , a))))
+  → isOfHLevel (suc n) A
+theorem {zero} f = invEq exercise3-5 λ x → x , λ y → {!   !}
+theorem {suc zero} f = theorem7-2-1 (λ x p → let z = snd (f x) in {!   !}) 
+theorem {suc (suc n)} f x y = {!   !} 

src/Misc/FiveLemma/Category/Exact.agda

@@ -0,0 +1,105 @@
+{-# OPTIONS --cubical #-}
+
+module Misc.FiveLemma.Category.Exact where
+
+open import Agda.Primitive
+open import Cubical.Categories.Abelian
+open import Cubical.Categories.Additive
+open import Cubical.Categories.Category
+open import Cubical.Categories.Morphism
+open import Cubical.Data.Sigma
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Functions.Embedding
+open import Cubical.Functions.Surjection
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module _ (AC : AbelianCategory ℓ ℓ') where
+  open AbelianCategory AC
+
+  -- image is defined as kernel (cokernel f)
+  image : {x y : ob} (f : Hom[ x , y ]) → Σ ob (λ i → Hom[ i , y ])
+  image f = hasKernels (coker f) .Kernel.k , (ker (coker f))
+
+  isExact : {x y z : ob} (f : Hom[ x , y ]) (g : Hom[ y , z ]) → Type ℓ'
+  isExact {y = y} f g = Σ (Hom[ (Kernel.k g-ker) , (fst f-im) ]) λ m → isIso cat m where
+    f-im = image f
+    g-ker = hasKernels g
+
+  module _ where
+    open import Data.Fin
+    open import Data.Nat
+    open import Data.Vec
+
+    finExactSequence : {n : ℕ}
+      → (obSeq : Fin (suc (suc n)) → ob)
+      → (homSeq : (m : Fin (suc n)) → Hom[ (obSeq (inject₁ m)) , (obSeq (suc m)) ])
+      → Type ℓ'
+    finExactSequence {n = n} obSeq homSeq =
+      (m : Fin n) → isExact (homSeq (inject₁ m)) (homSeq (suc m))
+
+    pattern 3+ n = suc (suc (suc n))
+
+    -- Ob sequences must have at least 2 elements
+    obSeq : (n : ℕ) → Type ℓ
+    obSeq n = Vec ob (2+ n)
+
+    private
+      z = ℕ.zero
+
+      zFin2 : Fin 2
+      zFin2 = inject₁ Fin.zero
+
+    -- I am using Vec in the reverse way!!!
+
+    -- Fin 5   0    1    2    3    4
+    -- obSeq = E :: D :: C :: B :: A :: []
+
+    -- Fin 4    3     2     1      0
+    -- homSeq = de :: cd :: bc :: [ab]
+
+    -- sequence of Homs
+    data HomSeq : {n : ℕ} → (os : obSeq n) → Type (ℓ-max ℓ ℓ') where
+      h[_] : {os : obSeq z} → Hom[ lookup os (suc Fin.zero) , lookup os (inject₁ Fin.zero) ] → HomSeq os
+      _h∷_ : {n : ℕ} {os : obSeq n} {o : ob} → Hom[ (head os) , o ] → HomSeq os → HomSeq (o ∷ os)
+
+    homSeqN : {n : ℕ} → (os : obSeq n) → (m : Fin (suc n)) → Type ℓ'
+    homSeqN {n = n} os m = Hom[ (lookup os (opposite (inject₁ m))) , (lookup os (opposite (suc m))) ]
+
+    -- homSeqLookupOpp : {n : ℕ} {os : obSeq n} → HomSeq os → (m : Fin (suc n)) → homSeqN os m
+    -- homSeqLookupOpp {n = ℕ.zero} {os = y ∷ x ∷ []} h[ h ] Fin.zero = h
+    -- homSeqLookupOpp {n = suc n} {os = y ∷ x ∷ os} (h1 h∷ hs) (suc m) =
+    --   homSeqLookupOpp {n = n} {os = x ∷ os} hs {!   !}
+    -- homSeqLookup {n = ℕ.zero} h[ x ] Fin.zero = {! x  !}
+    -- homSeqLookup {n = suc n} (_h∷_ {os = os} {o = o} h1 hs) m = helper {!    !} where
+    --   op = opposite m
+    --   helper : (k : Fin (2+ n)) → homSeqN (o ∷ os) (opposite k)
+    --   helper k = {!   !}
+    
+    -- Retrieve the LAST hom in the sequence
+    -- hhead : ∀ {n : ℕ} {os : obSeq n} → HomSeq os → Hom[ {!   !} , {!   !} ]
+    -- hhead h[ x ] = x
+    -- hhead (x h∷ hs) = x
+
+    -- htail : ∀ {n : ℕ} {os : obSeq (suc n)} → HomSeq os → HomSeq (tail os)
+    -- htail {n} {x ∷ os} (x₁ h∷ hs) = hs
+
+    -- hlookup : ∀ {n : ℕ} {os : obSeq (suc n)}
+    --   → HomSeq os → (m : Fin n) → Hom[ lookup os (inject₁ (inject₁ (inject₁ m))) , lookup os (inject₁ (inject₁ (suc m))) ]
+    -- hlookup {n = suc ℕ.zero} (x h∷ hs) m = {! x  !}
+    -- hlookup {n = 2+ n} hs m = {!   !}
+
+    -- -- exactHomSeq must have at least 3 obs
+    -- exactHomSeq : {n : ℕ} → {os : obSeq (suc n)} → HomSeq os → (m : Fin (suc n)) → Type ℓ'
+    -- exactHomSeq {n = ℕ.zero} (y h∷ h[ x ]) Fin.zero = isExact x y
+    -- exactHomSeq {n = suc n} (y h∷ (x h∷ x₂)) Fin.zero = {!   !}
+    -- exactHomSeq {n = suc n} (y h∷ (x h∷ x₂)) (suc m) = {!   !}
+
+    -- -- exactHomVec : Type (ℓ-max ℓ ℓ')
+    -- -- exactHomVec = {n : ℕ} {o : ob} →                 
+    -- --   Σ (HomVec o n) λ h → finExactSequence {!   !} {!   !} 

src/Misc/FiveLemma/Category/Lemma.agda

@@ -0,0 +1,78 @@
+{-# OPTIONS --cubical #-}
+
+module Misc.FiveLemma.Category.Lemma where
+
+open import Agda.Primitive
+open import Cubical.Data.Sigma
+open import Cubical.Categories.Abelian
+open import Cubical.Categories.Additive
+open import Cubical.Categories.Category
+open import Cubical.Categories.Morphism
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Functions.Embedding
+open import Cubical.Functions.Surjection
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module fiveLemma (AC : AbelianCategory ℓ ℓ') where
+  open AbelianCategory AC
+
+  -- image is defined as kernel (cokernel f)
+  image : {x y : ob} (f : Hom[ x , y ]) → Σ ob (λ i → Hom[ i , y ])
+  image f = hasKernels (coker f) .Kernel.k , (ker (coker f))
+
+  isExact : {x y z : ob} (f : Hom[ x , y ]) (g : Hom[ y , z ]) → Type ℓ'
+  isExact {y = y} f g = Σ (Hom[ (Kernel.k g-ker) , (fst f-im) ]) λ m → isIso cat m where
+    f-im = image f
+    g-ker = hasKernels g
+
+  module _
+    (A B C D E A' B' C' D' E' : ob)
+    (f : Hom[ A , B ])
+    (g : Hom[ B , C ])
+    (h : Hom[ C , D ])
+    (j : Hom[ D , E ])
+    (l : Hom[ A , A' ])
+    (m : Hom[ B , B' ])
+    (n : Hom[ C , C' ])
+    (p : Hom[ D , D' ])
+    (q : Hom[ E , E' ])
+    (r : Hom[ A' , B' ])
+    (s : Hom[ B' , C' ])
+    (t : Hom[ C' , D' ])
+    (u : Hom[ D' , E' ])
+    (fgExact : isExact f g)
+    (ghExact : isExact g h)
+    (hjExact : isExact h j)
+    (rsExact : isExact r s)
+    (stExact : isExact s t)
+    (tuExact : isExact t u)
+    (lEpi : isEpic cat l)
+    (mIso : isIso cat m)
+    (pIso : isIso cat p)
+    (qMono : isMonic cat q)
+    (sq1 : (_⋆_ l r) ≡ (_⋆_ f m))
+    (sq2 : (_⋆_ m s) ≡ (_⋆_ g n))
+    (sq3 : (_⋆_ n t) ≡ (_⋆_ h p))
+    (sq4 : (_⋆_ p u) ≡ (_⋆_ j q))
+    where
+      nEpi : isEpic cat n
+      nEpi b∘n≡b'∘n = {!   !} where
+        
+
+        -- lemma : isExact f g → isExact g h → isExact h j
+        --   → isExact r s → isExact s t → isExact t u
+        --   → isSurjection (fst l) → isEquiv (fst m) → isEquiv (fst p) → isEmbedding (fst q)
+        --   → isEquiv (fst n)
+        -- lemma fgIsExact ghIsExact hjIsExact rsIsExact stIsExact tuIsExact lIsSurjection mIsEquiv pIsEquiv qIsInjection =
+        --   isEmbedding×isSurjection→isEquiv (nIsEmbedding , nIsSurjection) where
+        --     nIsEmbedding : isEmbedding (fst n)
+        --     nIsEmbedding c1 c2 = {!   !}
+
+        --     nIsSurjection : isSurjection (fst n)
+        --     nIsSurjection b = {!   !}  

src/Misc/FiveLemma/Group/Exact.agda

@@ -0,0 +1,18 @@
+{-# OPTIONS --cubical #-}
+
+module Misc.FiveLemma.Group.Exact where
+
+open import Agda.Primitive
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Misc.FiveLemma.Group.Morphisms
+
+private
+  variable
+    ℓ ℓ' : Level
+
+isExact : {A B C : Group ℓ} → (f : GroupHom A B) → (g : GroupHom B C) → Type ℓ
+isExact {B = B} f g = (b : ⟨ B ⟩) → (isInKer g b) ≃ (isInIm' f b)

src/Misc/FiveLemma/Group/ExactSequence.agda

@@ -0,0 +1,66 @@
+{-# OPTIONS --cubical #-}
+
+module Misc.FiveLemma.Group.ExactSequence where
+
+open import Agda.Primitive
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.Instances.Unit
+open import Cubical.Data.Nat hiding (_·_)
+open import Data.Fin
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Isomorphism
+open import Misc.FiveLemma.Group.Exact
+open import Misc.FiveLemma.Group.Morphisms
+
+private
+  variable
+    ℓ ℓ' : Level
+
+pattern 1+ n = suc n
+pattern 2+ n = suc (suc n)
+
+inj1 = λ {m : ℕ} (n : Fin m) → inject₁ n
+inj2 = λ {m : ℕ} (n : Fin m) → inject₁ (inject₁ n)
+
+FiniteLES : {len : ℕ}
+  → (groupSeq : (n : Fin (2+ len)) → Group ℓ)
+  → (homSeq : (m : Fin (1+ len)) → GroupHom (groupSeq (inj1 m)) (groupSeq (suc m)))
+  → Type ℓ
+FiniteLES {len = len} groupSeq homSeq = (m : Fin len) → isExact (homSeq (inj1 m)) (homSeq (suc m))
+
+InfiniteLES :
+  (groupSeq : (n : ℕ) → Group ℓ)
+  → (homSeq : (n : ℕ) → GroupHom (groupSeq n) (groupSeq (suc n)))
+  → Type ℓ
+InfiniteLES groupSeq homSeq = (m : ℕ) → isExact (homSeq m) (homSeq (suc m))
+
+module _ {A B : Group ℓ} (f : GroupHom A B) where
+  private
+    groupSeq : (n : Fin 3) → Group ℓ
+    groupSeq zero = UnitGroup
+    groupSeq (1+ zero) = A
+    groupSeq (2+ zero) = B
+
+    homSeq : (n : Fin 2) → GroupHom (groupSeq (inj1 n)) (groupSeq (suc n))
+    homSeq zero =
+      let open GroupStr (A .snd) in
+      (λ _ → 1g) ,
+      record {
+        pres· = λ x y → sym (·IdR 1g) ;
+        pres1 = refl ;
+        presinv = λ x → let z = sym (·IdL (inv 1g)) ∙ cong (_· inv 1g) (sym (·InvL 1g)) ∙ sym (·Assoc (inv 1g) 1g (inv 1g)) ∙ cong (inv 1g ·_) (·InvR 1g) ∙ ·InvL 1g in sym z
+      }
+    homSeq (1+ zero) = f
+
+  0AB≃Mono : FiniteLES groupSeq homSeq ≃ isMono f
+  0AB≃Mono = isoToEquiv (iso ff {! gg  !} {!   !} {!   !}) where
+    ff : FiniteLES groupSeq homSeq → isMono f
+    ff ses fx≡fy = {!   !}
+
+    gg : isMono f → FiniteLES groupSeq homSeq
+    gg fMono m a = isoToEquiv (iso {!   !} {!   !} {!   !} {!   !}) where
+      fff : isInKer (homSeq (1+ m)) a → isInIm' (homSeq (inj1 m)) a
+      fff a-in-ker = {!   !}

src/Misc/FiveLemma/Group/Injective.agda

@@ -0,0 +1,134 @@
+{-# OPTIONS --cubical #-}
+
+module Misc.FiveLemma.Group.Injective where
+
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.GroupPath
+open import Cubical.Algebra.Group.Instances.Unit
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.Properties
+open import Cubical.Algebra.Monoid
+open import Cubical.Algebra.Semigroup
+open import Cubical.Data.Unit
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.HITs.PropositionalTruncation.Base
+open import Cubical.HITs.PropositionalTruncation.Properties
+  renaming (rec to propTruncRec ; map to propTruncMap ; rec2 to propTruncRec2 ; map2 to propTruncMap2 ; elim to propTruncElim)
+open import Cubical.HITs.Pushout.Base
+open import Cubical.HITs.Pushout
+
+open import Misc.FiveLemma.Group.Morphisms
+open import Misc.FiveLemma.Group.Exact
+
+open BijectionIso'
+open IsGroupHom
+open GroupStr using (1g)
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module _
+  (A B C D E A' B' C' D' E' : Group ℓ)
+  (f : GroupHom A B) (g : GroupHom B C) (h : GroupHom C D) (j : GroupHom D E)
+  (l : GroupHom A A') (m : BijectionIso' B B') (n : GroupHom C C') (p : BijectionIso' D D') (q : GroupHom E E')
+  (r : GroupHom A' B') (s : GroupHom B' C') (t : GroupHom C' D') (u : GroupHom D' E')
+  (fg : isExact f g) (gh : isExact g h) (hj : isExact h j)
+  (rs : isExact r s) (st : isExact s t) (tu : isExact t u)
+  (lSurj : isSurjective' l)
+  (qInj : isInjective q)
+  (sq1 : (a : fst A) → r .fst (l .fst a) ≡ m .fun .fst (f .fst a))
+  (sq2 : (b : fst B) → s .fst (m .fun .fst b) ≡ n .fst (g .fst b))
+  (sq3 : (c : fst C) → t .fst (n .fst c) ≡ p .fun .fst (h .fst c))
+  (sq4 : (d : fst D) → u .fst (p .fun .fst d) ≡ q .fst (j .fst d))
+  where
+    nInjective : isInjective n
+    nInjective c c-in-ker[n] =
+      let
+        t[n[c]]≡0 : t .fst (n .fst c) ≡ D' .snd .1g
+        t[n[c]]≡0 = cong (t .fst) c-in-ker[n] ∙ t .snd .pres1
+
+        t[n[c]]≡p[h[c]] : t .fst (n .fst c) ≡ p .fun .fst (h .fst c)
+        t[n[c]]≡p[h[c]] = sq3 c
+
+        p[h[c]]≡0 : p .fun .fst (h .fst c) ≡ D' .snd .1g
+        p[h[c]]≡0 = sym t[n[c]]≡p[h[c]] ∙ t[n[c]]≡0
+
+        h[c]≡0 : h .fst c ≡ D .snd .1g
+        h[c]≡0 = p .inj (h .fst c) p[h[c]]≡0
+
+        c-in-ker[h] : isInKer h c
+        c-in-ker[h] = h[c]≡0
+
+        c-in-im[g] : isInIm' g c
+        c-in-im[g] = gh c .fst c-in-ker[h]
+
+        b : ⟨ B ⟩
+        b = fst c-in-im[g]
+
+        g[b]≡c : g .fst b ≡ c
+        g[b]≡c = snd c-in-im[g]
+
+        n[g[b]]≡0 : n .fst (g .fst b) ≡ C' .snd .1g
+        n[g[b]]≡0 = cong (n .fst) g[b]≡c ∙ c-in-ker[n]
+
+        m[b] : ⟨ B' ⟩
+        m[b] = m .fun .fst b
+
+        s[m[b]]≡n[g[b]] : s .fst m[b] ≡ n .fst (g .fst b)
+        s[m[b]]≡n[g[b]] = sq2 b
+
+        s[m[b]]≡0 : s .fst m[b] ≡ C' .snd .1g
+        s[m[b]]≡0 = s[m[b]]≡n[g[b]] ∙ n[g[b]]≡0
+
+        m[b]-in-ker[s] : isInKer s m[b]
+        m[b]-in-ker[s] = s[m[b]]≡0
+        
+        m[b]-in-im[r] : isInIm' r m[b]
+        m[b]-in-im[r] = rs m[b] .fst m[b]-in-ker[s]
+
+        a' : ⟨ A' ⟩
+        a' = fst m[b]-in-im[r]
+
+        r[a']≡m[b] : r .fst a' ≡ m[b]
+        r[a']≡m[b] = snd m[b]-in-im[r]
+
+        a : ⟨ A ⟩
+        a = lSurj a' .fst
+        
+        l[a]≡a' : l .fst a ≡ a'
+        l[a]≡a' = lSurj a' .snd
+
+        m[f[a]] : ⟨ B' ⟩
+        m[f[a]] = m .fun .fst (f .fst a)
+
+        r[l[a]]≡m[f[a]] : r .fst (l .fst a) ≡ m[f[a]]
+        r[l[a]]≡m[f[a]] = sq1 a
+
+        m[f[a]]≡m[b] : m[f[a]] ≡ m[b]
+        m[f[a]]≡m[b] = sym r[l[a]]≡m[f[a]] ∙ cong (r .fst) l[a]≡a' ∙ r[a']≡m[b]
+
+        f[a]≡b : f .fst a ≡ b
+        f[a]≡b = isInjective→isMono (m .fun) (m .inj) m[f[a]]≡m[b]
+
+        g[f[a]]≡c : g .fst (f .fst a) ≡ c
+        g[f[a]]≡c = cong (g .fst) f[a]≡b ∙ g[b]≡c
+
+        f[a]-in-im[f] : isInIm' f (f .fst a)
+        f[a]-in-im[f] = a , refl
+
+        f[a]-in-ker[g] : isInKer g (f .fst a)
+        f[a]-in-ker[g] = invIsEq (fg (f .fst a) .snd) f[a]-in-im[f]
+
+        g[f[a]]≡0 : g .fst (f .fst a) ≡ C .snd .1g
+        g[f[a]]≡0 = f[a]-in-ker[g]
+
+        c≡0 : c ≡ C .snd .1g
+        c≡0 = sym g[f[a]]≡c ∙ g[f[a]]≡0
+      in c≡0

src/Misc/FiveLemma/Group/Lemma.agda

@@ -0,0 +1,57 @@
+{-# OPTIONS --cubical #-}
+
+module Misc.FiveLemma.Group.Lemma where
+
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.GroupPath
+open import Cubical.Algebra.Group.Instances.Unit
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.Properties
+open import Cubical.Algebra.Monoid
+open import Cubical.Algebra.Semigroup
+open import Cubical.Data.Unit
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.HITs.PropositionalTruncation.Base
+open import Cubical.HITs.PropositionalTruncation.Properties
+  renaming (rec to propTruncRec ; map to propTruncMap ; rec2 to propTruncRec2 ; map2 to propTruncMap2 ; elim to propTruncElim)
+open import Cubical.HITs.Pushout.Base
+open import Cubical.HITs.Pushout
+
+open import Misc.FiveLemma.Group.Morphisms
+open import Misc.FiveLemma.Group.Exact
+open import Misc.FiveLemma.Group.Injective
+open import Misc.FiveLemma.Group.Surjective
+
+open BijectionIso'
+open IsGroupHom
+open GroupStr using (1g)
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module _
+  (A B C D E A' B' C' D' E' : Group ℓ)
+  (f : GroupHom A B) (g : GroupHom B C) (h : GroupHom C D) (j : GroupHom D E)
+  (l : GroupHom A A') (m : BijectionIso' B B') (n : GroupHom C C') (p : BijectionIso' D D') (q : GroupHom E E')
+  (r : GroupHom A' B') (s : GroupHom B' C') (t : GroupHom C' D') (u : GroupHom D' E')
+  (fg : isExact f g) (gh : isExact g h) (hj : isExact h j)
+  (rs : isExact r s) (st : isExact s t) (tu : isExact t u)
+  (lSurj : isSurjective' l)
+  (qInj : isInjective q)
+  (sq1 : (a : fst A) → r .fst (l .fst a) ≡ m .fun .fst (f .fst a))
+  (sq2 : (b : fst B) → s .fst (m .fun .fst b) ≡ n .fst (g .fst b))
+  (sq3 : (c : fst C) → t .fst (n .fst c) ≡ p .fun .fst (h .fst c))
+  (sq4 : (d : fst D) → u .fst (p .fun .fst d) ≡ q .fst (j .fst d))
+  where
+    nInj = nInjective A B C D E A' B' C' D' E' f g h j l m n p q r s t u fg gh hj rs st tu lSurj qInj sq1 sq2 sq3 sq4
+    nSur = nSurjective A B C D E A' B' C' D' E' f g h j l m n p q r s t u fg gh hj rs st tu lSurj qInj sq1 sq2 sq3 sq4
+
+    lemma : BijectionIso' C C'
+    lemma = bijIso' n nInj nSur

src/Misc/FiveLemma/Group/Morphisms.agda

@@ -0,0 +1,61 @@
+{-# OPTIONS --cubical #-}
+
+-- I'm doing this just because isInIm is defined to be a mere prop
+-- Not sure why it's defined this way yet
+-- TODO: Find out
+
+module Misc.FiveLemma.Group.Morphisms where
+
+open import Agda.Primitive
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Semigroup
+open import Cubical.Data.Sigma
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.HITs.PropositionalTruncation
+
+private
+  variable
+    ℓ ℓ' : Level
+    G H : Group ℓ
+
+isInIm' : GroupHom G H → ⟨ H ⟩ → Type _
+isInIm' {G = G} ϕ h = Σ[ g ∈ ⟨ G ⟩ ] ϕ .fst g ≡ h
+
+Im' : GroupHom G H → Type _
+Im' {H = H} ϕ = Σ[ x ∈ ⟨ H ⟩ ] isInIm' ϕ x
+
+isSurjective' : GroupHom G H → Type _
+isSurjective' {H = H} ϕ = (x : ⟨ H ⟩) → isInIm' ϕ x
+
+-- Group bijections
+record BijectionIso' (G : Group ℓ) (H : Group ℓ') : Type (ℓ-max ℓ ℓ') where
+  constructor bijIso'
+
+  field
+    fun : GroupHom G H
+    inj : isInjective fun
+    surj : isSurjective' fun
+
+module _ where
+  open GroupStr
+  open BijectionIso'
+
+  BijectionIso'→GroupIso : BijectionIso' G H → GroupIso G H
+  BijectionIso'→GroupIso {G = G} {H = H} i = grIso
+    where
+    f = fst (fun i)
+
+    helper : (b : _) → isProp (Σ[ a ∈ ⟨ G ⟩ ] f a ≡ b)
+    helper _ (a , ha) (b , hb) =
+      Σ≡Prop (λ _ → is-set (snd H) _ _)
+            (isInjective→isMono (fun i) (inj i) (ha ∙ sym hb) )
+
+    grIso : GroupIso G H
+    grIso = iso f g fg gf , snd (fun i) where
+      g = λ b → rec (helper b) (λ a → a) ∣ (surj i b) ∣₁ .fst
+      fg = λ b → rec (helper b) (λ a → a) ∣ (surj i b) ∣₁ .snd
+      gf = λ b j → rec (helper (f b)) (λ a → a) (squash₁ ∣ (surj i (f b)) ∣₁ ∣ (b , refl) ∣₁ j) .fst

src/Misc/FiveLemma/Group/Surjective.agda

@@ -0,0 +1,188 @@
+{-# OPTIONS --cubical #-}
+
+module Misc.FiveLemma.Group.Surjective where
+
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.GroupPath
+open import Cubical.Algebra.Group.Instances.Unit
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.Properties
+open import Cubical.Algebra.Monoid
+open import Cubical.Algebra.Semigroup
+open import Cubical.Data.Unit
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.HITs.PropositionalTruncation.Base
+open import Cubical.HITs.PropositionalTruncation.Properties
+  renaming (rec to propTruncRec ; map to propTruncMap ; rec2 to propTruncRec2 ; map2 to propTruncMap2 ; elim to propTruncElim)
+open import Cubical.HITs.Pushout.Base
+open import Cubical.HITs.Pushout
+
+open import Misc.FiveLemma.Group.Morphisms
+open import Misc.FiveLemma.Group.Exact
+
+open BijectionIso'
+open IsGroupHom
+open GroupStr using (1g)
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module _
+  (A B C D E A' B' C' D' E' : Group ℓ)
+  (f : GroupHom A B) (g : GroupHom B C) (h : GroupHom C D) (j : GroupHom D E)
+  (l : GroupHom A A') (m : BijectionIso' B B') (n : GroupHom C C') (p : BijectionIso' D D') (q : GroupHom E E')
+  (r : GroupHom A' B') (s : GroupHom B' C') (t : GroupHom C' D') (u : GroupHom D' E')
+  (fg : isExact f g) (gh : isExact g h) (hj : isExact h j)
+  (rs : isExact r s) (st : isExact s t) (tu : isExact t u)
+  (lSurj : isSurjective' l)
+  (qInj : isInjective q)
+  (sq1 : (a : fst A) → r .fst (l .fst a) ≡ m .fun .fst (f .fst a))
+  (sq2 : (b : fst B) → s .fst (m .fun .fst b) ≡ n .fst (g .fst b))
+  (sq3 : (c : fst C) → t .fst (n .fst c) ≡ p .fun .fst (h .fst c))
+  (sq4 : (d : fst D) → u .fst (p .fun .fst d) ≡ q .fst (j .fst d))
+  where
+    nSurjective : isSurjective' n
+    nSurjective c' =
+      let
+        d' : ⟨ D' ⟩
+        d' = t .fst c'
+
+        pGroupIso = BijectionIso'→GroupIso p
+        pIso = pGroupIso .fst
+        pInv = Iso.inv pIso
+
+        d = ⟨ D ⟩
+        d = pInv d'
+
+        p[d]≡t[c'] : p .fun .fst d ≡ t .fst c'
+        p[d]≡t[c'] = Iso.rightInv pIso d'
+
+        u[p[d]] : ⟨ E' ⟩
+        u[p[d]] = u .fst (p .fun .fst d)
+
+        j[d] : ⟨ E ⟩
+        j[d] = j .fst d
+
+        q[j[d]] : ⟨ E' ⟩
+        q[j[d]] = q .fst j[d]
+
+        u[p[d]]≡q[j[d]] : u[p[d]] ≡ q[j[d]]
+        u[p[d]]≡q[j[d]] = sq4 d
+
+        d'-in-ker[u] : isInKer u d'
+        d'-in-ker[u] =
+          let im[t]→ker[u] = invIsEq (tu d' .snd) in
+          im[t]→ker[u] (c' , refl)
+
+        u[p[d]]≡0 : u[p[d]] ≡ E' .snd .1g
+        u[p[d]]≡0 = cong (u .fst) p[d]≡t[c'] ∙ d'-in-ker[u]
+
+        q[j[d]]≡0 : q[j[d]] ≡ E' .snd .1g
+        q[j[d]]≡0 = sym u[p[d]]≡q[j[d]] ∙ u[p[d]]≡0
+
+        j[d]≡0 : j[d] ≡ E .snd .1g
+        j[d]≡0 = qInj j[d] q[j[d]]≡0
+
+        d-in-ker[j] : isInKer j d
+        d-in-ker[j] = j[d]≡0
+
+        d-in-im[h] : isInIm' h d
+        d-in-im[h] =
+          let ker[j]→im[h] = hj d .fst in
+          ker[j]→im[h] d-in-ker[j]
+
+        c : ⟨ C ⟩
+        c = d-in-im[h] .fst
+
+        h[c]≡d : h .fst c ≡ d
+        h[c]≡d = d-in-im[h] .snd
+
+        n[c] : ⟨ C' ⟩
+        n[c] = n .fst c
+
+        t[n[c]]≡p[h[c]] : t .fst n[c] ≡ p .fun .fst (h .fst c)
+        t[n[c]]≡p[h[c]] = sq3 c
+
+        t[n[c]]≡t[c'] : t .fst n[c] ≡ t .fst c'
+        t[n[c]]≡t[c'] =
+          t .fst n[c]             ≡⟨ t[n[c]]≡p[h[c]] ⟩
+          p .fun .fst (h .fst c)  ≡⟨ cong (p .fun .fst) h[c]≡d ⟩
+          p .fun .fst d           ≡⟨ p[d]≡t[c'] ⟩
+          t .fst c' ∎
+
+        c'-n[c] : ⟨ C' ⟩
+        c'-n[c] = let open GroupStr (C' .snd) in c' · (inv n[c])
+
+        t[c'-n[c]]≡0 : t .fst c'-n[c] ≡ D' .snd .1g
+        t[c'-n[c]]≡0 =
+          let open GroupStr (C' .snd) renaming (_·_ to _·ᶜ_; inv to invᶜ) in
+          let open GroupStr (D' .snd) renaming (_·_ to _·ᵈ_; inv to invᵈ) hiding (isGroup) in
+          t .fst (c' ·ᶜ (invᶜ n[c]))          ≡⟨ t .snd .pres· c' (invᶜ n[c]) ⟩
+          (t .fst c') ·ᵈ (t .fst (invᶜ n[c])) ≡⟨ cong ((t .fst c') ·ᵈ_) (t .snd .presinv n[c]) ⟩
+          (t .fst c') ·ᵈ (invᵈ (t .fst n[c])) ≡⟨ cong (λ z → (t .fst c') ·ᵈ (invᵈ z)) t[n[c]]≡t[c'] ⟩
+          (t .fst c') ·ᵈ (invᵈ (t .fst c'))   ≡⟨ cong ((t .fst c') ·ᵈ_) (sym (t .snd .presinv c')) ⟩
+          (t .fst c') ·ᵈ (t .fst (invᶜ c'))   ≡⟨ sym (t .snd .pres· c' (invᶜ c')) ⟩
+          t .fst (c' ·ᶜ (invᶜ c'))            ≡⟨ cong (t .fst) (IsGroup.·InvR isGroup c') ⟩
+          t .fst (C' .snd .1g)                ≡⟨ t .snd .pres1 ⟩
+          D' .snd .1g ∎
+
+        [c'-n[c]]-in-ker[t] : isInKer t c'-n[c]
+        [c'-n[c]]-in-ker[t] = t[c'-n[c]]≡0
+
+        [c'-n[c]]-in-im[s] : isInIm' s c'-n[c]
+        [c'-n[c]]-in-im[s] =
+          let ker[t]→im[s] = st c'-n[c] .fst in
+          ker[t]→im[s] [c'-n[c]]-in-ker[t]
+
+        b' : ⟨ B' ⟩
+        b' = [c'-n[c]]-in-im[s] .fst
+
+        s[b']≡c'-n[c] : s .fst b' ≡ c'-n[c]
+        s[b']≡c'-n[c] = [c'-n[c]]-in-im[s] .snd
+
+        mGroupIso = BijectionIso'→GroupIso m
+        mIso = mGroupIso .fst
+        mInv = Iso.inv mIso
+
+        b : ⟨ B ⟩
+        b = mInv b'
+
+        m[b]≡b' : m .fun .fst b ≡ b'
+        m[b]≡b' = Iso.rightInv mIso b'
+
+        s[m[b]]≡s[b'] : s .fst (m .fun .fst b) ≡ s .fst b'
+        s[m[b]]≡s[b'] = cong (s .fst) m[b]≡b'
+
+        s[m[b]]≡c'-n[c] : s .fst (m .fun .fst b) ≡ c'-n[c]
+        s[m[b]]≡c'-n[c] = s[m[b]]≡s[b'] ∙ s[b']≡c'-n[c]
+
+        g[b] : ⟨ C ⟩
+        g[b] = g .fst b
+
+        g[b]+c : ⟨ C ⟩
+        g[b]+c = C .snd .GroupStr._·_ g[b] c
+
+        n[g[b]] : ⟨ C' ⟩
+        n[g[b]] = n .fst g[b]
+
+        n[g[b]]≡s[m[b]] : n[g[b]] ≡ s .fst (m .fun .fst b)
+        n[g[b]]≡s[m[b]] = sym (sq2 b)
+
+        n[g[b]]≡c'-n[c] : n[g[b]] ≡ c'-n[c]
+        n[g[b]]≡c'-n[c] = n[g[b]]≡s[m[b]] ∙ s[m[b]]≡c'-n[c]
+
+        n[g[b]]+n[c]≡c' : C' .snd .GroupStr._·_ n[g[b]] n[c] ≡ c'
+        n[g[b]]+n[c]≡c' =
+          let open GroupStr (C' .snd) in
+          cong (_· n[c]) n[g[b]]≡c'-n[c] ∙ sym (·Assoc c' (inv n[c]) n[c]) ∙ cong (c' ·_) (·InvL n[c]) ∙ ·IdR c'
+
+        n[g[b]+c]≡c' : n .fst g[b]+c ≡ c'
+        n[g[b]+c]≡c' = n .snd .pres· g[b] c ∙ n[g[b]]+n[c]≡c'
+      in g[b]+c , n[g[b]+c]≡c'

src/Misc/STLCLogRel.agda

@@ -0,0 +1,135 @@
+module Misc.STLCLogRel where
+
+open import Agda.Builtin.Sigma
+open import Data.Bool
+open import Data.Empty
+open import Data.Fin hiding (fold)
+open import Data.Maybe
+open import Data.Nat
+open import Data.Product
+open import Data.Sum
+open import Relation.Nullary
+
+id : {A : Set} → A → A
+id {A} x = x
+
+data type : Set where
+  unit : type
+  bool : type
+  _-→_ : type → type → type
+  `_ : ℕ → type
+  μ_ : type → type
+
+data term : Set where
+  `_ : ℕ → term
+  `true : term
+  `false : term
+  `if_then_else_ : term → term → term → term
+  `λ[_]_ : (τ : type) → (e : term) → term
+  _∙_ : term → term → term
+  `fold : term → term
+  `unfold : term → term
+
+data ctx : Set where
+  nil : ctx
+  cons : ctx → type → ctx
+
+lookup : ctx → ℕ → Maybe type
+lookup nil _ = nothing
+lookup (cons ctx₁ x) zero = just x 
+lookup (cons ctx₁ x) (suc n) = lookup ctx₁ n
+
+data type-sub : Set where
+  nil : type-sub
+
+type-subst : type → type → type
+type-subst unit v = unit
+type-subst bool v = bool
+type-subst (τ -→ τ₁) v = (type-subst τ v) -→ (type-subst τ₁ v)
+type-subst (` zero) v = v
+type-subst (` suc x) v = ` x
+type-subst (μ τ) v = μ (type-subst τ v)
+
+data sub : Set where
+  nil : sub
+  cons : sub → term → sub
+
+subst : term → term → term
+subst (` zero) v = v
+subst (` suc x) v = ` x
+subst `true v = `true
+subst `false v = `false
+subst (`if x then x₁ else x₂) v = `if (subst x v) then (subst x₁ v) else (subst x₂ v)
+subst (`λ[ τ ] x) v = `λ[ τ ] subst x v
+subst (x ∙ x₁) v = (subst x v) ∙ (subst x₁ v)
+subst (`fold x) v = `fold (subst x v)
+subst (`unfold x) v = `unfold (subst x v)
+
+data value-rel : type → term → Set where 
+  v-`true : value-rel bool `true
+  v-`false : value-rel bool `false
+  v-`λ[_]_ : ∀ {τ e} → value-rel τ (`λ[ τ ] e)
+  v-`fold : ∀ {τ e} → value-rel (type-subst τ (μ τ)) e → value-rel (μ τ) (`fold e)
+
+data good-subst : ctx → sub → Set where
+  nil : good-subst nil nil
+  cons : ∀ {ctx τ γ v}
+    → good-subst ctx γ
+    → value-rel τ v
+    → good-subst (cons ctx τ) γ
+
+data step : term → term → Set where
+  step-if-1 : ∀ {e₁ e₂} → step (`if `true then e₁ else e₂) e₁
+  step-if-2 : ∀ {e₁ e₂} → step (`if `false then e₁ else e₂) e₂
+  step-`λ : ∀ {τ e v} → step ((`λ[ τ ] e) ∙ v) (subst e v)
+  step-`fold : ∀ {v} → step (`unfold (`fold v)) v
+
+data steps : ℕ → term → term → Set where
+  zero : ∀ {e} → steps zero e e
+  suc : ∀ {e e' e''} → (n : ℕ) → step e e' → steps n e' e'' → steps (suc n) e e''
+
+data _⊢_∶_ : ctx → term → type → Set where
+  type-`true : ∀ {ctx} → ctx ⊢ `true ∶ bool
+  type-`false : ∀ {ctx} → ctx ⊢ `false ∶ bool
+  type-`ifthenelse : ∀ {ctx e e₁ e₂ τ}
+    → ctx ⊢ e ∶ bool
+    → ctx ⊢ e₁ ∶ τ
+    → ctx ⊢ e₂ ∶ τ
+    → ctx ⊢ (`if e then e₁ else e₂) ∶ τ
+  type-`x : ∀ {ctx x}
+    → (p : Is-just (lookup ctx x))
+    → ctx ⊢ (` x) ∶ (to-witness p)
+  type-`λ : ∀ {ctx τ τ₂ e}
+    → (cons ctx τ) ⊢ e ∶ τ₂
+    → ctx ⊢ (`λ[ τ ] e) ∶ (τ -→ τ₂)
+  type-∙ : ∀ {ctx τ₁ τ₂ e₁ e₂}
+    → ctx ⊢ e₁ ∶ (τ₁ -→ τ₂)
+    → ctx ⊢ e₂ ∶ τ₂
+    → ctx ⊢ (e₁ ∙ e₂) ∶ τ₂
+
+  type-`fold : ∀ {ctx τ e}
+    → ctx ⊢ e ∶ (type-subst τ (μ τ))
+    → ctx ⊢ (`fold e) ∶ (μ τ)
+  type-`unfold : ∀ {ctx τ e}
+    → ctx ⊢ e ∶ (μ τ)
+    → ctx ⊢ (`unfold e) ∶ (type-subst τ (μ τ))
+
+irreducible : term → Set
+irreducible e = ¬ (∃ λ e' → step e e')
+
+data term-relation : type → term → Set where
+  e-term : ∀ {τ e}
+    → (∀ {n} → (e' : term) → steps n e e' → irreducible e' → value-rel τ e')
+    → term-relation τ e
+
+type-sound : ∀ {Γ e τ} → Γ ⊢ e ∶ τ → Set
+type-sound {Γ} {e} {τ} s = ∀ {n} → (e' : term) → steps n e e' → value-rel τ e' ⊎ ∃ λ e'' → step e' e''
+
+_⊨_∶_ : (Γ : ctx) → (e : term) → (τ : type) → Set
+_⊨_∶_ Γ e τ = (γ : sub) → (good-subst Γ γ) → term-relation τ e
+
+fundamental : ∀ {Γ e τ} → (well-typed : Γ ⊢ e ∶ τ) → type-sound well-typed → Γ ⊨ e ∶ τ
+fundamental {Γ} {e} {τ} well-typed type-sound γ good-sub = e-term f
+  where
+    f : {n : ℕ} (e' : term) → steps n e e' → irreducible e' → value-rel τ e'
+    f e' steps irred = [ id , (λ exists → ⊥-elim (irred exists)) ] (type-sound e' steps)

src/Sorry.agda

@@ -0,0 +1,8 @@
+{-# OPTIONS --cubical-compatible #-}
+
+module Sorry where
+
+open import Agda.Primitive
+
+postulate
+  sorry : {l : Level} → {A : Set l} → A

src/ThesisWork/EMSpace.agda

@@ -0,0 +1,42 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.EMSpace where
+
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Data.Nat
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Homotopy.Loopspace
+open import Cubical.Homotopy.Group.Base
+open import Cubical.HITs.SetTruncation as ST hiding (rec)
+open import Cubical.HITs.Truncation as T hiding (rec)
+
+variable
+  ℓ ℓ' : Level
+
+data K1 {ℓ : Level} (G : Group ℓ) : Type ℓ where
+  base : K1 G
+  loop : ⟨ G ⟩ → base ≡ base
+  loop-1g : loop (str G .GroupStr.1g) ≡ refl
+  loop-∙ : (x y : ⟨ G ⟩) → loop (str G .GroupStr._·_ x y) ≡ loop y ∙ loop x
+
+K[_,1] : (G : Group ℓ) → Type ℓ
+K[ G ,1] = ∥ K1 G ∥ 3
+
+π₁KG1≃G : (G : Group ℓ) → GroupIso (πGr 0 (K[ G ,1] , ∣ base ∣)) G
+π₁KG1≃G G = {!   !} , {!   !} where
+
+module _ where
+  open import Cubical.HITs.S1
+  open import Cubical.Data.Int
+  open import Cubical.Algebra.Group.Instances.Int
+
+  K[Z,1]=S1 : K[ ℤGroup ,1] ≃ S¹
+  K[Z,1]=S1 = isoToEquiv (iso f {!   !} {!   !} {!   !}) where
+    f : K[ ℤGroup ,1] → S¹
+    f x = T.rec {!   !} {!   !} {!   !}

src/ThesisWork/LES.agda

@@ -1,93 +0,0 @@
-{-# OPTIONS --cubical #-}
-
-module ThesisWork.LES where
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.Pointed
-open import Cubical.Foundations.Equiv
-open import Data.Nat
-open import Data.Fin
-open import Data.Product
-open import Cubical.Homotopy.Base
-open import Cubical.Homotopy.Loopspace
-open import Cubical.Homotopy.Group.Base
-open import Cubical.Homotopy.Group.LES
-open import Cubical.HITs.SetTruncation renaming (map to mapTrunc)
-open import Cubical.HITs.SetTruncation.Fibers
-
-private
-  variable
-    X Y : Type
-
-LES-node : ∀ {l} → {X Y : Pointed l} → (f : X →∙ Y) → ℕ × Fin 3 → Type l
-LES-node {Y = Y} f (n , zero) = π n Y
-LES-node {X = X} f (n , suc zero) = π n X
-LES-node {X = (X , x)} {Y = (Y , y)} (f , f-eq) (n , suc (suc zero)) =
-    let F = fiber f y in
-    π n (F , x , f-eq)
-
-sucF : ℕ × Fin 3 → ℕ × Fin 3
-sucF (n , zero) = n , suc zero
-sucF (n , suc zero) = n , suc (suc zero)
-sucF (n , suc (suc zero)) = suc n , zero
-
-LES-edge : ∀ {l} → {X∙ Y∙ : Pointed l} → (f∙ : X∙ →∙ Y∙) → (n : ℕ × Fin 3)
-    → LES-node f∙ (sucF n) → LES-node f∙ n
-LES-edge {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) (n , zero) = h n where
-    h1 : ∀ (n : ℕ) → (Ω^ n) X∙ →∙ (Ω^ n) Y∙
-    h1 zero = f∙
-    h1 (suc n) = (λ x → refl) , helper where
-        helper : refl ≡ snd (Ω ((Ω^ n) Y∙))
-        helper i j = (Ω^ n) (Y , y) .snd
-
-        -- helper = λ i j →
-        --     let
-        --         top : (Ω^ n) (Y , y) .fst
-        --         top = {!  refl !}
-        --         u = λ k → λ where
-        --             (i = i0) → {!   !}
-        --             (i = i1) → {!   !}
-        --             (j = i0) → {!   !}
-        --             (j = i1) → {!   !}
-        --     in hcomp u {!   !}
-
-    h : ∀ (n : ℕ) → π n X∙ → π n Y∙
-    h n = mapTrunc (fst (h1 n))
-
-    -- h zero ∣ a ∣₂ = ∣ f a ∣₂
-    -- h (suc n) ∣ a ∣₂ = let IH = h n ∣ a i0 ∣₂ in ∣ {!   !} ∣₂
-    -- h zero (squash₂ a b p q i j) = squash₂ (h 0 a) (h 0 b) (cong (h 0) p) (cong (h 0) q) i j
-    -- h (suc n) (squash₂ a b p q i j) = {!   !}
-
-LES-edge {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) (n , suc zero) = h n where
-    F = fiber f y
-    
-    h1 : ∀ (n : ℕ) → (Ω^ n) (F , x , f-eq) →∙ (Ω^ n) X∙
-    h1 zero = fst , refl
-    h1 (suc n) = (λ f i → (Ω^ n) (X , x) .snd) , λ i j → (Ω^ n) (X , x) .snd
-
-    h : ∀ (n : ℕ) → π n (F , x , f-eq) → π n X∙
-    h n = mapTrunc (fst (h1 n))
-
-LES-edge {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) (n , suc (suc zero)) = h n where
-    F = fiber f y
-
-    h1 : ∀ (n : ℕ) → (Ω^ (suc n)) Y∙ →∙ (Ω^ n) (F , x , f-eq)
-    h1 zero = (λ y → x , f-eq) , refl
-    h1 (suc n) = (λ y i → (Ω^ n) (F , x , f-eq) .snd) , λ i j → (Ω^ n) (F , x , f-eq) .snd
-
-    h : ∀ (n : ℕ) → π (suc n) Y∙ → π n (F , x , f-eq)
-    h n = mapTrunc (fst (h1 n))
-
--- LES-edge f n_ with mapN n_
--- LES-edge {X = X∙ @ (X , x)} {Y = Y∙ @ (Y , y)} f n_ | (n , zero) = {! h  !} where
---     h : π n X∙ → π n Y∙
---     h ∣ x ∣₂ = ∣ {!   !} ∣₂
---     h (squash₂ z z₁ p q i i₁) = {!   !}
---     -- z : LES-node f (mapN (suc n_))
---     -- z : π n X
---     -- z : ∥ typ ((Ω^ 0) X) ∥₂
---     -- z : ∥ typ X ∥₂
---     -- z : ∥ typ X ∥₂
--- LES-edge f n_ | (n , suc zero) = λ z → {!   !}       
--- LES-edge f n_ | (n , suc (suc zero)) = λ z → {!   !} 

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

@@ -4,6 +4,7 @@ module ThesisWork.Pi3S2.Lemma4-1-5 where
 
 open import Cubical.Data.Sigma
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Equiv.Properties
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Pointed
@@ -23,14 +24,69 @@ lemma {A∙ = A∙ @ (A , a0)} {B∙ = B∙ @ (B , b0)} f∙ @ (f , f-eq) = eqv
   eqv : fst (fiberF ((λ r → fst r) , refl)) ≃ fst (Ω B∙)
   eqv =
       fst (fiberF ((λ r → fst r) , refl))
-    ≃⟨ {!   !} ⟩
+    ≃⟨ idEquiv (fst (fiberF (fst , refl))) ⟩
       Σ (fst (fiberF f∙)) (λ fibf @ (a , p) → a ≡ a0)
-    ≃⟨ {!   !} ⟩
+    ≃⟨ helper1 ⟩
       Σ A (λ a → (a ≡ a0) × (f a ≡ b0))
-    ≃⟨ {!   !} ⟩
+    ≃⟨ helper2 ⟩
       f a0 ≡ b0
-    ≃⟨ {!   !} ⟩
+    ≃⟨ helper3 ⟩
       b0 ≡ b0
     ≃⟨ idEquiv (b0 ≡ b0) ⟩
       fst (Ω B∙)
-    ■
+    ■ where
+      helper1 : Σ (fst (fiberF (f , f-eq))) (λ fibf → fibf .fst ≡ a0) ≃ Σ A (λ a → (a ≡ a0) × (f a ≡ b0))
+      helper1 = isoToEquiv (iso f' g' (λ _ → refl) λ _ → refl) where
+        f' : Σ (fst (fiberF (f , f-eq))) (λ fibf → fibf .fst ≡ a0) → Σ A (λ a → (a ≡ a0) × (f a ≡ b0))
+        f' x @ ((x1 , x2) , x3) = x1 , x3 , x2 
+
+        g' : Σ A (λ a → (a ≡ a0) × (f a ≡ b0)) → Σ (fst (fiberF (f , f-eq))) (λ fibf → fibf .fst ≡ a0)
+        g' x @ (x1 , x2 , x3) = (x1 , x3) , x2
+
+      helper2 : Σ A (λ a → (a ≡ a0) × (f a ≡ b0)) ≃ (f a0 ≡ b0)
+      helper2 = isoToEquiv (iso f' g' fg {!   !}) where
+        f' : Σ A (λ a → (a ≡ a0) × (f a ≡ b0)) → f a0 ≡ b0
+        f' (x1 , x2 , x3) = cong f (sym x2) ∙ x3 
+
+        g' : f a0 ≡ b0 → Σ A (λ a → (a ≡ a0) × (f a ≡ b0))
+        g' x = a0 , refl , x
+
+        fg : section f' g'
+        fg b =
+          f' (g' b) ≡⟨ refl ⟩
+          f' (a0 , refl , b) ≡⟨ refl ⟩
+          cong f (sym refl) ∙ b ≡⟨ refl ⟩
+          refl ∙ b ≡⟨ sym (lUnit b) ⟩
+          b ∎
+
+        gf : retract f' g'
+        gf a @ (x1 , x2 , x3) =
+          g' (cong f (sym x2) ∙ x3) ≡⟨ refl ⟩
+          a0 , refl , (cong f (sym x2) ∙ x3) ≡⟨ cong (λ b → {!   !}) {!   !} ⟩
+          a ∎
+
+      helper3 : (f a0 ≡ b0) ≃ (b0 ≡ b0)
+      helper3 = isoToEquiv (iso f' g' fg gf) where
+        f' : f a0 ≡ b0 → b0 ≡ b0
+        f' x = sym f-eq ∙ x
+
+        g' : b0 ≡ b0 → f a0 ≡ b0
+        g' x = f-eq ∙ x
+
+        fg : section f' g'
+        fg b =
+          f' (g' b) ≡⟨ refl ⟩
+          f' (f-eq ∙ b) ≡⟨ refl ⟩
+          sym f-eq ∙ (f-eq ∙ b) ≡⟨ assoc (sym f-eq) f-eq b ⟩
+          (sym f-eq ∙ f-eq) ∙ b ≡⟨ cong (_∙ b) (lCancel f-eq) ⟩
+          refl ∙ b ≡⟨ sym (lUnit b) ⟩
+          b ∎ 
+
+        gf : retract f' g'
+        gf a =
+          g' (f' a) ≡⟨ refl ⟩
+          g' (sym f-eq ∙ a) ≡⟨ refl ⟩
+          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 ∎

src/ThesisWork/Pi3S2/Step1.agda

@@ -4,6 +4,7 @@ module ThesisWork.Pi3S2.Step1 where
 
 open import Agda.Primitive
 open import Cubical.Data.Sigma
+open import Cubical.Data.Nat
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Equiv.Properties
 open import Cubical.Foundations.Isomorphism
@@ -11,8 +12,33 @@ open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.Prelude
 open import Cubical.Homotopy.Loopspace
 
+-- open import ThesisWork.Pi3S2.Lemma4-1-5 renaming (lemma to lemma4-1-5)
+
+fiberF : {l : Level} → {X∙ Y∙ : Pointed l} → (f : X∙ →∙ Y∙) → Pointed l
+fiberF {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) = 
+  fiber f y , x , f-eq
+  -- fiber f y , x , f-eq
+
 arrow∙ : {l : Level} → Type (lsuc l)
 arrow∙ {l} = Σ (Pointed l) (λ X → Σ (Pointed l) (λ Y → X →∙ Y))
 
 F : {l : Level} → arrow∙ {l} → arrow∙ {l}
-F x @ (X , Y , f) = {! fiber   !} , X , {!  fst !}
+F (X∙ @ (X , x) , Y∙ @ (Y , y) , f∙ @ (f , f-eq)) = fiberF f∙ , X∙ , fst , refl
+
+F⁻ : {l : Level} → (n : ℕ) → arrow∙ {l} → arrow∙ {l}
+F⁻ zero x = x
+F⁻ (suc n) x = F (F⁻ n x)
+
+-- Given a pointed map f∙ : X∙ →∙ Y∙, we define its fiber sequence
+-- A : ℕ → Type by Aₙ :≡ p₂(Fⁿ(X , y , f))
+
+A : {l : Level} → {X∙ Y∙ : Pointed l} → (f∙ : X∙ →∙ Y∙) → ℕ → Pointed l
+A {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) n =
+  let it = F⁻ n (X∙ , Y∙ , f∙) in
+  fst (snd it)
+
+f⁻ : {l : Level} → {X∙ Y∙ : Pointed l} → (f∙ : X∙ →∙ Y∙) → (n : ℕ) → fst (A f∙ (suc n)) → fst (A f∙ n)
+f⁻ {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ n a =
+  let it = F⁻ n (X∙ , Y∙ , f∙) in
+  {!  snd (snd it) !}
+  

src/ThesisWork/Pi3S2/SuccStr.agda

@@ -3,7 +3,7 @@
 module ThesisWork.Pi3S2.SuccStr where
 
 open import Cubical.Foundations.Prelude
-open import Data.Nat
+open import Data.Nat using (ℕ ; zero ; suc)
 
 SuccStr : (I : Type) (S : I → I) → (i : I) → (n : ℕ) → I
 SuccStr I S i zero = i 
@@ -17,8 +17,33 @@ module _ where
   ℕ-SuccStr = SuccStr ℕ suc
 
 module _ where
-  open import Data.Integer renaming (suc to zsuc)
+  open import Data.Integer using (ℤ) renaming (suc to zsuc)
 
   -- (ℤ , λ n . n + 1)
   ℤ-SuccStr : (i : ℤ) → (n : ℕ) → ℤ
-  ℤ-SuccStr = SuccStr ℤ zsuc
+  ℤ-SuccStr = SuccStr ℤ zsuc
+
+module _ where
+  open import Data.Fin
+  open import Data.Product
+
+  inc-k-inv : {k : ℕ} → (ℕ × Fin k) → (ℕ × Fin k)
+  inc-k-inv {k} (n , zero) = (suc n) , opposite zero
+  inc-k-inv {k} (n , suc k1) = n , inject₁ k1
+
+  inc : {k : ℕ} → (ℕ × Fin k) → (ℕ × Fin k)
+  inc {k} (n , k1) =
+    let result = inc-k-inv (n , opposite k1) in
+    (fst result) , opposite (snd result)
+
+  _ : inc {k = 3} (5 , fromℕ 2) ≡ (6 , zero)
+  _ = refl
+
+  -- _ : inc {k = 3} (5 , inject₁ (fromℕ 1)) ≡ (6 , zero)
+  -- _ = {!  refl !}
+
+  _ : inc {k = 5} (5 , fromℕ 4) ≡ (6 , zero)
+  _ = refl
+
+  ℕ-k-SuccStr : (k : ℕ) → (ℕ × Fin k) → ℕ → (ℕ × Fin k)
+  ℕ-k-SuccStr k = SuccStr (ℕ × Fin k) inc

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/.gitignore

@@ -1 +1,11 @@
 main.pdf
+*-blx.bib
+*.aux
+*.log
+*.nav
+*.out
+*.run.xml
+*.snm
+*.toc
+*.bbl
+*.blg

talks/2024-grads/Demo.agda

@@ -6,27 +6,19 @@ 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 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 n) = not (isEven n)
 
-lemma : ∀ (n : ℕ) → 2 * suc n + n * (n + 1) ≡ suc n * (suc n + 1)
-lemma = solve-∀
+example : isEven 5 ≡ false
+example = refl
 
-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)
-    ∎
+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 

talks/2024-grads/Demo1.agda

@@ -0,0 +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 Data.Bool
+open import Data.Bool.Properties
+open ≡-Reasoning
+
+isEven : ℕ → Bool
+isEven zero = true
+isEven (suc x) = not (isEven x)
+
+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/Makefile

@@ -1,2 +1,11 @@
+.PHONY: watch clean
+
 main.pdf: main.tex
-	tectonic $<
+	make clean
+	pdflatex main.tex
+
+watch:
+	watchexec -e tex,bib -r --stop-timeout 0 make main.pdf
+
+clean:
+	rm -f *-blx.bib *.aux *.log *.nav *.out *.run.xml *.snm *.toc *.pdf

talks/2024-grads/main.tex

@@ -1,8 +1,19 @@
-\documentclass{beamer}
-\usetheme{Darmstadt}
-\usepackage{bussproofs}
+\documentclass[handout,a4paper]{beamer}
+\useoutertheme{miniframes}
+% \usetheme{Darmstadt}
 
-\setbeameroption{show notes on second screen=right}
+\usepackage[TU,T1]{fontenc}
+% \usepackage{hyperref}
+\usepackage{bussproofs}
+\usepackage{colortbl}
+\usepackage{geometry}
+
+\usepackage[backend=bibtex,style=numeric-comp,sorting=none]{biblatex}
+\addbibresource{references.bib}
+\nocite{*}
+
+% \setbeamercovered{transparent}
+% \setbeameroption{show notes on second screen=right}
 
 \title{Formalizing mathematics with cubical type theory}
 \author{Michael Zhang}
@@ -11,9 +22,22 @@
 
 \begin{document}
 
+\section{Introduction}
+
 \frame{\titlepage}
 
-\section{Theorem prover intro}
+% \begin{frame}
+%   \frametitle{About me}
+
+%   \begin{itemize}
+%     \item Third-year master's student with \textbf{Favonia}
+%     \item Worked several years as a software engineer at Epic, Amazon, Swoop
+%     \item Binary analysis researcher at defense contractor SIFT
+%     \item Previously officer of GopherHack, UMN, SASE
+%   \end{itemize}
+% \end{frame}
+
+\section{Theorem provers}
 
 \begin{frame}
   \frametitle{Intro}
@@ -21,18 +45,20 @@
   \begin{itemize}
     \item Why formalize proofs?
     \note[item]{Why: Would be nice to get computers to check our work for us}
+    \pause
 
     \item What can we formalize?
     \note[item]{What: Program properties, compiler optimizations, correctness}
-    \note[item]{Notably, can NOT prove some things, Rice's theorem}
+    \pause
 
-    \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 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 $$}
+    % \pause
 
-    \item What does the current state of the ecosystem look like?
+    \item What are some existing theorem provers?
     \begin{itemize}
-      \item Coq, Lean, Agda, ...
+      \item Rocq (Coq), Lean, Agda
     \end{itemize}
   \end{itemize}
 \end{frame}
@@ -41,43 +67,594 @@
   \frametitle{Demo}
 \end{frame}
 
-\section{Homotopy type theory}
+\section{Type theory}
 
 \begin{frame}
-  \frametitle{Curry-Howard Isomorphism, or "proofs are programs"}
+  \frametitle{Set theory}
 
-  \begin{tabular}{c|c}
-    Logic & Programming \\
-    \hline
-    c & d \\
-  \end{tabular}
+  \begin{itemize}
+    \item Math is built upon sets
+    \pause
+
+    \item We often operate at a much higher level
+    \pause
+
+    \item Skip the details
+    \pause
+
+    \item We can't do this for mechanized systems!
+  \end{itemize}
+\end{frame}
+
+
+
+\begin{frame}
+  \frametitle{Introducing the type}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.75\textwidth]{images/type.png}
+  \end{figure}
 \end{frame}
 
 \begin{frame}
-  \frametitle{Martin-L{\"o}f type theory}
+  \frametitle{Proofs are programs}
+
+  \begin{table}[]
+    \begin{tabular}{c|c}
+    \hline
+    Logic side                     & Programming side              \\ \hline \hline
+    formula                        & type                          \\ \hline
+    proof                          & term                          \\ \hline
+    formula is true                & type has an element           \\ \hline
+    formula is false               & type does not have an element \\ \hline
+    logical constant $\top$ (truth)     & unit type                     \\ \hline
+    logical constant $\bot$ (falsehood) & empty type                    \\ \hline
+    implication                    & function type                 \\ \hline
+    conjunction                    & product type                  \\ \hline
+    disjunction                    & sum type                      \\ \hline \onslide<+(1)->
+    universal quantification       & dependent product type        \\ \hline
+    existential quantification     & dependent sum type            \\ \hline
+    \end{tabular}
+  \end{table}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Important features of 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:
+    \pause
+    \item Stratified universes: $\mathsf{Type}_0, \mathsf{Type}_1, \mathsf{Type}_2, \dots$
 
+    \pause
+    \item Inductive types, defined by type former, constructors, eliminators, and computation rules
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Important features of Martin-L{\"o}f type theory}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.5\textwidth]{images/nat.png}
+  \end{figure}
+  \pause
+
+  \begin{itemize}
+    \item
+    For example, $\mathbb{N}$ is defined with 2 possible constructors: $\mathsf{zero}$ and $\mathsf{suc}$.
+
+    \begin{columns} 
+      \begin{column}{.3\textwidth}
+        \begin{prooftree}
+          \AxiomC{}
+          \UnaryInfC{$\Gamma \vdash \mathsf{zero} : \mathbb{N}$}
+        \end{prooftree}
+      \end{column}
+      \begin{column}{.3\textwidth}
+        \begin{prooftree}
+          \AxiomC{$\Gamma \vdash n : \mathbb{N}$}
+          \UnaryInfC{$\Gamma \vdash \mathsf{suc}(n) : \mathbb{N}$}
+        \end{prooftree}
+      \end{column}
+    \end{columns}
+
+    \pause
+    \item
+    Elimination rule for $\mathbb{N}$:
     \begin{prooftree}
-      \AxiomC{$ \Gamma \vdash c_0 : C $}
-      \AxiomC{$ \Gamma , x : \mathbb{N} , y : C \vdash c_s : C $}
+      \AxiomC{$ \Gamma \vdash c_z : 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 $}
+      \TrinaryInfC{$ \Gamma \vdash \mathsf{ind}_{\mathbb{N}} (c_z , x . y . c_s , n) : C $}
     \end{prooftree}
+  \end{itemize}
+\end{frame}
 
-    \item \emph{Dependent types}:
-    $$ \mathsf{Vec} : (A : \mathsf{Type}) \rightarrow (n : \mathbb{N}) \rightarrow \mathsf{Type} $$
+\begin{frame}
+  \frametitle{Important features of Martin-L{\"o}f type theory}
+
+  \begin{itemize}
+    \item \emph{Dependent sums}, or $\Sigma$-types
   \end{itemize}
 
-  \footnotetext[1]{This is the non-dependent version of the induction principle}
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.7\textwidth]{images/sigma.png}
+  \end{figure}
+
+  \pause
+  \begin{columns}
+    \begin{column}{.3\textwidth}
+      $$ \mathsf{isEven} : \mathbb{N} \rightarrow \mathsf{Type} $$
+    \end{column}
+    \begin{column}{.3\textwidth}
+      $$ \mathsf{Even} : \sum_{n : \mathbb{N}} \mathsf{isEven}(n) $$
+    \end{column}
+  \end{columns}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Important features of Martin-L{\"o}f type theory}
+
+  \begin{itemize}
+    \item \emph{Dependent functions}, or $\Pi$-types
+    \pause
+    
+    \begin{equation*}
+    \begin{aligned}
+      \mathsf{List} &: \mathsf{Type} \rightarrow \mathsf{Type} \\
+      \onslide<+(1)->
+      \mathsf{Vec} &: \mathsf{Type} \rightarrow \mathbb{N} \rightarrow \mathsf{Type}
+    \end{aligned}
+    \end{equation*}
+
+  \end{itemize}
+
+  \pause
+  $$ \mathsf{append} : \prod_{A : \mathsf{Type}} \left( \prod_{m, n : \mathbb{N}} \left( \mathsf{Vec}(A, m) \rightarrow \mathsf{Vec}(A, n) \rightarrow \mathsf{Vec}(A, m + n) \right) \right) $$
+
+\end{frame}
+
+\begin{frame}
+  \frametitle{Important features of Martin-L{\"o}f type theory}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.5\textwidth]{images/id.png}
+  \end{figure}
+
+  \begin{itemize}
+    \item The identity type, $\mathsf{Id}_A(x, y)$, for some $x, y : A$
+    \pause
+    \item Also written as $x \equiv_A y$, or just $x \equiv y$ if $A$ is obvious
+    \pause
+    \item Single constructor: $\mathsf{refl}_x : \mathsf{Id}_A(x, x)$
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Important features of Martin-L{\"o}f type theory}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.5\textwidth]{images/id2.png}
+  \end{figure}
+
+  \begin{itemize}
+    \item There can be multiple paths between points!
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Homotopy type theory}
+
+  \begin{itemize}
+    \item A homotopy, from algebraic topology, is a way to continuously deform one path into another ($A \times [0, 1] \rightarrow B$)
+
+    \item In type theory, we consider two functions $f, g : A \rightarrow B$ as being homotopic if we can inhabit $h : (x : A) \rightarrow f(x) \equiv g(x)$
+    % \item Note: assume all functions are continuous.
+
+    \begin{figure}
+      \centering
+      \includegraphics[width=0.5\textwidth]{images/homotopy.png}
+    \end{figure}
+
+    \note[item]{Interpret paths between points in a space as the identity type $\mathsf{Id}$}
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Homotopy type theory}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.8\textwidth]{images/paths.png}
+  \end{figure}
+
+  \note[item]{We consider these "paths" to be our identities}
+  \note[item]{The continuousness is important because it means that we can't just connect any two elements, they still have to be constructed uniformly}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Isomorphism}
+
+  \begin{columns}
+    \begin{column}{0.5\textwidth}
+      \begin{itemize}
+        \item A function $f : A \rightarrow B$
+        \item A function $g : B \rightarrow A$
+      \end{itemize}
+    \end{column}
+    \begin{column}{0.5\textwidth}
+      \begin{figure}
+        \centering
+        \includegraphics[width=0.8\textwidth]{images/maps.png}
+      \end{figure}
+    \end{column}
+  \end{columns}
+
+
+  \begin{columns}
+    \begin{column}{0.5\textwidth}
+      \begin{itemize}
+        \item $\prod_{(a: A)} g(f(a)) \equiv a$
+        \item $\prod_{(b: B)} f(g(b)) \equiv b$
+      \end{itemize}
+    \end{column}
+    \begin{column}{0.5\textwidth}
+      \begin{figure}
+        \centering
+        \includegraphics[width=0.8\textwidth]{images/mapsid.png}
+      \end{figure}
+    \end{column}
+  \end{columns}
+
+  \note[item]{Equivalence is sort of like an upgraded isomorphism}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Univalence}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.7\textwidth]{images/ua.png}
+  \end{figure}
+
+  \begin{itemize}
+    \item Equivalences \emph{are} identities
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Univalence}
+
+  \begin{itemize}
+    \item Equivalences \emph{are} identities
+    $$ (A \simeq B) \simeq (A \equiv B) $$
+
+    \note[item]{Essentially, if you can prove a way to go back and forth between $A$ and $B$, then $A$ and $B$ can be identified}
+    \item 
+    Intuitively, if you wanted to use a $B$ where you wanted to use an $A$, just convert it and then convert it back later
+
+    \pause
+    \item Importantly, there can be multiple inhabitants of $A \equiv B$
+    \begin{itemize}
+      \item Booleans! \\ 
+      $\mathsf{ua}(\mathsf{id})$ and $\mathsf{ua}(\mathsf{not})$ are different elements of $\mathsf{Bool} \equiv \mathsf{Bool}$
+    \end{itemize}
+
+    \pause
+    \item
+    Transport allows you to use $A$ and $B$ interchangeably
+  \end{itemize}
+
+    $$ \mathsf{transport} : (P : (X : \mathsf{Type}) \rightarrow \mathsf{Type}) \rightarrow (p : x \equiv_X y) \rightarrow P(x) \rightarrow P(y) $$
+\end{frame}
+
+\begin{frame}
+  \frametitle{Univalence axiom?}
+
+  \begin{itemize}
+    \item Unfortunately, univalence does not compute in Book HoTT
+    \pause
+    \item Assume the functions we want as axioms
+  \end{itemize}
+
+  $$
+    \mathsf{ua} : (A \simeq B) \rightarrow (A \equiv B)
+  $$
+\end{frame}
+
+\begin{frame}
+  \frametitle{Higher inductive types}
+
+  \note[item]{Another way to inject paths into a type}
+
+  \begin{itemize}
+    \item Normally inductive types give us ways to construct \emph{points}
+    \pause
+    \item Higher inductive types give us ways to construct \emph{paths}
+  \end{itemize}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.5\textwidth]{images/zquot.png}
+  \end{figure}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Circle ($S^1$)}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.4\textwidth]{images/s1.png}
+  \end{figure}
+
+  \begin{itemize}
+    \item $\mathsf{base} : S^1$, some arbitrary base point
+    \item $\mathsf{loop} : \mathsf{base} \equiv \mathsf{base}$, a path representing the rest of the circle
+  \end{itemize}
 \end{frame}
 
 \section{Fundamental group of a circle}
 
-\begin{frame} \end{frame}
+\begin{frame}
+  \frametitle{The fundamental group $\pi_1$}
+
+  \begin{itemize}
+    \item One central idea of algebraic topology: identify which spaces are different from each other
+    (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}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.5\textwidth]{images/loopspace.jpg}
+  \end{figure}
+\end{frame}
+
+\begin{frame}
+  \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
+    \pause
+    \item Determining fundamental groups of $n$-spheres is a difficult problem in algebraic topology
+    \pause
+    \item Fortunately, $\pi_1(S^1)$ has a known solution
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{The fundamental group of the circle}
+
+  \begin{itemize}
+    \note[item]{glossing over some details, loop space asks about the point base only}
+    \item Fundamental group asks us about the loops in the circle space
+    \pause
+    \item $\mathsf{base} \equiv \mathsf{base}$ because we don't care about choice of base point
+    \pause
+    \item Some example elements:
+      \begin{itemize}
+        \item ...
+        \item $\mathsf{loop}^{-1} \cdot \mathsf{loop}^{-1}$\
+        \item $\mathsf{loop}^{-1}$
+        \item $\mathsf{refl}$
+        \item $\mathsf{loop}$
+        \item $\mathsf{loop} \cdot \mathsf{loop}$
+        \item ...
+      \end{itemize}
+
+
+    \pause
+    \item The fundamental group of the circle space is the integers
+    $$ \pi_1(S^1) \simeq \mathbb{Z} $$
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{The fundamental group of the circle, core idea}
+
+  \begin{itemize}
+    \item Use a winding helix to represent both!
+  \end{itemize}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.3\textwidth]{images/winding.png}
+  \end{figure}
+\end{frame}
+
+\begin{frame}
+  \frametitle{The fundamental group of the circle, core idea}
+
+  \begin{itemize}
+    \item Problem: we want multiple loopings to map us to different integers.
+  \end{itemize}
+
+  \pause
+
+  \begin{columns}
+    \begin{column}{.45\textwidth}
+      \begin{itemize}
+        \only<-2>{
+          \item Idea: define a custom type family that takes different number of loops to different "rotations" of the integers!
+        }
+        \only<3>{
+          \item Define the encoding:
+            \begin{itemize}
+              \item $\mathsf{code} : S^1 \rightarrow \mathsf{Type}$
+              \item $\mathsf{code}(\mathsf{base}) = \mathbb{Z}$
+              \item $\mathsf{code}(\mathsf{loop}) = \mathsf{ua}(\mathsf{suc})$
+            \end{itemize}
+        }
+      \end{itemize}
+    \end{column}
+    \begin{column}{.55\textwidth}
+  \begin{figure}
+    \centering
+    \includegraphics[width=\textwidth]{images/encoding.png}
+  \end{figure}
+    \end{column}
+  \end{columns}
+\end{frame}
+
+\begin{frame}
+  \frametitle{The fundamental group of the circle, core idea}
+
+  \begin{itemize}
+    \item Need to define the following data to prove the equivalence:
+    $$ (\mathsf{base} \equiv_{S^1} c) \simeq \mathsf{code}(c) $$
+    \pause
+    \item For some $(c : S^1)$ and $(n : \mathbb{N})$ that encodes how many loopings a path to $c$ could take
+      \begin{itemize}
+        \item $ f : (\mathsf{base} \equiv_{S^1} c) \rightarrow \mathsf{code}(c) $
+        \item $ g : \mathsf{code}(c) \rightarrow (\mathsf{base} \equiv_{S^1} c) $
+        \item $ (g \circ f)(p) \equiv \mathsf{id}_{\mathsf{base} \equiv_{S^1} c} $
+        \item $ (f \circ g)(n) \equiv \mathsf{id}_{\mathbb{Z}} $
+      \end{itemize}
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Homotopy type theory proof idea}
+
+  \begin{itemize}
+    \item For $f : (\mathsf{base} \equiv_{S^1} c) \rightarrow \mathsf{code}(c)$, just use the winding map!
+    \item This allows us to turn any loop into an integer
+    \item For some $p : \mathsf{base} \equiv \mathsf{base}$, $\mathsf{transport}^{\mathsf{code}}(p, 0)$ turns 0 into any integer by mapping over the equivalence between integers
+  \end{itemize}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.5\textwidth]{images/encode.png}
+  \end{figure}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Homotopy type theory proof idea}
+
+  \begin{itemize}
+    \item For $g : \mathsf{code}(c) \rightarrow \mathsf{base} \equiv_{S^1} c$,
+    we can iteratively compose $\mathsf{loop}$s to $\mathsf{refl}$ using a function $\mathsf{loop}^n$
+    \begin{itemize}
+      \item $\mathsf{loop}^{-1 + n} = \mathsf{loop}^n \cdot \mathsf{loop}^{-1}$
+      \item $\mathsf{loop}^0 = \mathsf{refl}$
+      \item $\mathsf{loop}^{n + 1} = \mathsf{loop}^n \cdot \mathsf{loop}$
+    \end{itemize}
+
+    \pause
+    \item Then, use this to define $g$
+    \begin{itemize}
+      \item $g(c : \mathsf{code}(\mathsf{base})) = \mathsf{loop}^c$
+      \item $g(c : \mathsf{code}(\mathsf{loop})) : (\mathsf{loop}^c \equiv^{\lambda x \mapsto \mathsf{code}(x) \rightarrow \mathsf{base} \equiv x}_{\mathsf{loop}} \mathsf{loop}^c)$
+      \item This can be defined in two ways
+    \end{itemize}
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Homotopy type theory proof}
+
+  \begin{itemize}
+    \item The homotopies $(g \circ f \equiv \mathsf{id}_{(\mathsf{base} \equiv_{S^1} c)})$ and $(f \circ g \equiv \mathsf{id}_{\mathsf{code}(c)})$ can be proven just by applying path induction and these groupoid laws of paths:
+      \begin{itemize}
+        \item Identity: $(p : x \equiv_A y) \rightarrow p \cdot \mathsf{refl} \equiv p$
+        \item Identity: $(p : x \equiv_A y) \rightarrow \mathsf{refl} \cdot p \equiv p$
+        \item Inverse: $(p : x \equiv_A y) \rightarrow p \cdot p^{-1} \equiv \mathsf{refl}$
+        \item Inverse: $(p : x \equiv_A y) \rightarrow p^{-1} \cdot p \equiv \mathsf{refl}$
+        \item Associativity: $(p : x \equiv_A y) \rightarrow (q : y \equiv_A z) \rightarrow (r : z \equiv_A w) \newline \rightarrow (p \cdot q) \cdot r \equiv p \cdot (q \cdot r)$
+      \end{itemize}
+  \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}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.75\textwidth]{images/composition.png}
+  \end{figure}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Defining $g$ with cubes}
+
+  \begin{figure}
+    \centering
+    \includegraphics[width=0.75\textwidth]{images/decodecube.png}
+  \end{figure}
+\end{frame}
+
+\section{Conclusion}
+
+% \begin{frame}
+%   \frametitle{Other topics in homotopy type theory}
+
+%   \begin{itemize}
+%     \item 
+%   \end{itemize}
+% \end{frame}
+
+\begin{frame}
+  \frametitle{Current work}
+
+  \begin{itemize}
+    \item Re-formalizing results from HoTT book chapters 7 on $n$-types and 8 on homotopy theory
+    \item Re-formalizing results from Floris van Doorn's dissertation on spectral sequences
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Conclusion and references}
+
+  \begin{itemize}
+    \item Code: \url{https://git.mzhang.io/michael/type-theory}
+  \end{itemize}
+
+  \bigskip
+
+  \printbibliography
+\end{frame}
 
 \end{document}

talks/2024-grads/references.bib

@@ -0,0 +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
+}