diff --git a/notes/HLevels.md b/notes/HLevels.md
new file mode 100644
index 0000000..8138e22
--- /dev/null
+++ b/notes/HLevels.md
@@ -0,0 +1,27 @@
+# Properties
+
+- Theorem 7.1.4:
+  - IF: $X$ is an $n$-type
+  - IF: $X \rightarrow Y$ is a retraction (has a left-inverse)
+  - THEN: $Y$ is an $n$-type
+- Corollary 7.1.5:
+  - IF: $X \simeq Y$
+  - IF: $X$ is an $n$-type
+  - THEN: $Y$ is an $n$-type
+- Theorem 7.1.7:
+  - IF: $X$ is an $n$-type
+  - THEN: it is also an $(n + 1)$-type
+- Theorem 7.1.8:
+  - IF: $A$ is an $n$-type
+  - IF: $B(a)$ is an $n$-type for all $a : A$
+  - THEN: $\sum_{(x : A)} B(x)$ is an $n$-type
+
+## -2: Contractible
+
+## -1: Mere props
+
+- If $A$ and $B$ are mere props, so is $A \times B$
+
+- If $B(a)$ is a prop for any $a:A$, then $\prod_{(x:A)} B(x)$ is a prop
+
+-
diff --git a/src/CubicalHott/Example3-6-2.agda b/src/CubicalHott/Example3-6-2.agda
new file mode 100644
index 0000000..06e1467
--- /dev/null
+++ b/src/CubicalHott/Example3-6-2.agda
@@ -0,0 +1,10 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Example3-6-2 where
+
+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
diff --git a/src/CubicalHott/Lemma3-11-3.agda b/src/CubicalHott/Lemma3-11-3.agda
new file mode 100644
index 0000000..9468305
--- /dev/null
+++ b/src/CubicalHott/Lemma3-11-3.agda
@@ -0,0 +1,5 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma3-11-3 where
+
+open import Cubical.Foundations.Prelude
\ No newline at end of file
diff --git a/src/CubicalHott/Lemma3-11-4.agda b/src/CubicalHott/Lemma3-11-4.agda
index 8d92639..d6ec615 100644
--- a/src/CubicalHott/Lemma3-11-4.agda
+++ b/src/CubicalHott/Lemma3-11-4.agda
@@ -5,4 +5,11 @@ module CubicalHott.Lemma3-11-4 where
 open import Cubical.Foundations.Prelude
 
 lemma : {A : Type} → isProp (isContr A)
-lemma (x , px) (y , py) i = px y i , {!   !}
\ No newline at end of file
+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 → {!   !}
+  -- λ 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 855d15b..3e5a00d 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 , let z = snd x (fst y) i in λ y' j → {!   !}
+theorem zero x y i = snd x (fst y) i , {!   !}
 theorem (suc zero) x y = {!   !} 
 theorem (suc (suc n)) x y = {!   !}
\ No newline at end of file