diff --git a/1FundamentalGroup/Quest0SideQuests/TrueNotFalse.agda b/1FundamentalGroup/Quest0SideQuests/TrueNotFalse.agda
new file mode 100644
index 0000000..7e8ede4
--- /dev/null
+++ b/1FundamentalGroup/Quest0SideQuests/TrueNotFalse.agda
@@ -0,0 +1,9 @@
+module 1FundamentalGroup.Quest0SideQuests.TrueNotFalse where
+
+open import Cubical.Data.Empty
+open import Cubical.Data.Unit renaming ( Unit to ⊤ )
+open import Cubical.Data.Bool using (Bool ; true ; false)
+open import Cubical.Foundations.Prelude
+
+true≢false : true ≡ false → ⊥
+true≢false = {!!}
diff --git a/1FundamentalGroup/Quest0SideQuests/SideQuest0.agda b/1FundamentalGroup/Quest0SideQuests/TrueNotFalseSolutions.agda
similarity index 66%
rename from 1FundamentalGroup/Quest0SideQuests/SideQuest0.agda
rename to 1FundamentalGroup/Quest0SideQuests/TrueNotFalseSolutions.agda
index fac13ea..16149ff 100644
--- a/1FundamentalGroup/Quest0SideQuests/SideQuest0.agda
+++ b/1FundamentalGroup/Quest0SideQuests/TrueNotFalseSolutions.agda
@@ -1,12 +1,12 @@
-module 1FundamentalGroup.Quest0SideQuests.SideQuest0 where
+module 1FundamentalGroup.Quest0SideQuests.TrueNotFalseSolutions where
 
 open import Cubical.Data.Empty
 open import Cubical.Data.Unit renaming ( Unit to ⊤ )
-open import Cubical.Data.Bool
+open import Cubical.Data.Bool using (Bool ; true ; false)
 open import Cubical.Foundations.Prelude
 
-true≢false' : true ≡ false → ⊥
-true≢false' h = transport ⊤≡⊥ tt where
+true≢false : true ≡ false → ⊥
+true≢false h = transport ⊤≡⊥ tt where
 
   propify : Bool → Type
   propify false = ⊥
diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/SideQuest0.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/SideQuest0.agdai
new file mode 100644
index 0000000..a266b9d
Binary files /dev/null and b/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/SideQuest0.agdai differ
diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/TrueNotFalse.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/TrueNotFalse.agdai
new file mode 100644
index 0000000..059626c
Binary files /dev/null and b/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/TrueNotFalse.agdai differ
diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/TrueNotFalseSolutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/TrueNotFalseSolutions.agdai
new file mode 100644
index 0000000..f91a74e
Binary files /dev/null and b/_build/2.6.2/agda/1FundamentalGroup/Quest0SideQuests/TrueNotFalseSolutions.agdai differ