wip

journals/2024_09_26.md

@@ -0,0 +1,3 @@
+- asdf
+- asdf $asdf$
+-

src/CubicalHott/Lemma2-3-10.agda

@@ -0,0 +1,11 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma2-3-10 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+
+lemma : {A B : Type} {f : A → B} {P : B → Type} {x y : A}
+  → (p : x ≡ y) → (u : P (f x))
+  → subst (P ∘ f) p u ≡ subst P (cong f p) u
+lemma {f = f} {P = P} p u i = transp (λ i → P (f (p i))) i0 u

src/CubicalHott/Theorem8-1.agda

@@ -6,12 +6,15 @@ open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
 open import Cubical.Foundations.Univalence
 open import Cubical.HITs.S1 hiding (encode; decode)
 open import Cubical.Homotopy.Loopspace
-open import Data.Nat hiding (pred; _+_) renaming (suc to nsuc)
+open import Cubical.Data.Nat hiding (pred; _+_) renaming (suc to nsuc)
 open import Data.Integer
 
+open import CubicalHott.Lemma2-3-10 renaming (lemma to lemma2-3-10)
+
 private
   variable
     l : Level
@@ -34,10 +37,19 @@ code (loop i) = ua suc≃ i where
     ret (-[1+_] zero) = refl
     ret (-[1+_] (nsuc n)) = refl
 
+loop⁻ : ℤ → base ≡ base
+loop⁻ (+_ zero) = refl
+loop⁻ +[1+ n ] = loop⁻ (+ n) ∙ loop
+loop⁻ (-[1+_] zero) = loop⁻ (+ zero) ∙ (sym loop)
+loop⁻ (-[1+_] (nsuc n)) = loop⁻ -[1+ n ] ∙ (sym loop)
+
 -- Lemma 8.1.2
 
 lemma8-1-2a : (x : ℤ) → subst code loop x ≡ suc x
-lemma8-1-2a x = {!   !}
+lemma8-1-2a x =
+  subst code loop x ≡⟨ lemma2-3-10 {!   !} {!   !} ⟩
+  subst (idfun _) (cong code loop) x ≡⟨ {!   !} ⟩
+  suc x ∎
 
 -- Definition 8.1.5
 
@@ -47,7 +59,9 @@ encode s p = subst code p +0
 -- Definition 8.1.6
 
 decode : (x : S¹) → code x → base ≡ x
+decode base c = refl
+decode (loop i) c = {!   !}
 
 -- Corollary 8.1.10
-          
+              
 corollary8-1-10 : Ω (S¹ , base) ≃∙ ℤ , +0