wip

src/CubicalHott/Definition8-5-4.agda

@@ -0,0 +1,17 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Definition8-5-4 where
+
+open import Agda.Primitive
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Sigma
+
+record H-Space (A : Type) : Type where
+  field
+    e : A
+    μ : A → A → A
+    
+    left : (a : A) → μ e a ≡ a
+    right : (a : A) → μ a e ≡ a
+
+open H-Space public

src/CubicalHott/Lemma8-5-5.agda

@@ -0,0 +1,17 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma8-5-5 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import CubicalHott.Definition8-5-4
+
+lemma : {A : Type} → (H : H-Space A) → (a : A) → isEquiv (λ e → (H-Space.μ H) a e)
+lemma {A} H a = isoToIsEquiv (iso f g {!   !} {!   !}) where
+  f : A → A
+  f e = (H-Space.μ H) a e
+
+  g : A → A
+
+

src/CubicalHott/Theorem7-1-11.agda

@@ -0,0 +1,40 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem7-1-11 where
+
+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.Foundations.Univalence
+open import Cubical.Data.Nat
+open import Data.Unit
+
+lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n)
+lemma zero (A , a , Acontr) (B , b , Bcontr) i = G , g , {!   !} where
+  -- G : A ≡ B
+  -- G = ua (isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr))
+
+  -- g : PathP (λ i → G i) a b
+  -- g = {!   !}
+
+  -- contr : Acontr ≡ Bcontr
+
+  eqv1 : A ≃ B
+  eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr)
+
+  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
+
+  contr : (y : G) → g ≡ y
+  contr y 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

@@ -0,0 +1,45 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem7-1-4 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Homotopy.Base
+open import Cubical.Data.Nat
+
+theorem : {X Y : Type}
+  → (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 =
+  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 =
+  {!   !} where
+    ε : (p ∘ s) ∼ idfun Y
+    
+
+  -- -- X is h-level (n+2)
+  -- -- If X is h-level (n+1), then Y is h-level (n+1)
+  -- theorem f (cong p') z (suc n) xOfHLevel where
+    -- f : p' a ≡ p' b → a ≡ b
+    -- f = λ q → sym (r a) ∙ cong p q ∙ r b
+
+    -- z : retract (λ q i → p' (q i)) f
+    -- z q =
+    --   f (λ i → p' (q i)) ≡⟨⟩
+    --   sym (r a) ∙ cong p (λ i → p' (q i)) ∙ r b ≡⟨ {!   !} ⟩
+    --   sym (r a) ∙ cong p (λ i → p' (q i)) ∙ r b ≡⟨ {!   !} ⟩
+    --   q ∎
+
+    -- xOfHLevel = xHlevel (p' a) (p' b)
+

src/CubicalHott/Theorem8-1.agda

@@ -5,13 +5,17 @@ module CubicalHott.Theorem8-1 where
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Prelude
+open import Cubical.Homotopy.Group.Base
 open import Cubical.Foundations.Function
 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 Data.Integer
+open import Cubical.Data.Int
+open import Cubical.Data.Int.Base
 
 open import CubicalHott.Lemma2-3-10 renaming (lemma to lemma2-3-10)
 
@@ -22,17 +26,18 @@ private
 -- Definition 8.1.1
 
 suc≃ : ℤ ≃ ℤ
-suc≃ = isoToEquiv (iso suc pred sec ret) where
-  sec : section suc pred
-  sec (+_ zero) = refl
-  sec +[1+ n ] = refl
-  sec (-[1+_] zero) = refl
-  sec (-[1+_] (nsuc n)) = refl
-  ret : retract suc pred
-  ret (+_ zero) = refl
-  ret +[1+ n ] = refl
-  ret (-[1+_] zero) = refl
-  ret (-[1+_] (nsuc n)) = refl
+suc≃ = isoToEquiv (iso sucℤ predℤ sec ret) where
+  sec : section sucℤ predℤ
+  sec (pos zero) = refl
+  sec (pos (nsuc n)) = refl
+  sec (negsuc zero) = refl
+  sec (negsuc (nsuc n)) = refl
+
+  ret : retract sucℤ predℤ
+  ret (pos zero) = refl
+  ret (pos (nsuc n)) = refl
+  ret (negsuc zero) = refl
+  ret (negsuc (nsuc n)) = refl
 
 suc≡ : ℤ ≡ ℤ
 suc≡ = ua suc≃
@@ -42,37 +47,85 @@ code base = ℤ
 code (loop i) = suc≡ i
 
 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)
+loop⁻ (pos zero) = refl
+loop⁻ (pos (nsuc n)) = loop⁻ (pos n) ∙ loop
+loop⁻ (negsuc zero) = sym loop
+loop⁻ (negsuc (nsuc n)) = loop⁻ (negsuc n) ∙ sym loop
 
 -- Lemma 8.1.2
 
-lemma8-1-2a : (x : ℤ) → subst code loop x ≡ suc x
+lemma8-1-2a : (x : ℤ) → subst code loop x ≡ sucℤ x
 lemma8-1-2a x =
   subst code loop x ≡⟨ lemma2-3-10 (idfun S¹) code loop x ⟩
   subst (idfun Type) (cong code loop) x ≡⟨⟩
   subst (idfun Type) suc≡ x ≡⟨⟩
-  suc x ∎
+  sucℤ x ∎
 
 -- Definition 8.1.5
 
 encode : (x : S¹) → base ≡ x → code x
-encode s p = subst code p +0
+encode s p = subst code p (pos zero)
 
 -- Definition 8.1.6
 
+lemma1 : (x : ℤ) → loop⁻ (predℤ x) ∙ loop ≡ loop⁻ x
+lemma1 (pos zero) = rCancel (sym loop)
+lemma1 (pos (nsuc n)) = refl
+lemma1 (negsuc zero) =
+  sym (assoc ? ? ?)
+  ∙ cong (λ p → sym loop ∙ p) (lCancel ?)
+  ∙ sym (rUnit (sym loop))
+lemma1 (negsuc (nsuc n)) = {! refl  !}
+
 decode : (x : S¹) → code x → base ≡ x
 decode base c = loop⁻ c
-decode (loop i) c j =
-  let u = λ k → λ where
-    (i = i0) → {!   !}
-    (i = i1) → loop⁻ c j
-    (j = i0) → base
-    (j = i1) → loop (i ∨ ~ k)
-  in hcomp u {!   !}
+decode (loop i) c j = path j (unglue (~ i ∨ i) c) {! i  !} where
+
+  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⁻
+    ∎
+  -- 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
+
+-- Theorem 8.1.9
+
+theorem8-1-9 : (x : S¹) → ((base ≡ x) ≃ code x)
+theorem8-1-9 x = isoToEquiv (iso (encode x) (decode x) {!   !} {!   !})
 
 -- Corollary 8.1.10
               
-corollary8-1-10 : Ω (S¹ , base) ≃∙ ℤ , +0
+corollary8-1-10 : Ω (S¹ , base) ≃∙ ℤ , pos zero
+corollary8-1-10 = theorem8-1-9 base , refl
+
+-- Corollary 8.1.11
+
+corollary8-1-11 : π 1 (S¹ , base) ≡ ℤ
+corollary8-1-11 =
+  π 1 (S¹ , base) ≡⟨⟩
+  ∥ typ (Ω (S¹ , base)) ∥₂ ≡⟨⟩
+  ∥ base ≡ base ∥₂ ≡⟨ cong ∥_∥₂ (ua (fst corollary8-1-10)) ⟩
+  ∥ ℤ ∥₂ ≡⟨ setTruncIdempotent isSetℤ ⟩
+  ℤ ∎ 

src/HoTTEST/Agda/Cubical/Exercises8.lagda.md

@@ -58,7 +58,7 @@ transport computes away at `i = i1`.
 ```agda
 fromPathP : {A : I → Type ℓ} {x : A i0} {y : A i1} →
   PathP A x y → transport (λ i → A i) x ≡ y
-fromPathP {A = A} {x = x} p i = {!   !}
+fromPathP {A = A} {x = x} p i = transp (λ j → A (i ∨ j)) i (p i)
 ```
 
 ### Exercise 3 (★★★)
@@ -87,9 +87,9 @@ toPathP : {A : I → Type ℓ} {x : A i0} {y : A i1} →
   transport (λ i → A i) x ≡ y → PathP A x y
 toPathP {A = A} {x = x} p i =
   hcomp
-    (λ {j (i = i0) → {!!} ;
-        j (i = i1) → {!!} })
-   {!!}
+    (λ {j (i = i0) → x ;
+        j (i = i1) → p i })
+   {!   !}
 ```
 
 ### Exercise 4 (★)