diff --git a/index.md b/index.md
index 45aca764..0176745a 100644
--- a/index.md
+++ b/index.md
@@ -23,6 +23,9 @@ http://homepages.inf.ed.ac.uk/wadler/
 
   - [Naturals: Natural numbers]({{ "/Naturals" | relative_url }})
   - [Properties: Proof by induction]({{ "/Properties" | relative_url }})
+  - [PropertiesEx: Solutions to exercises]({{ "/PropertiesEx" | relative_url }})
+  - [Relations: Inductive Definition of Relations]({{ "/Relations" | relative_url }})
+  - [RelationsEx: Solutions to exercises]({{ "/RelationsEx" | relative_url }})
   - [Maps: Total and Partial Maps]({{ "/Maps" | relative_url }})
   - [Stlc: The Simply Typed Lambda-Calculus]({{ "/Stlc" | relative_url }})
   - [StlcProp: Properties of STLC]({{ "/StlcProp" | relative_url }})
diff --git a/src/Logic.lagda b/src/Logic.lagda
new file mode 100644
index 00000000..38b38661
--- /dev/null
+++ b/src/Logic.lagda
@@ -0,0 +1,170 @@
+---
+title     : "Logic: Propositions as Type"
+layout    : page
+permalink : /Logic
+---
+
+This chapter describes the connection between logical connectives
+(conjunction, disjunction, implication, for all, there exists,
+equivalence) and datatypes (product, sum, function, dependent
+function, dependent product, Martin Löf equivalence).
+
+## Imports
+
+\begin{code}
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+\end{code}
+
+## Conjunction
+
+Given two propositions `A` and `B`, the conjunction `A × B` holds
+if both `A` holds and `B` holds.  We formalise this idea by
+declaring a suitable inductive type.
+\begin{code}
+data _×_ : Set → Set → Set where
+  _,_ : ∀ {A B : Set} → A → B → A × B
+\end{code}
+If `A` and `B` are propositions then `A × B` is
+also a proposition.  Evidence that `A × B` holds is of the form
+`a , b`, where `a` is evidence that `A` holds and
+`b` is evidence that `B` holds.
+
+We set the precedence of conjunction so that it binds less
+tightly than anything save disjunction, and of the pairing
+operator so that it binds less tightly than any arithmetic
+operator.
+\begin{code}
+infixr 2 _×_
+infixr 4 _,_
+\end{code}
+
+
+
+## Disjunction
+
+Given two propositions `A` and `B`, the disjunction `A ⊎ B` holds
+if either `A` holds or `B` holds.  We formalise this idea by
+declaring a suitable inductive type.
+\begin{code}
+data _⊎_ : Set → Set → Set where
+  inj₁  : ∀ {A B : Set} → A → A ⊎ B
+  inj₂ : ∀ {A B : Set} → B → A ⊎ B
+\end{code}
+If `A` and `B` are propositions then `A ⊎ B` is
+also a proposition.  Evidence that `A ⊎ B` holds is either of the form
+`inj₁ a`, where `a` is evidence that `A` holds, or `inj₂ b`, where
+`b` is evidence that `B` holds.
+
+We set the precedence of disjunction so that it binds less tightly
+than any other operator.
+\begin{code}
+infix 1 _⊎_
+\end{code}
+Thus, `m ≤ n ⊎ n ≤ m` parses as `(m ≤ n) ⊎ (n ≤ m)`,
+and `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`.
+
+## Distribution
+
+Distribution of `×` over `⊎` is an isomorphism.
+\begin{code}
+data _≃_ : Set → Set → Set where
+  iso : ∀ {A B : Set} → (f : A → B) → (g : B → A) →
+          (∀ (x : A) → g (f x) ≡ x) → (∀ (y : B) → f (g y) ≡ y) → A ≃ B
+
+×-distributes-+ : ∀ {A B C : Set} → ((A ⊎ B) × C) ≃ ((A × C) ⊎ (B × C))
+×-distributes-+ = iso f g gf fg
+  where
+
+  f : ∀ {A B C : Set} → (A ⊎ B) × C → (A × C) ⊎ (B × C)
+  f (inj₁ a , c) = inj₁ (a , c)
+  f (inj₂ b , c) = inj₂ (b , c)
+
+  g : ∀ {A B C : Set} → (A × C) ⊎ (B × C) → (A ⊎ B) × C
+  g (inj₁ (a , c)) = (inj₁ a , c)
+  g (inj₂ (b , c)) = (inj₂ b , c)
+
+  gf : ∀ {A B C : Set} → (x : (A ⊎ B) × C) → g (f x) ≡ x
+  gf (inj₁ a , c) = refl
+  gf (inj₂ b , c) = refl
+
+  fg : ∀ {A B C : Set} → (y : (A × C) ⊎ (B × C)) → f (g y) ≡ y
+  fg (inj₁ (a , c)) = refl
+  fg (inj₂ (b , c)) = refl
+\end{code}
+
+Distribution of `⊎` over `×` is half an isomorphism.
+\begin{code}
+data _≃ʳ_ : Set → Set → Set where
+  isoʳ : ∀ {A B : Set} → (f : A → B) → (g : B → A) →
+          (∀ (x : A) → g (f x) ≡ x) → A ≃ʳ B
+
++-distributes-× : ∀ {A B C : Set} → ((A × B) ⊎ C) ≃ʳ ((A ⊎ C) × (B ⊎ C))
++-distributes-× =  isoʳ f g gf
+  where
+
+  f : ∀ {A B C : Set} → (A × B) ⊎ C → (A ⊎ C) × (B ⊎ C)
+  f (inj₁ (a , b)) = (inj₁ a , inj₁ b)
+  f (inj₂ c) = (inj₂ c , inj₂ c)
+
+  g : ∀ {A B C : Set} → (A ⊎ C) × (B ⊎ C) → (A × B) ⊎ C
+  g (inj₁ a , inj₁ b) = inj₁ (a , b)
+  g (inj₁ a , inj₂ c) = inj₂ c
+  g (inj₂ c , inj₁ b) = inj₂ c
+  g (inj₂ c , inj₂ c′) = inj₂ c  -- or inj₂ c′
+
+  gf : ∀ {A B C : Set} → (x : (A × B) ⊎ C) → g (f x) ≡ x
+  gf (inj₁ (a , b)) = refl
+  gf (inj₂ c) = refl
+\end{code}
+
+## True
+
+\begin{code}
+data ⊤ : Set where
+  tt : ⊤
+\end{code}
+
+## False
+
+\begin{code}
+data ⊥ : Set where
+  -- no clauses!  
+
+⊥-elim : {A : Set} → ⊥ → A
+⊥-elim ()
+\end{code}
+
+## Implication
+
+## Negation
+
+\begin{code}
+¬_ : Set → Set
+¬ A = A → ⊥
+
+infix 3 ¬_
+
+data Dec : Set → Set where
+  yes : ∀ {A : Set} → A → Dec A
+  no  : ∀ {A : Set} → (¬ A) → Dec A
+
+contraposition : ∀ {A B : Set} → (A → B) → (¬ B → ¬ A)
+contraposition f ¬b a = ¬b (f a)
+\end{code}
+
+
+
+## Intuitive and Classical logic
+
+## Universals
+
+## Existentials
+
+## Equivalence
+
+## Unicode
+
+This chapter introduces the following unicode.
+
+    ≤  U+2264  LESS-THAN OR EQUAL TO (\<=, \le)
+    
diff --git a/src/Naturals.lagda b/src/Naturals.lagda
index 52b19305..10cb8a54 100644
--- a/src/Naturals.lagda
+++ b/src/Naturals.lagda
@@ -563,8 +563,9 @@ of the logarithms of *m* and *n*.
 
 ## Unicode
 
-In each chapter, we will list at the end all unicode characters.
-In this chapter we use the following.
+In each chapter, we will list at the end all unicode characters that
+first appear in that chapter.  This chapter introduces the following
+unicode.
 
     ℕ  U+2115  DOUBLE-STRUCK CAPITAL N (\bN)  
     →  U+2192  RIGHTWARDS ARROW (\to, \r)
diff --git a/src/Properties.lagda b/src/Properties.lagda
index 012317ab..3bf164a6 100644
--- a/src/Properties.lagda
+++ b/src/Properties.lagda
@@ -616,7 +616,7 @@ right.
 
 ## Unicode
 
-In this chapter we introduced the following unicode.
+This chapter introduces the following unicode.
 
     ≡  U+2261  IDENTICAL TO (\==)
     ∀  U+2200  FOR ALL (\forall)
diff --git a/src/Relations.lagda b/src/Relations.lagda
index 78ce3d5d..1d06910d 100644
--- a/src/Relations.lagda
+++ b/src/Relations.lagda
@@ -481,7 +481,7 @@ the keyword `where`. -->
 
 ## Unicode
 
-In this chapter we use the following unicode.
+This chapter introduces the following unicode.
 
     ≤  U+2264  LESS-THAN OR EQUAL TO (\<=, \le)
     ˡ  U+02E1  MODIFIER LETTER SMALL L (\^l)
diff --git a/src/EvenOdd.agda b/src/extra/EvenOdd.agda
similarity index 83%
rename from src/EvenOdd.agda
rename to src/extra/EvenOdd.agda
index f8ab288a..9fdf2e0f 100644
--- a/src/EvenOdd.agda
+++ b/src/extra/EvenOdd.agda
@@ -21,12 +21,9 @@ mutual
   data odd : ℕ → Set where
     suc : ∀ {n : ℕ} → even n → odd (suc n)
 
-+-lemma : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + (suc m + 0)
++-lemma : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + suc (m + 0)
 +-lemma m rewrite +-identity m | +-suc m m = refl
 
-+-lemma′ : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + (suc m + 0)
-+-lemma′ m rewrite +-suc m (m + 0) = {!!}
-
 mutual
   is-even : ∀ (n : ℕ) → even n → ∃(λ (m : ℕ) → n ≡ 2 * m)
   is-even zero zero =  zero , refl
@@ -36,3 +33,12 @@ mutual
   is-odd : ∀ (n : ℕ) → odd n → ∃(λ (m : ℕ) → n ≡ 1 + 2 * m)
   is-odd (suc n) (suc evenn) with is-even n evenn
   ... | m , n≡2*m rewrite n≡2*m = m , refl
+
++-lemma′ : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + suc (m + 0)
++-lemma′ m rewrite +-suc m (m + 0) = {!!}
+
+is-even′ : ∀ (n : ℕ) → even n → ∃(λ (m : ℕ) → n ≡ 2 * m)
+is-even′ zero zero =  zero , refl
+is-even′ (suc n) (suc oddn) with is-odd n oddn
+... | m , n≡1+2*m rewrite n≡1+2*m | +-identity m | +-suc m m = suc m , {!!}
+