wip

src/CubicalHott/Example3-6-2.agda

@@ -7,4 +7,4 @@ open import Cubical.Foundations.Prelude
 example : {A : Type} → {B : A → Type}
   → ((x : A) → isProp (B x))
   → isProp ((x : A) → B x)
-example B-x-prop x y = λ i z → B-x-prop {!   !} {!   !} {!   !} i
+example B-x-prop fx fy = λ i z → B-x-prop z (B-x-prop z (fx z) (fy z) i) (B-x-prop z (fx z) (fy z) i) i

src/CubicalHott/Lemma3-11-3.agda

@@ -2,4 +2,4 @@
 
 module CubicalHott.Lemma3-11-3 where
 
-open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Prelude

src/CubicalHott/Lemma3-11-4.agda

@@ -3,13 +3,17 @@
 module CubicalHott.Lemma3-11-4 where
 
 open import Cubical.Foundations.Prelude
+open import CubicalHott.Example3-6-2 renaming (example to example3-6-2)
 
 lemma : {A : Type} → isProp (isContr A)
 lemma {A} A-contr-x @ (x , px) (y , py) i =
   let A-is-set = isProp→isSet (isContr→isProp A-contr-x) in
-  -- px y i ≡ z
-  -- ———— Boundary (wanted) —————————————————————————————————————
-  -- i = i0 ⊢ px z
-  -- i = i1 ⊢ py z
-  px y i , λ z j → {!   !}
+  px y i , goal i where
+    helper1 : isProp ((z : A) → px y i ≡ z)
+    helper1 = example3-6-2 (λ x → isContr→isProp {!   !})
+
+    goal : PathP (λ i → (z : A) → px y i ≡ z) px py
+    goal i z = {! helper1  !}
+
+
   -- λ y' j → isProp→isSet (isContr→isProp A-contr-x) (px y i) y' {!   !} {!   !} j i

src/CubicalHott/Theorem7-1-10.agda

@@ -9,6 +9,6 @@ open import Cubical.Data.Nat
 z = isContr
 
 theorem : {X : Type} → (n : ℕ) → isProp (isOfHLevel n X)
-theorem zero x y i = snd x (fst y) i , {!   !}
+theorem zero = {!   !}
 theorem (suc zero) x y = {!   !} 
 theorem (suc (suc n)) x y = {!   !}