diff --git a/src/plfa/part3/Compositional.lagda.md b/src/plfa/part3/Compositional.lagda.md
index c8f559270..66f17f8c8 100644
--- a/src/plfa/part3/Compositional.lagda.md
+++ b/src/plfa/part3/Compositional.lagda.md
@@ -230,7 +230,7 @@ We proceed by induction on the semantics.
     * Suppose `γ ⊢ L ↓ v₁′ ↦ v₁`, `γ ⊢ M ↓ v₁′`, and `v₂ ⊑ ⊥`.
       We have `γ ⊢ L ↓ v₁′ ↦ (v₁ ⊔ v₂)` by rule `sub`
       because `v₁′ ↦ (v₁ ⊔ v₂) ⊑ v₁′ ↦ v₁`.
-    * Suppose `γ ⊢ L ↓ v₁′′ ↦ v₁, γ ⊢ M ↓ v₁′′`,
+    * Suppose `γ ⊢ L ↓ v₁′′ ↦ v₁`, `γ ⊢ M ↓ v₁′′`,
       `γ ⊢ L ↓ v₁′ ↦ v₂`, and `γ ⊢ M ↓ v₁′`.
       This case is the most interesting.
       By two uses of the rule `⊔-intro` we have
diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md
index 018327cd8..5133333e7 100644
--- a/src/plfa/part3/Denotational.lagda.md
+++ b/src/plfa/part3/Denotational.lagda.md
@@ -402,9 +402,9 @@ we'll name `v`. Then for the second application,
 `f` must map `v` to some value. Let's name it `w`. So the function's
 table must include two entries, both `u ↦ v` and `v ↦ w`. For each
 application of the table, we extract the appropriate entry from it
-using the `sub` rule.  In particular, we use the ⊑-conj-R1 and
-⊑-conj-R2 to select `u ↦ v` and `v ↦ w`, respectively, from the table
-`u ↦ v ⊔ v ↦ w`. So the meaning of twoᶜ is that it takes this table
+using the `sub` rule.  In particular, we use the `⊑-conj-R1` and
+`⊑-conj-R2` to select `u ↦ v` and `v ↦ w`, respectively, from the table
+`u ↦ v ⊔ v ↦ w`. So the meaning of `twoᶜ` is that it takes this table
 and parameter `u`, and it returns `w`.  Indeed we derive this as
 follows.
 
@@ -563,7 +563,7 @@ Denotational equality is an equivalence relation.
                         (λ z → proj₂ (eq1 γ v) (proj₂ (eq2 γ v) z)) ⟩
 ```
 
-Two terms `M` and `N` are denotational equal when their denotations are
+Two terms `M` and `N` are denotationally equal when their denotations are
 equal, that is, `ℰ M ≃ ℰ N`.
 
 The following submodule introduces equational reasoning for the `≃`
@@ -1093,7 +1093,7 @@ The crux of the proof is the case for `⊑-trans`.
         u₁ ⊑ u₂
 
 By the induction hypothesis for `u₁ ⊑ u`, we know
-that `v ↦ w factors u into u′`, for some value `u′`,
+that `v ↦ w` factors `u` into `u′`, for some value `u′`,
 so we have `all-funs u′` and `u′ ⊆ u`.
 By the induction hypothesis for `u ⊑ u₂`, we know
 that for any `v′ ↦ w′ ∈ u`, `v′ ↦ w′` factors `u₂` into `u₃`.