diff --git a/README.md b/README.md
index 8465b57..7cc6e4d 100644
--- a/README.md
+++ b/README.md
@@ -45,15 +45,15 @@ Some text should be highlighted, and any `?` should turn into `{ }`.
 
 ## How the game works
 
-Our Game is under development. Please contact the devs.
-Currently you can try the _quests_ in the `Trinitarianism` folder.
+Our Game is currently under development. 
+As of now you can try the _quests_ in the `Trinitarianism` folder.
 Each quest consists of three files, for example :
-- `Trinitarianism/Quest0.md` is the guide for the quest
+- `Trinitarianism/Quest0.md` is the guide for the quest.
   In there, you will find details of the tasks 
   you must finish in order to complete the quest.
   For now, it is recommended that
   you view these online within github.
-- `Trinitarianism/Quest0.agda` is the actual file in which
+- `Trinitarianism/Quest0.agda` is the agda file in which
   you do the quest. 
 - `Trinitarianism/Quest0Solutions.agda` contains
   solutions to the tasks in the quest.
diff --git a/Trinitarianism/.DS_Store b/Trinitarianism/.DS_Store
deleted file mode 100644
index 5008ddf..0000000
Binary files a/Trinitarianism/.DS_Store and /dev/null differ
diff --git a/Trinitarianism/Preambles/P2.agda b/Trinitarianism/Preambles/P2.agda
index 3cdcc62..3a68b12 100644
--- a/Trinitarianism/Preambles/P2.agda
+++ b/Trinitarianism/Preambles/P2.agda
@@ -3,3 +3,4 @@ module Trinitarianism.Preambles.P2 where
 open import Cubical.Core.Everything public
 open import Cubical.Data.Nat public hiding (_+_ ; isEven)
 open import Trinitarianism.Quest1Solutions public
+open import Cubical.Data.Empty public using (⊥)
diff --git a/Trinitarianism/Quest0.md b/Trinitarianism/Quest0.md
index 807e0f4..102f867 100644
--- a/Trinitarianism/Quest0.md
+++ b/Trinitarianism/Quest0.md
@@ -44,7 +44,8 @@ TrueToTrue = {!!}
     and now you can fill the hole `{ }`
   - navigate to the hole `{ }` using `C-c C-f` (forward) or `C-c C-b` (backward)
   - enter `C-c C-r` and agda will try to help you (`r` stands for _refine_)
-  - you should see `λ x → { }`
+  - you should see `λ x → { }`. This is agda's notation for `x ↦ { }` 
+    and is called `λ` abstraction, `λ` for 'let'.
   - navigate to the new hole
   - enter `C-c C-,` to check the _goal_ (`C-c C-comma`)
   - the Goal area ('agda information' window) should look like
diff --git a/Trinitarianism/Quest1.agda b/Trinitarianism/Quest1.agda
index 2e90b68..8c0d83d 100644
--- a/Trinitarianism/Quest1.agda
+++ b/Trinitarianism/Quest1.agda
@@ -11,5 +11,8 @@ Remove this comment block and formulate
 'there exists an even natural' here.
 -}
 
+_×_ : Type → Type → Type
+A × C = Σ A (λ a → C)
+
 div2 : Σ ℕ isEven → ℕ
 div2 x = {!!}
diff --git a/Trinitarianism/Quest1.md b/Trinitarianism/Quest1.md
index 7c456cd..5000e56 100644
--- a/Trinitarianism/Quest1.md
+++ b/Trinitarianism/Quest1.md
@@ -103,9 +103,13 @@ using `ℕ` from the cubical agda library.)
      
 Now that we have expressed `isEven` we need to be able write down "existence".
 In maths we might write 
-```∃ x ∈ ℕ, isEven x```
+```
+∃ x ∈ ℕ, isEven x
+```
 which in agda notation is 
-```Σ ℕ isEven```
+```
+Σ ℕ isEven
+```
 This is called a _sigma type_, which has three interpretations:
 - the proposition 'there exists an even natural'
 - the construction 
@@ -139,8 +143,27 @@ Name = ?
 
 In general when `A : Type` is a type and `B : A → Type` is a 
 predicate/dependent construction/bundle over `A`, 
-we can write the type `Σ A B` whose terms are pairs `a , b` 
-where `a : A` and `b : B a`.
+we can write the sigma type `Σ A B` whose terms are pairs `a , b` 
+where `a : A` and `b : B a`. 
+In the special case when `B` is not dependent on `a : A`,
+i.e. it looks like `λ a → C` for some `C : Type` then 
+`Σ A B` is just 
+- the proposition '`A` and `C`' 
+  since giving a proof of this is the same as giving a proof 
+  of `A` and a proof of `C`
+- a recipe `a : A` together with a recipe `c : C`
+- `B` is now a _trivial bundle_ since the fibers `B a` are 
+  constant with respect to `a : A`.
+  In other words it is just a _product_ `Σ A B ≅ A × C`.
+  For this reason, 
+  some refer to the sigma type as the _dependent product_,
+  but we will avoid this terminology.
+```agda
+_×_ : Type → Type → Type
+A × C = Σ A (λ a → C)
+```
+Agda supports the notation `_×_` (without spaces)
+which means from now on you can write `A × C` (with spaces).
 
 There are two ways of using a term in a sigma type.
 We can extract the first part using `fst` or the second part using `snd`.
diff --git a/Trinitarianism/Quest1Solutions.agda b/Trinitarianism/Quest1Solutions.agda
index b158b69..1c5a560 100644
--- a/Trinitarianism/Quest1Solutions.agda
+++ b/Trinitarianism/Quest1Solutions.agda
@@ -7,10 +7,12 @@ isEven zero = ⊤
 isEven (suc zero) = ⊥
 isEven (suc (suc n)) = isEven n
 
-
 existsEven : Σ ℕ isEven
 existsEven = 4 , tt
 
+_×_ : Type → Type → Type
+A × C = Σ A (λ a → C)
+
 div2 : Σ ℕ isEven → ℕ
 div2 (0 , tt) = 0
 div2 (suc (suc n) , hn) = suc (div2 (n , hn))
diff --git a/Trinitarianism/Quest2.md b/Trinitarianism/Quest2.md
index ad3c69e..700b3d4 100644
--- a/Trinitarianism/Quest2.md
+++ b/Trinitarianism/Quest2.md
@@ -9,9 +9,6 @@ so it should have type `ℕ → ℕ → ℕ`.
 _+_ : ℕ → ℕ → ℕ
 n + m = ?
 ```
-Agda supports the notation `_+_` (without spaces)
-which means from now on you can write `0 + 1` 
-and so on (with spaces).
 Try coming up with a sensible definition.
 It may not look 'the same' as ours.
 <p>
@@ -68,3 +65,26 @@ someone else's definition of addition,
 it might not work anymore.
 > But `_+_` and `_+'_` compute the same values. 
 > Are `_+_` and `_+'_` 'the same'? What is 'the same'?
+
+As the final task of the Quest,
+try to express and prove in agda the statement
+> For any natural number it is even or is is not even.
+We will make a summary of what is needed:
+- a definition of the type `A ⊕ B` (input `\oplus`),
+  which has three interpretations
+  - the proposition '`A` or `B`'
+  - the construction with two ways of making recipes 
+    `left : A → A ⊕ B`
+    and `right : B → A ⊕ B`.
+  - the coproduct of two objects `A` and `B`.
+  The type needs to take in parameters `A : Type` and `B : Type`
+  ```agda
+  data _⊕_ (A : Type) (B : Type) : Type where
+    ???
+  ```
+- a definition of negation. One can motivate it by the following
+  - Define `A ↔ B : Type` for two types `A : Type` and `B : Type`.
+  - Show that for any `A : Type` we have `(A ↔ ⊥) ↔ (A → ⊥)`
+  - Define `¬ : Type → Type` to be `λ A → (A → ⊥)`.
+- a formulation and proof of the statement above
+
diff --git a/Trinitarianism/Quest2Solutions.agda b/Trinitarianism/Quest2Solutions.agda
index 56f3250..be2ecfc 100644
--- a/Trinitarianism/Quest2Solutions.agda
+++ b/Trinitarianism/Quest2Solutions.agda
@@ -21,3 +21,38 @@ Sum'OfEven x (zero , hy) = x .snd
 Sum'OfEven x (suc (suc y) , hy) = Sum'OfEven x (y , hy)
 
 -}
+
+data _⊕_ (A : Type) (B : Type) : Type where
+  left : A → A ⊕ B
+  right : B → A ⊕ B
+
+_↔_ : Type → Type → Type
+_↔_ A B = (A → B) × (B → A)
+
+¬Motivation : (A : Type) → ((A ↔ ⊥) ↔ (A → ⊥))
+¬Motivation A =
+  -- forward direction
+  (
+    -- suppose we have a proof `hiff : A ↔ ⊥`
+    λ hiff →
+    -- give the forward map only
+    fst hiff
+  ) ,
+  -- backward direction; assume a proof hto : A → ⊥
+  λ hto →
+    -- we need to show A → ⊥ which we have already
+    hto
+    ,
+    -- we need to show ⊥ → A, which is the principle of explosion
+    λ ()
+
+¬ : Type → Type
+¬ A = A → ⊥
+
+isEvenDecidable : (n : ℕ) → isEven n ⊕ ¬ (isEven n)
+-- zero is even; go left
+isEvenDecidable zero = left tt
+-- one is not even; go right
+isEvenDecidable (suc zero) = right (λ ())
+-- inductive step
+isEvenDecidable (suc (suc n)) = isEvenDecidable n
diff --git a/Trinitarianism/README.md b/Trinitarianism/README.md
index 85e12c8..5713794 100644
--- a/Trinitarianism/README.md
+++ b/Trinitarianism/README.md
@@ -41,9 +41,9 @@ In category theory, types are objects and terms are generalised elements.
 - existence / Σ type / total space of bundles 
 - for all / Π type / space of sections of bundles
 
-## Something doesn't feel the Same
+## What is 'the Same'?
 
 There will be one thing missing from this 'place to do maths'
 and that is a notion of _equality_.
-This is where HoTT deviates from its predecessors,
-and is the theme of the next arc.
+How HoTT treats equality is where it deviates from its predecessors.
+This is the theme of the next arc.
diff --git a/_build/2.6.2/agda/Trinitarianism/Preambles/P2.agdai b/_build/2.6.2/agda/Trinitarianism/Preambles/P2.agdai
index 37e8e37..6f40a83 100644
Binary files a/_build/2.6.2/agda/Trinitarianism/Preambles/P2.agdai and b/_build/2.6.2/agda/Trinitarianism/Preambles/P2.agdai differ
diff --git a/_build/2.6.2/agda/Trinitarianism/Quest1Solutions.agdai b/_build/2.6.2/agda/Trinitarianism/Quest1Solutions.agdai
index 70eb87e..b0c96bd 100644
Binary files a/_build/2.6.2/agda/Trinitarianism/Quest1Solutions.agdai and b/_build/2.6.2/agda/Trinitarianism/Quest1Solutions.agdai differ
diff --git a/_build/2.6.2/agda/Trinitarianism/Quest2Solutions.agdai b/_build/2.6.2/agda/Trinitarianism/Quest2Solutions.agdai
index 207b804..bb64659 100644
Binary files a/_build/2.6.2/agda/Trinitarianism/Quest2Solutions.agdai and b/_build/2.6.2/agda/Trinitarianism/Quest2Solutions.agdai differ