Merge pull request #562 from lacrosse/typos-and-additions

Fix typos and add a missing Unicode symbol

src/plfa/part1/Decidable.lagda.md

@@ -654,5 +654,5 @@ import Relation.Binary using (Decidable)
     ∨  U+2228  LOGICAL OR (\or, \vee)
     ⊃  U+2283  SUPERSET OF (\sup)
     ᵇ  U+1D47  MODIFIER LETTER SMALL B  (\^b)
-    ⌊  U+230A  LEFT FLOOR (\cll)
-    ⌋  U+230B  RIGHT FLOOR (\clr)
+    ⌊  U+230A  LEFT FLOOR (\clL)
+    ⌋  U+230B  RIGHT FLOOR (\clR)

src/plfa/part1/Equality.lagda.md

@@ -520,15 +520,15 @@ it sparingly, but it is occasionally essential.
 
 ## Leibniz equality
 
-The form of asserting equality that we have used is due to Martin
-Löf, and was published in 1975.  An older form is due to Leibniz, and
+The form of asserting equality that we have used is due to Martin-Löf,
+and was published in 1975.  An older form is due to Leibniz, and
 was published in 1686.  Leibniz asserted the _identity of
 indiscernibles_: two objects are equal if and only if they satisfy the
 same properties. This principle sometimes goes by the name Leibniz'
 Law, and is closely related to Spock's Law, "A difference that makes
 no difference is no difference".  Here we define Leibniz equality,
 and show that two terms satisfy Leibniz equality if and only if they
-satisfy Martin Löf equality.
+satisfy Martin-Löf equality.
 
 Leibniz equality is usually formalised to state that `x ≐ y` holds if
 every property `P` that holds of `x` also holds of `y`.  Perhaps
@@ -593,7 +593,7 @@ implies `P x`.  To do so, we instantiate the equality with a predicate
 is trivial by reflexivity, and hence `Q y` follows from `x ≐ y`.  But
 `Q y` is exactly a proof of what we require, that `P y` implies `P x`.
 
-We now show that Martin Löf equality implies
+We now show that Martin-Löf equality implies
 Leibniz equality, and vice versa.  In the forward direction, if we know
 `x ≡ y` we need for any `P` to take evidence of `P x` to evidence of `P y`,
 which is easy since equality of `x` and `y` implies that any proof
@@ -625,7 +625,7 @@ to a proof of `P y` we need to show `x ≡ y`:
 ```
 The proof is similar to that for symmetry of Leibniz equality. We take
 `Q` to be the predicate that holds of `z` if `x ≡ z`. Then `Q x` is
-trivial by reflexivity of Martin Löf equality, and hence `Q y`
+trivial by reflexivity of Martin-Löf equality, and hence `Q y`
 follows from `x ≐ y`.  But `Q y` is exactly a proof of what we
 require, that `x ≡ y`.
 

src/plfa/part1/Induction.lagda.md

@@ -290,7 +290,7 @@ hypothesis:
 Reading the chain of equations in the inductive case of the proof, the
 top and bottom of the chain match the two sides of the equation to be
 shown, and reading down from the top and up from the bottom takes us
-to the simplified equation above. The remaining equation, does not follow
+to the simplified equation above. The remaining equation does not follow
 from simplification alone, so we use an additional operator for chain
 reasoning, `_≡⟨_⟩_`, where a justification for the equation appears
 within angle brackets.  The justification given is:

src/plfa/part2/Lambda.lagda.md

@@ -1314,7 +1314,7 @@ We can fill in the hole by typing C-c C-r again:
 
 And again:
 
-    ⊢suc′ = ⊢ƛ (⊢suc (⊢` { }3))
+    ⊢sucᶜ = ⊢ƛ (⊢suc (⊢` { }3))
     ?3 : ∅ , "n" ⦂ `ℕ ∋ "n" ⦂ `ℕ
 
 A further attempt with C-c C-r yields the message:
@@ -1323,7 +1323,7 @@ A further attempt with C-c C-r yields the message:
 
 We can fill in `Z` by hand. If we type C-c C-space, Agda will confirm we are done:
 
-    ⊢suc′ = ⊢ƛ (⊢suc (⊢` Z))
+    ⊢sucᶜ = ⊢ƛ (⊢suc (⊢` Z))
 
 The entire process can be automated using Agsy, invoked with C-c C-a.
 
@@ -1415,6 +1415,7 @@ This chapter uses the following unicode:
     ⇒  U+21D2  RIGHTWARDS DOUBLE ARROW (\=>)
     ƛ  U+019B  LATIN SMALL LETTER LAMBDA WITH STROKE (\Gl-)
     ·  U+00B7  MIDDLE DOT (\cdot)
+    ≟  U+225F  QUESTIONED EQUAL TO (\?=)
     —  U+2014  EM DASH (\em)
     ↠  U+21A0  RIGHTWARDS TWO HEADED ARROW (\rr-)
     ξ  U+03BE  GREEK SMALL LETTER XI (\Gx or \xi)