From fe2eedeed2980759a13b69f6e6ea27e4f2fbb69e Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Wed, 2 Oct 2024 18:42:04 -0500 Subject: [PATCH] agda (Agda version 2.7.0) hangs on src/CubicalHott/Theorem8-1.agda --- src/CubicalHott/Definition8-1-6.agda | 107 ++++++++++++++++---------- src/CubicalHott/Lemma8-3-1.agda | 3 +- src/CubicalHott/Theorem8-1-part1.agda | 2 +- src/CubicalHott/Theorem8-1.agda | 17 +++- 4 files changed, 84 insertions(+), 45 deletions(-) diff --git a/src/CubicalHott/Definition8-1-6.agda b/src/CubicalHott/Definition8-1-6.agda index 4e201d8..8ae813d 100644 --- a/src/CubicalHott/Definition8-1-6.agda +++ b/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 + + \ No newline at end of file diff --git a/src/CubicalHott/Lemma8-3-1.agda b/src/CubicalHott/Lemma8-3-1.agda index c356c0d..a43c5ef 100644 --- a/src/CubicalHott/Lemma8-3-1.agda +++ b/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 : ℕ) → \ No newline at end of file +lemma A a n x k = {! !} where \ No newline at end of file diff --git a/src/CubicalHott/Theorem8-1-part1.agda b/src/CubicalHott/Theorem8-1-part1.agda index 517e644..860e026 100644 --- a/src/CubicalHott/Theorem8-1-part1.agda +++ b/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) \ No newline at end of file +encode x p = subst code p (pos zero) \ No newline at end of file diff --git a/src/CubicalHott/Theorem8-1.agda b/src/CubicalHott/Theorem8-1.agda index 52aedca..48f6f3a 100644 --- a/src/CubicalHott/Theorem8-1.agda +++ b/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