diff --git a/0Trinitarianism/Quest4Solutions.agda b/0Trinitarianism/Quest4Solutions.agda
new file mode 100644
index 0000000..2298650
--- /dev/null
+++ b/0Trinitarianism/Quest4Solutions.agda
@@ -0,0 +1,7 @@
+module 0Trinitarianism.Quest4Solutions where
+
+open import Cubical.Foundations.Prelude
+
+data _≣_ {A : Type} : (x y : A) → Type where
+
+  rfl : (x : A) → x ≣ x
diff --git a/1FundamentalGroup/Quest0.agda b/1FundamentalGroup/Quest0.agda
index 430de35..0d0bae6 100644
--- a/1FundamentalGroup/Quest0.agda
+++ b/1FundamentalGroup/Quest0.agda
@@ -2,7 +2,6 @@
 module 1FundamentalGroup.Quest0 where
 open import 1FundamentalGroup.Preambles.P0
 
-
 Refl : base ≡ base
 Refl = {!!}
 
diff --git a/_build/2.6.2/agda/0Trinitarianism/Quest4Solutions.agdai b/_build/2.6.2/agda/0Trinitarianism/Quest4Solutions.agdai
new file mode 100644
index 0000000..1f731ce
Binary files /dev/null and b/_build/2.6.2/agda/0Trinitarianism/Quest4Solutions.agdai differ