Fixed some typos (#519)

src/plfa/part2/BigStep.lagda.md

@@ -215,7 +215,7 @@ sub-id = plfa.part2.Substitution.sub-id
 ```
 
 
-We define an auxilliary function for extending a substitution.
+We define an auxiliary function for extending a substitution.
 
 ```
 ext-subst : ∀{Γ Δ} → Subst Γ Δ → Δ ⊢ ★ → Subst (Γ , ★) Δ
@@ -393,7 +393,7 @@ underneath lambda abstractions via the `ζ` rule. The call-by-name
 semantics does not reduce under lambda, so a straightforward proof by
 induction on the reduction sequence is impossible.  In the article
 _Call-by-name, call-by-value, and the λ-calculus_, Plotkin proves the
-theorem in two steps, using two auxilliary reduction relations. The
+theorem in two steps, using two auxiliary reduction relations. The
 first step uses a classic technique called Curry-Feys standardisation.
 It relies on the notion of _standard reduction sequence_, which acts
 as a half-way point between full beta reduction and call-by-name by

src/plfa/part2/Confluence.lagda.md

@@ -49,7 +49,7 @@ diamond property. Here is a counter example.
 Both terms can reduce to `a a`, but the second term requires two steps
 to get there, not one.
 
-To side-step this problem, we'll define an auxilliary reduction
+To side-step this problem, we'll define an auxiliary reduction
 relation, called _parallel reduction_, that can perform many
 reductions simultaneously and thereby satisfy the diamond property.
 Furthermore, we show that a parallel reduction sequence exists between
@@ -407,7 +407,7 @@ The heart of the confluence proof is made of stone, or rather, of
 diamond!  We show that parallel reduction satisfies the diamond
 property: that if `M ⇛ N` and `M ⇛ N′`, then `N ⇛ L` and `N′ ⇛ L` for
 some `L`.  The typical proof is an induction on `M ⇛ N` and `M ⇛ N′`
-so that every possible pair gives rise to a witeness `L` given by
+so that every possible pair gives rise to a witness `L` given by
 performing enough beta reductions in parallel.
 
 However, a simpler approach is to perform as many beta reductions in
@@ -611,7 +611,7 @@ confluence L↠M₁ L↠M₂
 ## Notes
 
 Broadly speaking, this proof of confluence, based on parallel
-reduction, is due to W. Tait and P. Martin-Lof (see Barendredgt 1984,
+reduction, is due to W. Tait and P. Martin-Löf (see Barendredgt 1984,
 Section 3.2).  Details of the mechanization come from several sources.
 The `subst-par` lemma is the "strong substitutivity" lemma of Shafer,
 Tebbi, and Smolka (ITP 2015). The proofs of `par-triangle`, `strip`,

src/plfa/part2/DeBruijn.lagda.md

@@ -574,7 +574,7 @@ bound variable.
 Whereas before renaming was a result that carried evidence
 that a term is well typed in one context to evidence that it
 is well typed in another context, now it actually transforms
-the term, suitably altering the bound variables. Typechecking
+the term, suitably altering the bound variables. Type checking
 the code in Agda ensures that it is only passed and returns
 terms that are well typed by the rules of simply-typed lambda
 calculus.

src/plfa/part2/Inference.lagda.md

@@ -618,7 +618,7 @@ Consider the context:
 
   + If they differ, we recurse:
 
-    - If lookup fails, we apply `ext∋` to conver the proof
+    - If lookup fails, we apply `ext∋` to convert the proof
       there is no derivation from the contained context
       to the extended context.
 

src/plfa/part2/Subtyping.lagda.md

@@ -1235,7 +1235,7 @@ Come up with an algorithmic subtyping rule for variant types.
 
 #### Exercise `<:-alternative` (stretch)
 
-Revise this formalization of records with subtyping (including proofs
+Revise this formalisation of records with subtyping (including proofs
 of progress and preservation) to use the non-algorithmic subtyping
 rules for Chapter 15 of Types and Programming Languages, which we list here: