Merge pull request #518 from h4iku/fix-typo

Fixed some typos.

Thanks h4iku!

src/plfa/part3/Adequacy.lagda.md

@@ -100,7 +100,7 @@ open import plfa.part3.Soundness using (soundness)
 ## The property of being greater or equal to a function
 
 We define the following short-hand for saying that a value is
-greather-than or equal to a function value.
+greater-than or equal to a function value.
 
 ```
 above-fun : Value → Set
@@ -417,7 +417,7 @@ sub-𝕍 {c} {v ↦ w ⊔ v ↦ w'} ⟨ vcw , vcw' ⟩ ⊑-dist ev1c ⟨ v' ,
 
         𝕍 (v ↦ (w ⊔ w')) (clos (ƛ N) γ)
 
-  Let `c` be an arbtrary closure such that `𝔼 v c`.
+  Let `c` be an arbitrary closure such that `𝔼 v c`.
   Assume `w ⊔ w'` is greater than a function.
   Unfortunately, this does not mean that both `w` and `w'`
   are above functions. But thanks to the lemma `above-fun-⊔`,

src/plfa/part3/Denotational.lagda.md

@@ -638,7 +638,7 @@ of the following shape.
 The compositionality property is not trivial because the semantics we
 have defined includes three rules that are not syntax directed:
 `⊥-intro`, `⊔-intro`, and `sub`. The above equations suggest that the
-dentoational semantics can be defined as a recursive function, and
+denotational semantics can be defined as a recursive function, and
 indeed, we give such a definition and prove that it is equivalent to
 ℰ.
 
@@ -685,7 +685,7 @@ is called _adequacy_ in the literature.
 
     ℰ M ≃ ℰ (ƛ N)  implies M —↠ ƛ N′ for some N′
 
-The fourth chapter applies the results of the three preceeding
+The fourth chapter applies the results of the three preceding
 chapters (compositionality, soundness, and adequacy) to prove that
 denotational equality implies a property called _contextual
 equivalence_. This property is important because it justifies the use
@@ -823,7 +823,7 @@ D^suc zero (a[0] ∷ []) = ⊥
 D^suc (suc i) (a[i+1] ∷ a[i] ∷ ls) =  a[i] ↦ a[i+1]  ⊔  D^suc i (a[i] ∷ ls)
 ```
 
-We use the following auxilliary function to obtain the last element of
+We use the following auxiliary function to obtain the last element of
 a non-empty vector. (This formulation is more convenient for our
 purposes than the one in the Agda standard library.)
 
@@ -857,9 +857,9 @@ Dᶜ n (a[n] ∷ ls) = (D^suc n (a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦
 The exercise is to prove that for any path `ls`, the meaning of the
 Church numeral `n` is `Dᶜ n ls`.
 
-To fascilitate talking about arbitrary Church numerals, the following
+To facilitate talking about arbitrary Church numerals, the following
 `church` function builds the term for the nth Church numeral,
-using the auxilliary function `apply-n`.
+using the auxiliary function `apply-n`.
 
 ```
 apply-n : (n : ℕ) → ∅ , ★ , ★ ⊢ ★

src/plfa/part3/Soundness.lagda.md

@@ -226,10 +226,10 @@ The main challenge is dealing with the substitution in β reduction:
 We have that `γ ⊢ N [ M ] ↓ v` and need to show that
 `γ ⊢ (ƛ N) · M ↓ v`. Now consider the derivation of `γ ⊢ N [ M ] ↓ v`.
 The term `M` may occur 0, 1, or many times inside `N [ M ]`. At each of
-those occurences, `M` may result in a different value. But to build a
+those occurrences, `M` may result in a different value. But to build a
 derivation for `(ƛ N) · M`, we need a single value for `M`.  If `M`
-occured more than 1 time, then we can join all of the different values
-using `⊔`. If `M` occured 0 times, then we do not need any information
+occurred more than 1 time, then we can join all of the different values
+using `⊔`. If `M` occurred 0 times, then we do not need any information
 about `M` and can therefore use `⊥` for the value of `M`.