more proofs

src/CubicalHott/Lemma2-3-10.agda

@@ -5,7 +5,8 @@ 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}
+lemma : {A B : Type} {x y : A}
+  → (f : A → B) → (P : B → Type)
   → (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
+lemma f P p u i = transp (λ i → P (f (p i))) i0 u

src/CubicalHott/Theorem8-1.agda

@@ -21,21 +21,25 @@ 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≡ : ℤ ≡ ℤ
+suc≡ = ua suc≃
+
 code : S¹ → Type
 code base = ℤ
-code (loop i) = ua suc≃ i where
-  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
+code (loop i) = suc≡ i
 
 loop⁻ : ℤ → base ≡ base
 loop⁻ (+_ zero) = refl
@@ -47,8 +51,9 @@ loop⁻ (-[1+_] (nsuc n)) = loop⁻ -[1+ n ] ∙ (sym loop)
 
 lemma8-1-2a : (x : ℤ) → subst code loop x ≡ suc x
 lemma8-1-2a x =
-  subst code loop x ≡⟨ lemma2-3-10 {!   !} {!   !} ⟩
-  subst (idfun _) (cong code loop) 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 ∎
 
 -- Definition 8.1.5
@@ -59,8 +64,14 @@ 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 = {!   !}
+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 {!   !}
 
 -- Corollary 8.1.10
               

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

@@ -40,7 +40,7 @@ Prove the propositional computation law for `J`:
 ```agda
 JRefl : {A : Type ℓ} {x : A} (P : (z : A) → x ≡ z → Type ℓ'')
   (d : P x refl) → J P d refl ≡ d
-JRefl P d i = {!    !}
+JRefl {x = x} P d i = transp (λ _ → P x refl) i d
 ```
 
 ### Exercise 2 (★★)
@@ -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} p i = {!!}
+fromPathP {A = A} {x = x} p i = {!   !}
 ```
 
 ### Exercise 3 (★★★)
@@ -122,5 +122,17 @@ This requires drawing a cube (yes, an actual 3D one)!
 
 ```agda
 isPropIsContr : {A : Type ℓ} → isProp (isContr A)
-isPropIsContr (c0 , h0) (c1 , h1) j = {!!} 
+isPropIsContr (c0 , h0) (c1 , h1) j = sym (h1 c0) j , λ y i →
+    -- A
+    -- ———— Boundary (wanted) —————————————————————————————————————
+    -- i = i0 ⊢ h1 c0 (~ j)
+    -- i = i1 ⊢ y
+    -- j = i0 ⊢ h0 y i
+    -- j = i1 ⊢ h1 y i
+  let u = λ k → λ where
+    (i = i0) → h1 c0 (~ j ∧ k)
+    (i = i1) → y
+    (j = i0) → {! h0 y i  !}
+    (j = i1) → {!   !}
+  in hcomp u {!   !}
 ```

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

@@ -43,7 +43,15 @@ Hint: one hcomp should suffice. Use `comp-filler` and connections
 
 ```agda
 lUnit : {A : Type ℓ} {x y : A} (p : x ≡ y) → refl ∙ p ≡ p
-lUnit = {!!}
+lUnit {x = x} {y = y} p i j =
+  let u = λ k → λ where
+    (i = i0) → hfill (λ k → λ { (j = i0) → x ; (j = i1) → p k }) (inS x) k
+    (i = i1) → p j
+    (j = i0) → x
+    (j = i1) → p (i ∨ k)
+  in hcomp u (p (i ∧ j))
+
+cf = comp-filler
 
 ```
 ### (b)
@@ -53,15 +61,18 @@ Hint: use (almost) the exact same hcomp.
 
 ```agda
 rUnit : {A : Type ℓ} {x y : A} (p : x ≡ y) → p ∙ refl ≡ p
-rUnit = {!!}
+rUnit {x = x} {y = y} p i j =
+  let u = λ k → λ where
+    (i = i0) → hfill (λ k → λ { (j = i0) → x ; (j = i1) → y }) (inS (p j)) k
+    (i = i1) → p (j ∧ k)
+    (j = i0) → x
+    (j = i1) → p (k ∨ ~ i)
+  in hcomp u (p (j ∧ ~ i))
 
 -- uncomment to see if it type-checks
 
-{-
 rUnit≡lUnit : ∀ {ℓ} {A : Type ℓ} {x : A} → rUnit (refl {x = x}) ≡ lUnit refl
 rUnit≡lUnit = refl
--}
-
 ```
 
 
@@ -73,8 +84,20 @@ Hint: one hcomp should suffice. This one can be done without connections
 ```agda
 assoc : {A : Type ℓ} {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w)
   → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
-assoc = {!!}
-
+assoc {ℓ} {A} {x} {y} {z} {w} p q r i j =
+-- A
+-- ———— Boundary (wanted) —————————————————————————————————————
+-- j = i0 ⊢ x
+-- j = i1 ⊢ w
+-- i = i0 ⊢ hcomp (λ { j₁ (j = i0) → x ; j₁ (j = i1) → (q ∙ r) j₁ }) --          (p j)
+-- i = i1 ⊢ hcomp (λ { j₁ (j = i0) → x ; j₁ (j = i1) → r j₁ }) --          ((p ∙ q) j)
+  let u = λ k → λ where
+    (i = i0) → hfill (λ k → λ { (j = i0) → x ; (j = i1) → (q ∙ r) k }) (inS (p j)) k
+    (i = i1) → hfill (λ k → λ { (j = i0) → x ; (j = i1) → r k }) (inS ((p ∙ q) j)) k
+    (j = i0) → x
+    (j = i1) → hfill (λ i → λ { (k = i0) → w ; (k = i1) → q i }) (inS {! r k  !}) {! i  !}
+  in hcomp u {!   !}
+    -- (hfill (λ i → λ { (j = i0) → x ; (j = i1) → q i }) (inS (p j)) i)
 ```
 
 ### Exercise 3 (Master class in connections) (🌶)