diff --git a/1FundamentalGroup/Quest0SideQuests/Empty.agda b/1FundamentalGroup/Quest0SideQuests/Empty.agda
new file mode 100644
index 0000000..0d70498
--- /dev/null
+++ b/1FundamentalGroup/Quest0SideQuests/Empty.agda
@@ -0,0 +1,24 @@
+module 1FundamentalGroup.Quest0SideQuests.Empty where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Empty renaming (rec to ⊥Rec)
+open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_)
+
+toEmpty : (A : Type) → Type
+toEmpty A = {!!}
+
+-- why Type₁
+pathEmpty : (A : Type) → Type₁
+pathEmpty A = {!!}
+
+isoEmpty : (A : Type) → Type
+isoEmpty A = {!!}
+
+toEmpty→isoEmpty : (A : Type) → toEmpty A → isoEmpty A
+toEmpty→isoEmpty A f = {!!}
+
+isoEmpty→pathEmpty : (A : Type) → isoEmpty A → pathEmpty A
+isoEmpty→pathEmpty A = {!!}
+
+pathEmpty→toEmpty : (A : Type) → pathEmpty A → toEmpty A
+pathEmpty→toEmpty A p = {!!}
diff --git a/1FundamentalGroup/Quest0SideQuests/EmptySolutions.agda b/1FundamentalGroup/Quest0SideQuests/EmptySolutions.agda
new file mode 100644
index 0000000..0b3df63
--- /dev/null
+++ b/1FundamentalGroup/Quest0SideQuests/EmptySolutions.agda
@@ -0,0 +1,30 @@
+module 1FundamentalGroup.Quest0SideQuests.EmptySolutions where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Empty renaming (rec to ⊥Rec)
+open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_)
+
+toEmpty : (A : Type) → Type
+toEmpty A = A → ⊥
+
+-- why Type₁
+pathEmpty : (A : Type) → Type₁
+pathEmpty A = A ≡ ⊥
+
+isoEmpty : (A : Type) → Type
+isoEmpty A = A ≅ ⊥
+
+toEmpty→isoEmpty : (A : Type) → toEmpty A → isoEmpty A
+toEmpty→isoEmpty A f = iso f ⊥Rec rightInv leftInv where
+
+  rightInv : section f ⊥Rec
+  rightInv ()
+
+  leftInv : retract f ⊥Rec
+  leftInv x = ⊥Rec (f x)
+
+isoEmpty→pathEmpty : (A : Type) → isoEmpty A → pathEmpty A
+isoEmpty→pathEmpty A = isoToPath
+
+pathEmpty→toEmpty : (A : Type) → pathEmpty A → toEmpty A
+pathEmpty→toEmpty A p = J (λ B q → toEmpty B) (λ x → x) (sym p)
diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/Empty.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/Empty.agdai
new file mode 100644
index 0000000..75a28ce
Binary files /dev/null and b/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/Empty.agdai differ
diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/EmptySolutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/EmptySolutions.agdai
new file mode 100644
index 0000000..16b8695
Binary files /dev/null and b/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/EmptySolutions.agdai differ