From d15eefb62589c3f466c1b58502ee6a2b28934fed Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Sat, 19 Oct 2024 16:56:23 -0500
Subject: [PATCH] wip

---
 src/CubicalHott/Example3-6-2.agda  |  2 +-
 src/CubicalHott/Lemma3-11-3.agda   |  2 +-
 src/CubicalHott/Lemma3-11-4.agda   | 14 +++++++++-----
 src/CubicalHott/Theorem7-1-10.agda |  2 +-
 4 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/src/CubicalHott/Example3-6-2.agda b/src/CubicalHott/Example3-6-2.agda
index 06e1467..94954c2 100644
--- a/src/CubicalHott/Example3-6-2.agda
+++ b/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
\ No newline at end of file
+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
\ No newline at end of file
diff --git a/src/CubicalHott/Lemma3-11-3.agda b/src/CubicalHott/Lemma3-11-3.agda
index 9468305..a078336 100644
--- a/src/CubicalHott/Lemma3-11-3.agda
+++ b/src/CubicalHott/Lemma3-11-3.agda
@@ -2,4 +2,4 @@
 
 module CubicalHott.Lemma3-11-3 where
 
-open import Cubical.Foundations.Prelude
\ No newline at end of file
+open import Cubical.Foundations.Prelude
diff --git a/src/CubicalHott/Lemma3-11-4.agda b/src/CubicalHott/Lemma3-11-4.agda
index d6ec615..4ac0334 100644
--- a/src/CubicalHott/Lemma3-11-4.agda
+++ b/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
\ No newline at end of file
diff --git a/src/CubicalHott/Theorem7-1-10.agda b/src/CubicalHott/Theorem7-1-10.agda
index 3e5a00d..a3bd843 100644
--- a/src/CubicalHott/Theorem7-1-10.agda
+++ b/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 = {!   !}
\ No newline at end of file