agda (Agda version 2.7.0) hangs on src/CubicalHott/Theorem8-1.agda

src/CubicalHott/Definition8-1-6.agda

@@ -17,7 +17,7 @@ open import CubicalHott.Theorem8-1-part1
 -- Definition 8.1.6
 
 lemma1 : (x : ℤ) → loop⁻ (predℤ x) ∙ loop ≡ loop⁻ x
-lemma1 (pos zero) = rCancel (sym loop)
+lemma1 (pos zero) = lCancel loop
 lemma1 (pos (nsuc n)) = refl
 lemma1 (negsuc zero) = sym (assoc (sym loop) (sym loop) loop) ∙ cong (λ p → sym loop ∙ p) (lCancel loop) ∙ sym (rUnit (sym loop))
 lemma1 (negsuc (nsuc n)) =
@@ -25,49 +25,76 @@ lemma1 (negsuc (nsuc n)) =
   ∙ sym (assoc (loop⁻ (negsuc n)) (sym loop) (sym loop ∙ loop))
   ∙ cong (λ p → loop⁻ (negsuc n) ∙ p) (cong (λ p → sym loop ∙ p) (lCancel loop) ∙ sym (rUnit (sym loop)))
 
+lemma2 : (x : ℤ) → loop⁻ (sucℤ x) ∙ sym loop ≡ loop⁻ x
+lemma2 (pos zero) = sym (assoc refl loop (sym loop)) ∙ cong (refl ∙_) (rCancel loop) ∙ sym (rUnit refl)
+lemma2 (pos (nsuc n)) =
+  sym (assoc (loop⁻ (pos n) ∙ loop) loop (sym loop))
+  ∙ cong ((loop⁻ (pos n) ∙ loop) ∙_) (rCancel loop)
+  ∙ sym (rUnit (loop⁻ (pos n) ∙ loop))
+  ∙ cong (_∙ loop) (rUnit (loop⁻ (pos n)) ∙ cong (loop⁻ (pos n) ∙_) (sym (rCancel loop)) ∙ assoc (loop⁻ (pos n)) loop (sym loop))
+  ∙ cong (_∙ loop) (lemma2 (pos n))
+lemma2 (negsuc zero) = sym (lUnit (sym loop))
+lemma2 (negsuc (nsuc n)) = refl
+-- lemma2 x = cong (λ n → loop⁻ n ∙ loop) (sym (predSuc x)) ∙ lemma1 (sucℤ x)
+
 decode : (x : S¹) → code x → base ≡ x
 decode base c = loop⁻ c
-decode (loop i) c j = {!   !} where
-  -- S¹
-  -- ———— Boundary (wanted) —————————————————————————————————————
-  -- j = i0 ⊢ base
-  -- j = i1 ⊢ loop i
-  -- i = i0 ⊢ loop⁻ c j
-  -- i = i1 ⊢ loop⁻ c j
+decode (loop i) c j =
+  let u = λ k → λ where
+    (i = i0) → 
+      -- S¹
+      -- ———— Boundary (wanted) —————————————————————————————————————
+      -- k = i0 ⊢ loop⁻ (sucℤ c) j
+      -- k = i1 ⊢ loop⁻ c j
+      -- j = i0 ⊢ base
+      -- j = i1 ⊢ loop (~ k)
+      (compPath-filler (loop⁻ (sucℤ c)) (sym loop) ▷ lemma2 c) k j
+    (i = i1) → loop⁻ c j
+    (j = i0) → base
+    (j = i1) → loop (i ∨ ~ k)
+  in hcomp u (loop⁻ (unglue (i ∨ ~ i) c) j)
+  where
+    -- S¹
+    -- ———— Boundary (wanted) —————————————————————————————————————
+    -- j = i0 ⊢ base
+    -- j = i1 ⊢ loop i
+    -- i = i0 ⊢ loop⁻ c j
+    -- i = i1 ⊢ loop⁻ c j
 
-  path : subst (λ x' → code x' → base ≡ x') loop loop⁻ ≡ loop⁻
-  path =
-      subst (λ x' → (code x' → base ≡ x')) loop loop⁻
-    ≡⟨⟩
-      subst (λ x' → base ≡ x') loop ∘ loop⁻ ∘ subst code (sym loop)
-    ≡⟨⟩
-      (λ p → p ∙ loop) ∘ loop⁻ ∘ subst code (sym loop)
-    ≡⟨⟩
-      (λ p → p ∙ loop) ∘ (loop⁻ ∘ predℤ)
-    ≡⟨⟩
-      (λ n → loop⁻ (predℤ n) ∙ loop)
-    ≡⟨ funExt lemma1 ⟩
-      loop⁻
-    ∎
+    path : subst (λ x' → code x' → base ≡ x') loop loop⁻ ≡ loop⁻
+    path =
+        subst (λ x' → (code x' → base ≡ x')) loop loop⁻
+      ≡⟨⟩
+        subst (λ x' → base ≡ x') loop ∘ loop⁻ ∘ subst code (sym loop)
+      ≡⟨⟩
+        (λ p → p ∙ loop) ∘ loop⁻ ∘ subst code (sym loop)
+      ≡⟨⟩
+        (λ p → p ∙ loop) ∘ (loop⁻ ∘ predℤ)
+      ≡⟨⟩
+        (λ n → loop⁻ (predℤ n) ∙ loop)
+      ≡⟨ funExt lemma1 ⟩
+        loop⁻
+      ∎
 
-  path2 : PathP (λ i → code (loop i) → base ≡ loop i) loop⁻ loop⁻
-  path2 = toPathP path
+    path2 : PathP (λ i → code (loop i) → base ≡ loop i) loop⁻ loop⁻
+    path2 = toPathP path
 
-  n : ℤ
-  n = unglue (i ∨ ~ i) c
+    n : ℤ
+    n = unglue (i ∨ ~ i) c
 
-  -- we are trying to prove that loop⁻ c j ≡ loop⁻ c j
-  -- but on one side it's refl_base, and on the other, it's loop i
-  -- let
-  --   bottomFace = let u = λ j → λ where
-  --       (i = i0) → {!   !}
-  --       (i = i1) → {!   !}
-  --     in hfill u (inS {!   !}) {! j  !}
-
-  --   u = λ k → λ where
-  --     (i = i0) → {!   !}
-  --     (i = i1) → loop⁻ c j
-  --     (j = i0) → base
-  --     (j = i1) → loop (i ∨ ~ k)
-  -- in hcomp u bottomFace
+    -- we are trying to prove that loop⁻ c j ≡ loop⁻ c j
+    -- but on one side it's refl_base, and on the other, it's loop i
+    -- let
+    --   bottomFace = let u = λ j → λ where
+    --       (i = i0) → {!   !}
+    --       (i = i1) → {!   !}
+    --     in hfill u (inS {!   !}) {! j  !}
 
+    --   u = λ k → λ where
+    --     (i = i0) → {!   !}
+    --     (i = i1) → loop⁻ c j
+    --     (j = i0) → base
+    --     (j = i1) → loop (i ∨ ~ k)
+    -- in hcomp u bottomFace
+ 
+ 

src/CubicalHott/Lemma8-3-1.agda

@@ -12,5 +12,4 @@ open import Cubical.Homotopy.Loopspace
 
 lemma : (A : Type) → (a : A)
   → (n : ℕ) → hLevelTrunc n A → (k : ℕ) → π (k + n) (A , a) ≡ Unit
-lemma A a n x k = {!   !} where
-  lemma1 : (n : ℕ) → 
+lemma A a n x k = {!   !} where

src/CubicalHott/Theorem8-1-part1.agda

@@ -58,4 +58,4 @@ lemma8-1-2a x =
 -- Definition 8.1.5
 
 encode : (x : S¹) → base ≡ x → code x
-encode s p = subst code p (pos zero)
+encode x p = subst code p (pos zero)

src/CubicalHott/Theorem8-1.agda

@@ -13,7 +13,7 @@ open import Cubical.Foundations.Univalence
 open import Cubical.HITs.S1 hiding (encode; decode)
 open import Cubical.HITs.SetTruncation
 open import Cubical.Homotopy.Loopspace
-open import Cubical.Data.Nat hiding (pred; _+_) renaming (suc to nsuc)
+open import Cubical.Data.Nat hiding (_+_) renaming (suc to nsuc)
 open import Cubical.Data.Int
 -- open import Cubical.Data.Int.Base
 
@@ -21,11 +21,24 @@ open import Cubical.Data.Int
 open import CubicalHott.Theorem8-1-part1
 open import CubicalHott.Definition8-1-6
 
+-- Lemma 8.1.7
+
+decode-encode : (x : S¹) → (p : base ≡ x) → decode x (encode x p) ≡ p
+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 = {!   !}
 
 -- Theorem 8.1.9
 
 theorem8-1-9 : (x : S¹) → ((base ≡ x) ≃ code x)
-theorem8-1-9 x = isoToEquiv (iso (encode x) (decode x) {!   !} {!   !})
+theorem8-1-9 x = isoToEquiv (iso (encode x) (decode x) {! decode-encode x  !} (decode-encode x))
 
 -- Corollary 8.1.10