diff --git a/Trinitarianism/Quest0.agda b/Trinitarianism/Quest0.agda
index dcb28cd..31607c0 100644
--- a/Trinitarianism/Quest0.agda
+++ b/Trinitarianism/Quest0.agda
@@ -1,8 +1,9 @@
 module Trinitarianism.Quest0 where
 open import Trinitarianism.Quest0Preamble
 
-postulate
-  u : Level
+private
+  postulate
+    u : Level
 
 data ⊤ : Type u where
   trivial : ⊤
diff --git a/Trinitarianism/Quest0Solutions.agda b/Trinitarianism/Quest0Solutions.agda
new file mode 100644
index 0000000..51331f8
--- /dev/null
+++ b/Trinitarianism/Quest0Solutions.agda
@@ -0,0 +1,30 @@
+module Trinitarianism.Quest0Solutions where
+open import Trinitarianism.Quest0Preamble
+
+private
+  postulate
+    u : Level
+
+data ⊤ : Type u where
+  trivial : ⊤
+
+TrueToTrue : ⊤ → ⊤
+TrueToTrue = λ x → x
+
+TrueToTrue' : ⊤ → ⊤
+TrueToTrue' x = x
+
+TrueToTrue'' : ⊤ → ⊤
+TrueToTrue'' trivial = trivial
+
+TrueToTrue''' : ⊤ → ⊤
+TrueToTrue''' x = trivial
+
+data ⊥ : Type u where
+
+explosion : ⊥ → ⊤
+explosion x = {!!}
+
+data ℕ : Type u where
+  zero : ℕ
+  suc : ℕ → ℕ
diff --git a/Trinitarianism/AsProps/Quest0.agda b/Trinitarianism/bin/AsProps/Quest0.agda
similarity index 100%
rename from Trinitarianism/AsProps/Quest0.agda
rename to Trinitarianism/bin/AsProps/Quest0.agda
diff --git a/Trinitarianism/AsProps/Quest0Preamble.agda b/Trinitarianism/bin/AsProps/Quest0Preamble.agda
similarity index 100%
rename from Trinitarianism/AsProps/Quest0Preamble.agda
rename to Trinitarianism/bin/AsProps/Quest0Preamble.agda
diff --git a/Trinitarianism/AsProps/Quest0Solutions.agda b/Trinitarianism/bin/AsProps/Quest0Solutions.agda
similarity index 71%
rename from Trinitarianism/AsProps/Quest0Solutions.agda
rename to Trinitarianism/bin/AsProps/Quest0Solutions.agda
index 9771bb0..f283373 100644
--- a/Trinitarianism/AsProps/Quest0Solutions.agda
+++ b/Trinitarianism/bin/AsProps/Quest0Solutions.agda
@@ -1,10 +1,14 @@
-module Trinitarianism.AsProps.Quest0Solutions where
-open import Trinitarianism.AsProps.Quest0Preamble
+module Trinitarianism.Quest0Solutions where
+open import Trinitarianism.Quest0Preamble
 
-data ⊤ : Prop where
+private
+  postulate
+    u : Level
+
+data ⊤ : Type u where
   trivial : ⊤
 
-data ⊥ : Prop where
+data ⊥ : Type u where
 
 TrueToTrue : ⊤ → ⊤
 TrueToTrue = λ x → x
@@ -18,7 +22,7 @@ TrueToTrue'' trivial = trivial
 TrueToTrue''' : ⊤ → ⊤
 TrueToTrue''' x = trivial
 
-isZero : ℕ → Prop
+isZero : ℕ → Type u
 isZero zero = ⊤
 isZero (suc n) = ⊥
 
@@ -28,7 +32,7 @@ ExistsZero = zero , trivial
 AllZero→⊥ : ((x : ℕ) → isZero x) → ⊥
 AllZero→⊥ h = h 1
 
-data _∨_ (P Q : Prop) : Prop where
+data _∨_ (P Q : Type u) : Type u where
   left : P → P ∨ Q
   right : Q → P ∨ Q
 
diff --git a/Trinitarianism/AsProps/Quest0Solutions.lagda.md b/Trinitarianism/bin/AsProps/Quest0Solutions.lagda.md
similarity index 100%
rename from Trinitarianism/AsProps/Quest0Solutions.lagda.md
rename to Trinitarianism/bin/AsProps/Quest0Solutions.lagda.md
diff --git a/Trinitarianism/AsProps/Quest1.agda b/Trinitarianism/bin/AsProps/Quest1.agda
similarity index 100%
rename from Trinitarianism/AsProps/Quest1.agda
rename to Trinitarianism/bin/AsProps/Quest1.agda
diff --git a/Trinitarianism/AsTypes/Quest0.agda b/Trinitarianism/bin/AsTypes/Quest0.agda
similarity index 100%
rename from Trinitarianism/AsTypes/Quest0.agda
rename to Trinitarianism/bin/AsTypes/Quest0.agda
diff --git a/_build/2.6.3/agda/Trinitarianism/Quest0Solutions.agdai b/_build/2.6.3/agda/Trinitarianism/Quest0Solutions.agdai
new file mode 100644
index 0000000..c2ae7f3
Binary files /dev/null and b/_build/2.6.3/agda/Trinitarianism/Quest0Solutions.agdai differ