diff --git a/extra/extra/Lambda-new.lagda b/extra/extra/Lambda-new.lagda
index fc45fb41..3d5c98ab 100644
--- a/extra/extra/Lambda-new.lagda
+++ b/extra/extra/Lambda-new.lagda
@@ -460,7 +460,7 @@ we yield `V`, otherwise we yield `x` unchanged.
 
 * For abstractions, we compare `w`, the variable we are substituting for,
 with `x`, the variable bound in the abstraction. If they are the same,
-we yield the abstraction unchanged, otherwise we subsititute inside the body.
+we yield the abstraction unchanged, otherwise we substitute inside the body.
 
 * For application, we recursively substitute in the function
 and the argument.
@@ -919,7 +919,7 @@ For example
 
 give us the types associated with variables ` "z" ` and ` "s" `, respectively.
 The symbol `∋` (pronounced "ni", for "in" backwards) is chosen because
-checking that `Γ ∋ x ⦂ A` is anologous to checking whether `x ⦂ A` appears
+checking that `Γ ∋ x ⦂ A` is analogous to checking whether `x ⦂ A` appears
 in a list corresponding to `Γ`.
 
 If two variables in a context have the same name, then lookup
diff --git a/extra/stlc/StlcNew.lagda b/extra/stlc/StlcNew.lagda
index 726a1680..1e2e2eb9 100644
--- a/extra/stlc/StlcNew.lagda
+++ b/extra/stlc/StlcNew.lagda
@@ -360,7 +360,7 @@ we yield `V`, otherwise we yield `x` unchanged.
 
 * For abstractions, we compare `w`, the variable we are substituting for,
 with `x`, the variable bound in the abstraction. If they are the same,
-we yield the abstraction unchanged, otherwise we subsititute inside the body.
+we yield the abstraction unchanged, otherwise we substitute inside the body.
 
 In all other cases, we push substitution recursively into
 the subterms.
diff --git a/extra/stlc/StlcOld.lagda b/extra/stlc/StlcOld.lagda
index 05490b7f..7b71c8d1 100644
--- a/extra/stlc/StlcOld.lagda
+++ b/extra/stlc/StlcOld.lagda
@@ -402,7 +402,7 @@ we yield `V`, otherwise we yield `x′` unchanged.
 
 * For abstractions, we compare `x`, the variable we are substituting for,
 with `x′`, the variable bound in the abstraction. If they are the same,
-we yield abstraction unchanged, otherwise we subsititute inside the body.
+we yield abstraction unchanged, otherwise we substitute inside the body.
 
 In all other cases, we push substitution recursively into
 the subterms.
diff --git a/src/plfa/Lambda.lagda b/src/plfa/Lambda.lagda
index 7e350c8d..6e6ce1a8 100644
--- a/src/plfa/Lambda.lagda
+++ b/src/plfa/Lambda.lagda
@@ -209,7 +209,7 @@ definition may use `plusᶜ` as defined earlier (or may not
 
 #### Exercise `primed` (stretch)
 
-We can make examples with lambda terms slighly easier to write
+We can make examples with lambda terms slightly easier to write
 by adding the following definitions:
 \begin{code}
 ƛ′_⇒_ : Term → Term → Term
@@ -466,7 +466,7 @@ we yield `V`, otherwise we yield `x` unchanged.
 
 * For abstractions, we compare `y`, the substituted variable,
 with `x`, the variable bound in the abstraction. If they are the same,
-we yield the abstraction unchanged, otherwise we subsititute inside the body.
+we yield the abstraction unchanged, otherwise we substitute inside the body.
 
 * For application, we recursively substitute in the function
 and the argument.
@@ -758,7 +758,7 @@ steps it is called the diamond property. In symbols:
         --------------------
       → ((M —↠ P) × (N —↠ P)) )
 
-All of the reduction systems studied in this text are determistic.
+All of the reduction systems studied in this text are deterministic.
 In symbols:
 
     deterministic : ∀ {L M N}
@@ -987,7 +987,7 @@ For example,
 
 give us the types associated with variables `` "z" `` and `` "s" ``,
 respectively.  The symbol `∋` (pronounced "ni", for "in"
-backwards) is chosen because checking that `Γ ∋ x ⦂ A` is anologous to
+backwards) is chosen because checking that `Γ ∋ x ⦂ A` is analogous to
 checking whether `x ⦂ A` appears in a list corresponding to `Γ`.
 
 If two variables in a context have the same name, then lookup
diff --git a/tspl/Assignment3.lagda b/tspl/Assignment3.lagda
index a26b2149..faa38d51 100644
--- a/tspl/Assignment3.lagda
+++ b/tspl/Assignment3.lagda
@@ -251,7 +251,7 @@ two natural numbers.
 
 #### Exercise `primed` (stretch)
 
-We can make examples with lambda terms slighly easier to write
+We can make examples with lambda terms slightly easier to write
 by adding the following definitions.
 \begin{code}
 ƛ′_⇒_ : Term → Term → Term