From 136d9f67c3b57ae26fed15914509b9269348ab02 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Sun, 20 Oct 2024 03:06:06 -0500
Subject: [PATCH] proved theorem 7.1.10, closes #34

---
 src/CubicalHott/Theorem7-1-10.agda | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/CubicalHott/Theorem7-1-10.agda b/src/CubicalHott/Theorem7-1-10.agda
index a3bd843..6d684fd 100644
--- a/src/CubicalHott/Theorem7-1-10.agda
+++ b/src/CubicalHott/Theorem7-1-10.agda
@@ -6,9 +6,11 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 open import Cubical.Data.Nat
 
-z = isContr
+open import CubicalHott.Lemma3-11-4 renaming (lemma to lemma3-11-4)
 
 theorem : {X : Type} → (n : ℕ) → isProp (isOfHLevel n X)
-theorem zero = {!   !}
-theorem (suc zero) x y = {!   !} 
-theorem (suc (suc n)) x y = {!   !}
\ No newline at end of file
+theorem zero = lemma3-11-4
+theorem (suc zero) isProp1 isProp2 i x y j = isProp→isSet isProp1 x y (isProp1 x y) (isProp2 x y) i j
+theorem {X = X} (suc (suc n)) isHLevel1 isHLevel2 =
+  let IH = λ (x y : X) → theorem {X = x ≡ y} (suc n) in
+  funExt (λ x → funExt (λ y → IH x y (isHLevel1 x y) (isHLevel2 x y)))
\ No newline at end of file