From 78fe433b0d3ef28e9176397c866d4f1d1a9665c8 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Wed, 2 Oct 2024 20:32:00 -0500
Subject: [PATCH] complete this for now

---
 src/CubicalHott/Theorem8-1-part1.agda |  6 +++++
 src/CubicalHott/Theorem8-1.agda       | 39 ++++++++++++++++++++-------
 2 files changed, 36 insertions(+), 9 deletions(-)

diff --git a/src/CubicalHott/Theorem8-1-part1.agda b/src/CubicalHott/Theorem8-1-part1.agda
index 860e026..5141b88 100644
--- a/src/CubicalHott/Theorem8-1-part1.agda
+++ b/src/CubicalHott/Theorem8-1-part1.agda
@@ -55,6 +55,12 @@ lemma8-1-2a x =
   subst (idfun Type) suc≡ x ≡⟨⟩
   sucℤ x ∎
 
+lemma8-1-2b : (x : ℤ) → subst code (sym loop) x ≡ predℤ x
+lemma8-1-2b x =
+  subst code (sym loop) x ≡⟨ lemma2-3-10 (idfun S¹) code (sym loop) x ⟩
+  subst (idfun Type) (cong code (sym loop)) x ≡⟨⟩
+  predℤ x ∎
+
 -- Definition 8.1.5
 
 encode : (x : S¹) → base ≡ x → code x
diff --git a/src/CubicalHott/Theorem8-1.agda b/src/CubicalHott/Theorem8-1.agda
index 48f6f3a..103002f 100644
--- a/src/CubicalHott/Theorem8-1.agda
+++ b/src/CubicalHott/Theorem8-1.agda
@@ -15,6 +15,7 @@ open import Cubical.HITs.SetTruncation
 open import Cubical.Homotopy.Loopspace
 open import Cubical.Data.Nat hiding (_+_) renaming (suc to nsuc)
 open import Cubical.Data.Int
+open import Data.Empty
 -- open import Cubical.Data.Int.Base
 
 -- open import CubicalHott.Lemma2-3-10 renaming (lemma to lemma2-3-10)
@@ -28,22 +29,42 @@ decode-encode x p = J (λ x' p' → decode x' (encode x' p') ≡ p') refl p
 
 -- Lemma 8.1.8
 
-encode-decode : (x : S¹) → (c : code x) → encode x (decode x c) ≡ c
-encode-decode base (pos zero) = refl
-encode-decode base (pos (nsuc n)) = {!   !} ∙ cong sucℤ (encode-decode base (pos n))
-encode-decode base (negsuc zero) = refl
-encode-decode base (negsuc (nsuc n)) = {!   !}
-encode-decode (loop i) c = {!   !}
+encode-decode-base : (c : ℤ) → encode base (decode base c) ≡ c
+encode-decode-base (pos n) = pos-case n where
+  pos-case : (n : ℕ) → encode base (loop⁻ (pos n)) ≡ pos n
+  pos-case zero = refl
+  pos-case (nsuc n) =
+    encode base (loop⁻ (pos n) ∙ loop) ≡⟨⟩
+    subst code (loop⁻ (pos n) ∙ loop) (pos zero) ≡⟨⟩
+    subst code loop (subst code (loop⁻ (pos n)) (pos zero)) ≡⟨ lemma8-1-2a ((subst code (loop⁻ (pos n)) (pos zero))) ⟩
+    sucℤ (subst code (loop⁻ (pos n)) (pos zero)) ≡⟨ cong sucℤ (pos-case n) ⟩
+    pos (nsuc n) ∎
+encode-decode-base (negsuc n) = neg-case n where
+  neg-case : (n : ℕ) → encode base (loop⁻ (negsuc n)) ≡ negsuc n
+  neg-case zero = refl
+  neg-case (nsuc n) =
+    encode base (loop⁻ (negsuc n) ∙ sym loop) ≡⟨⟩
+    subst code (loop⁻ (negsuc n) ∙ sym loop) (pos zero) ≡⟨⟩
+    subst code (sym loop) (subst code (loop⁻ (negsuc n)) (pos zero)) ≡⟨ lemma8-1-2b (subst code (loop⁻ (negsuc n)) (pos zero)) ⟩
+    predℤ (subst code (loop⁻ (negsuc n)) (pos zero)) ≡⟨ cong predℤ (neg-case n) ⟩
+    negsuc (nsuc n) ∎
+
+-- encode-decode : (x : S¹) → (c : code x) → encode x (decode x c) ≡ c
+-- encode-decode (loop i) c = {!   !} -- encode (loop i) (decode (loop i) c) ≡ c
 
 -- Theorem 8.1.9
 
-theorem8-1-9 : (x : S¹) → ((base ≡ x) ≃ code x)
-theorem8-1-9 x = isoToEquiv (iso (encode x) (decode x) {! decode-encode x  !} (decode-encode x))
+-- theorem8-1-9 : (x : S¹) → ((base ≡ x) ≃ code x)
+-- theorem8-1-9 x = isoToEquiv (iso (encode x) (decode x) (encode-decode x) (decode-encode x))
+
+cheated-theorem-8-1-9 : (base ≡ base) ≃ ℤ
+cheated-theorem-8-1-9 = isoToEquiv (iso (encode base) (decode base) encode-decode-base (decode-encode base))
 
 -- Corollary 8.1.10
               
 corollary8-1-10 : Ω (S¹ , base) ≃∙ ℤ , pos zero
-corollary8-1-10 = theorem8-1-9 base , refl
+corollary8-1-10 = cheated-theorem-8-1-9 , refl
+-- corollary8-1-10 = theorem8-1-9 base , refl
 
 -- Corollary 8.1.11