diff --git a/Trinitarianism/Quest0.agda b/Trinitarianism/Quest0.agda
index 9aeccb3..39c894e 100644
--- a/Trinitarianism/Quest0.agda
+++ b/Trinitarianism/Quest0.agda
@@ -4,7 +4,7 @@ open import Trinitarianism.Quest0Preamble
 private
   postulate
     u : Level
-    A : Type u
+
 
 {-
 There are three ways of looking at `A : Type u`.
@@ -147,8 +147,12 @@ unlike Type Theory!)
 
 -}
 
+postulate
+  A : Type u
 
-
+NNO : A → (A → A) → (ℕ → A)
+NNO a s zero = a
+NNO a s (suc n) = s (NNO a s n)
 
 
 
diff --git a/Trinitarianism/Quest0.md b/Trinitarianism/Quest0.md
index 0b2ee50..74cdba6 100644
--- a/Trinitarianism/Quest0.md
+++ b/Trinitarianism/Quest0.md
@@ -127,8 +127,7 @@ We can see `ℕ` as a categorical notion:
 with `zero : ⊤ → ℕ` and `suc : ℕ → ℕ` such that
 given any `⊤ → A → A` there exist a unique morphism `ℕ → A`
 such that the diagram commutes:
-<img src="images/nno.png" alt="nno" width="200"/>
-
+<img src="images/nno.png" alt="nno" width="400"/>
 
 This has no interpretation as a proposition since
 there are too many terms,
@@ -137,8 +136,7 @@ between proofs of the same thing.
 (ZFC doesn't even mention logic internally,
 unlike Type Theory!)
 
+To see how to use terms of type `ℕ`, i.e. induct on `ℕ`, 
+go to Quest1!
 
 
-
--}
-
diff --git a/Trinitarianism/README.md b/Trinitarianism/README.md
index 33c4ef7..d1487f7 100644
--- a/Trinitarianism/README.md
+++ b/Trinitarianism/README.md
@@ -28,7 +28,7 @@ In category theory, types are objects and terms are generalised elements.
 - and / pairs / product
 - implication / functions / internal hom
 
-# Dependent Types
+## Dependent Types
 
 - predicate / type family / over category
 - substitution / substitution / pullback