diff --git a/extra/stlc/TinyLambda.lagda b/extra/stlc/TinyLambda.lagda
new file mode 100644
index 00000000..d8d9f678
--- /dev/null
+++ b/extra/stlc/TinyLambda.lagda
@@ -0,0 +1,149 @@
+## Imports
+
+\begin{code}
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; sym; trans; cong)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Nat using (ℕ; zero; suc; _+_; _∸_)
+open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
+open import Data.Unit using (⊤; tt)
+open import Function using (_∘_)
+open import Function.Equivalence using (_⇔_; equivalence)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+\end{code}
+
+Tiny lambda calculus
+\begin{code}
+module Source where
+
+  infix  4 _⊢_
+  infix  4 _∋_
+  infixl 5 _,_
+  infix  5 ƛ_
+  infixr 7 _⇒_
+  infixl 7 _·_
+  infix  9 `_
+  infix  9 S_
+
+  data Type : Set where
+    _⇒_ : Type → Type → Type
+    o   : Type
+
+  data Context : Set where
+    ∅   : Context
+    _,_ : Context → Type → Context
+
+  data _∋_ : Context → Type → Set where
+
+    Z : ∀ {Γ A}
+        ----------
+      → Γ , A ∋ A
+
+    S_ : ∀ {Γ A B}
+      → Γ ∋ A
+        ---------
+      → Γ , B ∋ A
+
+  data _⊢_ : Context → Type → Set where
+
+    `_ : ∀ {Γ} {A}
+      → Γ ∋ A
+        ------
+      → Γ ⊢ A
+
+    ƛ_  :  ∀ {Γ} {A B}
+      → Γ , A ⊢ B
+        ----------
+      → Γ ⊢ A ⇒ B
+
+    _·_ : ∀ {Γ} {A B}
+      → Γ ⊢ A ⇒ B
+      → Γ ⊢ A
+        ----------
+      → Γ ⊢ B
+
+  ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
+      ----------------------------------
+    → (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
+  ext ρ Z      =  Z
+  ext ρ (S x)  =  S (ρ x)
+
+  rename : ∀ {Γ Δ}
+    → (∀ {A} → Γ ∋ A → Δ ∋ A)
+      ------------------------
+    → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
+  rename ρ (` x)          =  ` (ρ x)
+  rename ρ (ƛ N)          =  ƛ (rename (ext ρ) N)
+  rename ρ (L · M)        =  (rename ρ L) · (rename ρ M)
+
+  exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A)
+      ----------------------------------
+    → (∀ {A B} → Γ , B ∋ A → Δ , B ⊢ A)
+  exts σ Z      =  ` Z
+  exts σ (S x)  =  rename S_ (σ x)
+
+  subst : ∀ {Γ Δ}
+    → (∀ {A} → Γ ∋ A → Δ ⊢ A)
+      ------------------------
+    → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
+  subst σ (` k)          =  σ k
+  subst σ (ƛ N)          =  ƛ (subst (exts σ) N)
+  subst σ (L · M)        =  (subst σ L) · (subst σ M)
+
+  _[_] : ∀ {Γ A B}
+          → Γ , B ⊢ A
+          → Γ ⊢ B 
+            ---------
+          → Γ ⊢ A
+  _[_] {Γ} {A} {B} N M =  subst {Γ , B} {Γ} σ {A} N
+    where
+    σ : ∀ {A} → Γ , B ∋ A → Γ ⊢ A
+    σ Z      =  M
+    σ (S x)  =  ` x
+
+  data Value : ∀ {Γ A} → Γ ⊢ A → Set where
+
+    V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B}
+        ---------------------------
+      → Value (ƛ N)
+
+  infix 2 _—→_
+
+  data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+
+    ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
+      → L —→ L′
+        -----------------
+      → L · M —→ L′ · M
+
+    ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
+      → Value V
+      → M —→ M′
+        --------------
+      → V · M —→ V · M′
+
+    β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
+      → Value W
+        -------------------
+      → (ƛ N) · W —→ N [ W ]
+
+  infix  2 _—↠_
+  infix 1 begin_
+  infixr 2 _—→⟨_⟩_
+  infix 3 _∎
+
+  data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+
+    _∎ : ∀ {Γ A} (M : Γ ⊢ A)
+        --------
+      → M —↠ M
+
+    _—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
+      → L —→ M
+      → M —↠ N
+        ---------
+      → L —↠ N
+
+  begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A} → (M —↠ N) → (M —↠ N)
+  begin M—↠N = M—↠N
+\end{code}
diff --git a/src/plta/Isomorphism.lagda b/src/plta/Isomorphism.lagda
index ec3a8954..dba6c9e1 100644
--- a/src/plta/Isomorphism.lagda
+++ b/src/plta/Isomorphism.lagda
@@ -391,7 +391,7 @@ import Function.LeftInverse using (_↞_)
 \end{code}
 Here `_↔_` corresponds to our `_≃_`, and `_↞_` corresponds to our `_≲_`.
 However, we stick with our definitions, because those in the
-standard library are less convenient to use: they use a nested record structure,
+standard library are less convenient: they depend on a nested record structure,
 and are parameterised with regard to an arbitrary notion of equivalence.
 
 ## Unicode
diff --git a/src/plta/Lambda.lagda b/src/plta/Lambda.lagda
index b6c90214..a852393d 100644
--- a/src/plta/Lambda.lagda
+++ b/src/plta/Lambda.lagda
@@ -690,18 +690,19 @@ It can be illustrated as follows.
 Here `L`, `M`, `N` are universally quantified while `P`
 is existentially quantified.  If each line stand for zero
 or more reduction steps, this is called confluence,
-while if each line stands a single reduction step it is
-called the _diamond property_.  In symbols:
+while if the top two lines stand for a single reduction
+step and the bottom two stand for zero or more reduction
+steps it is called the diamond property. In symbols:
 
     confluence : ∀ {L M N} → ∃[ P ]
       ( ((L —↠ M) × (L —↠ N))
         --------------------
-      → ((M —↠ P) × (M —↠ P)) )
+      → ((M —↠ P) × (N —↠ P)) )
 
     diamond : ∀ {L M N} → ∃[ P ]
-      ( ((L —↠ M) × (L —↠ N))
+      ( ((L —→ M) × (L —→ N))
         --------------------
-      → ((M —↠ P) × (M —↠ P)) )
+      → ((M —↠ P) × (N —↠ P)) )
 
 All of the reduction systems studied in this text are determistic.
 In symbols:
diff --git a/src/plta/More.lagda b/src/plta/More.lagda
index 930501ba..1d720430 100644
--- a/src/plta/More.lagda
+++ b/src/plta/More.lagda
@@ -8,6 +8,16 @@ permalink : /More/
 module plta.More where
 \end{code}
 
+So far, we have focussed on a relatively minimal language,
+based on Plotkin's PCF, which supports functions, naturals, and
+fixpoints.  In this chapter we extend our calculus to support
+more datatypes, including products, sums, unit type, empty
+type, and lists, all of which will be familiar from Part I of
+this textbook.  We also describe _let_ bindings.  Most of the
+description will be informal.  We show how to formalise a few
+of the constructs, but leave the rest as an exercise for the
+reader.
+
 
 ## Imports
 
@@ -21,9 +31,6 @@ open import Data.Unit using (⊤; tt)
 open import Function using (_∘_)
 open import Function.Equivalence using (_⇔_; equivalence)
 open import Relation.Nullary using (¬_; Dec; yes; no)
-open import Relation.Nullary.Decidable using (map)
-open import Relation.Nullary.Negation using (contraposition)
-open import Relation.Nullary.Product using (_×-dec_)
 \end{code}
 
 
@@ -601,3 +608,10 @@ normalise (suc g) L with progress L
 ...    | step {M} L⟶M with normalise g M
 ...        | normal h M⟶*N                =  normal (suc h) (L ⟶⟨ L⟶M ⟩ M⟶*N)
 \end{code}
+
+
+## Bisimulation
+
+
+
+\end{code}