diff --git a/src/Connectives.lagda b/src/Connectives.lagda
index def58a18..d086d8d9 100644
--- a/src/Connectives.lagda
+++ b/src/Connectives.lagda
@@ -28,7 +28,7 @@ open import Data.Nat.Properties.Simple using (+-suc)
 open import Function using (_∘_)
 \end{code}
 
-In what follows, we will occasionally require [extensionality][extensionality].
+We assume [extensionality][extensionality].
 \begin{code}
 postulate
   extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
diff --git a/src/Negation.lagda b/src/Negation.lagda
index 5392fc98..c1b1ad0d 100644
--- a/src/Negation.lagda
+++ b/src/Negation.lagda
@@ -96,28 +96,28 @@ will show that assuming `A` leads to a contradiction, and hence
 we may conclude `⊥`, evidenced by `¬y (f x)`.  Hence, we have shown
 `¬ A`.
 
-Using negation, it is straightforward to define unequal.
+Using negation, it is straightforward to define inequality.
 \begin{code}
 _≢_ : ∀ {A : Set} → A → A → Set
 x ≢ y  =  ¬ (x ≡ y)
 \end{code}
-It is straightforward to show distinct numbers are unequal.
+It is straightforward to show distinct numbers are not equal.
 \begin{code}
 _ : 1 ≢ 2
 _ = λ()
 \end{code}
-This is our first use of an absurd patters in a lambda expression.
+This is our first use of an absurd pattern in a lambda expression.
 The type `M ≡ N` is occupied exactly when `M` and `N` simplify to
 identical terms. Since `1` and `2` simplify to distinct normal forms,
-Agda determines that the absurd pattern `()` matches all arguments of
-type `1 ≡ 2`.  As a second example, it is also easy to validate
+Agda determines that there is no possible evidence that `1 ≡ 2`.
+As a second example, it is also easy to validate
 Peano's postulate that zero is not the successor of any number.
 \begin{code}
 peano : ∀ {m : ℕ} → zero ≢ suc m
 peano = λ()
 \end{code}
 The evidence is essentially the same, as the absurd pattern matches
-all arguments of type `zero ≡ suc m`. 
+all possible evidence of type `zero ≡ suc m`. 
 
 Given the correspondence of implication to exponentiation and
 false to the type with no members, we can view negation as
diff --git a/src/Quantifiers.lagda b/src/Quantifiers.lagda
index 7236a582..3d10ed85 100644
--- a/src/Quantifiers.lagda
+++ b/src/Quantifiers.lagda
@@ -22,7 +22,7 @@ open import Data.Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 \end{code}
 
-In what follows, we will occasionally require [extensionality][extensionality].
+We assume [extensionality][extensionality].
 \begin{code}
 postulate
   extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
@@ -44,9 +44,9 @@ dependent function type, which has appeared throughout this book.
 
 Evidence that `∀ (x : A) → B x` holds is of the form
 
-    λ (x : A) → N x
+    λ (x : A) → N
 
-where `N x` is a term of type `B x`, and `N x` and `B x` both contain
+where `N` is a term of type `B x`, and `N x` and `B x` both contain
 a free variable `x` of type `A`.  Given a term `L` providing evidence
 that `∀ (x : A) → B x` holds, and a term `M` of type `A`, the term `L
 M` provides evidence that `B M` holds.  In other words, evidence that
@@ -59,7 +59,7 @@ is a term of type `A` then we may conclude that `B M` holds.
 ∀-elim : ∀ {A : Set} {B : A → Set} → (∀ (x : A) → B x) → (M : A) → B M
 ∀-elim L M = L M
 \end{code}
-In medieval times, this rule was known by the name *dictum de omni*.
+As with `→-elim`, the rule corresponds to function application.
 
 Ordinary function types arise as the special case of dependent
 function types where the range does not depend on a variable drawn
@@ -70,8 +70,12 @@ universal, its domain is viewed as a data type and its range is viewed
 as a type of evidence.  This is just a matter of interpretation, since
 in Agda data types and types of evidence are indistinguishable.
 
-Unlike with conjunction, disjunction, and implication, there is no simple
-analogy between universals and arithmetic.
+Dependent function types are sometimes referred to as dependent products,
+because if `A` is a finite type with values `{ x₁ , ⋯ , xᵢ }`, and if
+each of the types `B x₁ , ⋯ B xᵢ` has `m₁ , ⋯ , mᵢ` distinct members,
+then `∀ (x : A) → B x` has `m₁ × ⋯ × mᵢ` members.  Because of the
+association of `Π` with products, sometimes the notation `∀ (x : A) → B x`
+is replaced by a notation such as `Π[ x ∈ A ] (B x)`.
 
 ### Exercise (`∀-distrib-×`)
 
@@ -91,54 +95,48 @@ Show that a disjunction of universals implies a universal of disjunctions.
 \end{code}
 Does the converse also hold? If so, prove; if not, explain why.
 
+
 ## Existentials
 
 Given a variable `x` of type `A` and a proposition `B x` which
 contains `x` as a free variable, the existentially quantified
-proposition `∃[ x ] → B x` holds if for some term `M` of type
+proposition `∃ (λ (x : A) → B x)` holds if for some term `M` of type
 `A` the proposition `B M` holds.  Here `B M` stands for
 the proposition `B x` with each free occurrence of `x` replaced by
 `M`.  The variable `x` appears free in `B x` but bound in
-`∃[ x ] → B x`.
-
-It is common to adopt a notation such as `∃[ x : A ]→ B[x]`,
-which introduces `x` as a bound variable of type `A` that appears
-free in `B[x]` and bound in `∃[ x : A ]→ B[x]`.  We won't do
-that here, but instead use the lambda notation built-in to Agda
-to introduce `x` as a bound variable.
+`∃ (λ (x : A) → B x)`.
 
 We formalise existential quantification by declaring a suitable
 inductive type.
 \begin{code}
-data ∃ (A : Set) (B : A → Set) : Set where
-  _,_ : (x : A) → B x → ∃ A B
+data ∃ {A : Set} (B : A → Set) : Set where
+  _,_ : (x : A) → B x → ∃ B
 \end{code}
-Evidence that `∃ (λ (x : A) → B[x])` holds is of the form
+Evidence that `∃ (λ (x : A) → B x)` holds is of the form
 `(M , N)` where `M` is a term of type `A`, and `N` is evidence
-that `B[M]` holds.
+that `B M` holds.
 
-\begin{code}
-syntax ∃ A (λ x → B) = ∃[ x ∈ A ] B
-\end{code}
-
-Given evidence that `∃ (λ (x : A) → B[x])` holds, and
-given evidence that `∀ (x : A) → B[x] → C` holds, where `C` does
+Given evidence that `∃ (λ (x : A) → B x)` holds, and
+given evidence that `∀ (x : A) → B x → C` holds, where `C` does
 not contain `x` as a free variable, we may conclude that `C` holds.
 \begin{code}
 ∃-elim : ∀ {A : Set} {B : A → Set} {C : Set} →
-  (∃[ x ∈ A ] B x) → (∀ (x : A) → B x → C) → C
+  (∃ (λ (x : A) → B x)) → (∀ (x : A) → B x → C) → C
 ∃-elim (M , N) P = P M N
 \end{code}
-In other words, if we know for every `x` of type `A` that `B[x]`
-implies `C`, and we know for some `x` of type `A` that `B[x]` holds,
+In other words, if we know for every `x` of type `A` that `B x`
+implies `C`, and we know for some `x` of type `A` that `B x` holds,
 then we may conclude that `C` holds.  This is because we may
-instantiate that proof that `∀ (x : A) → B[x] → C` to any `x`, and we
-may choose the particular `x` provided by the evidence that `∃ (λ (x :
-A) → B[x])`.
+instantiate that proof that `∀ (x : A) → B x → C` to any value
+`M` of type `A` and any `N` of type `B M`, and exactly such values
+are provided by the evidence for `∃ (λ (x : A) → B x)`.
 
-
-[It would be better to have even and odd as an exercise.  Is there
-a simpler example that I could start with?]
+Agda makes it possible to define our own syntactic abbreviations.
+\begin{code}
+syntax ∃ {A} (λ x → B) = ∃[ x ∈ A ] B
+\end{code}
+This allows us to write `∃[ x ∈ A ] (B x)` in place of
+`∃ (λ (x : A) → B x)`.
 
 As an example, recall the definitions of `even` from
 Chapter [Relations](Relations).  
diff --git a/src/extra/Exists.agda b/src/extra/Exists.agda
new file mode 100644
index 00000000..d3bbd2a2
--- /dev/null
+++ b/src/extra/Exists.agda
@@ -0,0 +1,54 @@
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; sym; trans; cong)
+open Eq.≡-Reasoning
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
+open import Data.Nat.Properties.Simple using (+-suc; +-right-identity)
+open import Relation.Nullary using (¬_)
+open import Function using (_∘_)
+open import Data.Product using (_×_; _,_; proj₁; proj₂)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+
+data ∃ {A : Set} (B : A → Set) : Set where
+  _,_ : (x : A) → B x → ∃ B
+
+syntax ∃ {A} (λ x → B) = ∃[ x ∈ A ] B
+
+
+data even : ℕ → Set
+data odd  : ℕ → Set
+
+data even where
+  even-zero : even zero
+  even-suc  : ∀ {n : ℕ} → odd n → even (suc n)
+
+data odd where
+  odd-suc   : ∀ {n : ℕ} → even n → odd (suc n)
+
+lemma : ∀ (m : ℕ) →  2 * suc m ≡ suc (suc (2 * m))
+lemma m =
+  begin
+    2 * suc m
+  ≡⟨⟩
+    suc m + (suc m + zero)
+  ≡⟨⟩
+    suc (m + (suc (m + zero)))
+  ≡⟨ cong suc (+-suc m (m + zero)) ⟩
+    suc (suc (m + (m + zero)))
+  ≡⟨⟩
+    suc (suc (2 * m))
+  ∎
+
+∃-even : ∀ {n : ℕ} → even n → ∃[ m ∈ ℕ ] (n ≡ 2 * m)
+∃-odd  : ∀ {n : ℕ} →  odd n → ∃[ m ∈ ℕ ] (n ≡ 1 + 2 * m)
+
+∃-even even-zero =  zero , refl
+∃-even (even-suc o) with ∃-odd o
+...                    | m , eqn rewrite eqn = suc m , sym (lemma m)
+
+∃-odd  (odd-suc e)  with ∃-even e
+...                    | m , eqn rewrite eqn = m , refl
+
+∃-even′ : ∀ {n : ℕ} → even n → ∃[ m ∈ ℕ ] (n ≡ 2 * m)
+∃-even′ even-zero =  zero , refl
+∃-even′ (even-suc o) with ∃-odd o
+...                    | m , eqn rewrite eqn | cong suc (+-right-identity m) = suc m , {!!}
diff --git a/src/extra/RewriteWTF.agda b/src/extra/RewriteWTF.agda
new file mode 100644
index 00000000..1a247e34
--- /dev/null
+++ b/src/extra/RewriteWTF.agda
@@ -0,0 +1,36 @@
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; sym; trans; cong)
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
+open import Data.Nat.Properties.Simple using (+-suc)
+open import Data.Product using (∃; ∃-syntax; _,_)
+
+data even : ℕ → Set
+data odd  : ℕ → Set
+
+data even where
+  even-zero : even zero
+  even-suc  : ∀ {n : ℕ} → odd n → even (suc n)
+
+data odd where
+  odd-suc   : ∀ {n : ℕ} → even n → odd (suc n)
+
+∃-even : ∀ {n : ℕ} → even n → ∃[ m ] (n ≡ 2 * m)
+∃-odd  : ∀ {n : ℕ} →  odd n → ∃[ m ] (n ≡ 1 + 2 * m)
+
+∃-even even-zero =  zero , refl
+∃-even (even-suc o) with ∃-odd o
+...                    | m , eqn rewrite eqn | sym (+-suc m (m + 0)) = suc m , refl
+
+∃-odd  (odd-suc e)  with ∃-even e
+...                    | m , eqn rewrite eqn = m , refl
+
+∃-even′ : ∀ {n : ℕ} → even n → ∃[ m ] (n ≡ 2 * m)
+∃-odd′  : ∀ {n : ℕ} →  odd n → ∃[ m ] (n ≡ 1 + 2 * m)
+
+∃-even′ even-zero =  zero , refl
+∃-even′ (even-suc o) with ∃-odd′ o
+...                     | m , eqn rewrite eqn | +-suc m (m + 0) = suc m , ?
+
+∃-odd′  (odd-suc e)  with ∃-even′ e
+...                     | m , eqn rewrite eqn = m , refl
+