diff --git a/src/CubicalHott/Corollary6-4-3.agda b/src/CubicalHott/Corollary6-4-3.agda
new file mode 100644
index 0000000..b521d82
--- /dev/null
+++ b/src/CubicalHott/Corollary6-4-3.agda
@@ -0,0 +1,16 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Corollary6-4-3 where
+
+open import Agda.Primitive
+open import Cubical.Relation.Nullary
+open import Cubical.Foundations.Prelude
+open import Cubical.HITs.S1
+
+corollary : (l : Level) → ¬ (isGroupoid (Type l))
+corollary l p = g1 p where
+  g1 : ¬ (isGroupoid (Type l))
+
+  g2 : (A : Type l) → ¬ (isSet (A ≡ A))
+  g1 grpd = g2 (Lift S¹) {! grpd (Lift S¹) ? ? ? ? !}
+  
\ No newline at end of file
diff --git a/src/CubicalHott/Corollary7-1-5.agda b/src/CubicalHott/Corollary7-1-5.agda
new file mode 100644
index 0000000..3b1f294
--- /dev/null
+++ b/src/CubicalHott/Corollary7-1-5.agda
@@ -0,0 +1,10 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Corollary7-1-5 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Data.Nat
+
+corollary : {X Y : Type} → (n : ℕ) → isOfHLevel n X → isOfHLevel n Y
+corollary n = {!   !}
\ No newline at end of file