Merge branch 'dev' of https://github.com/plfa/plfa.github.io into dev

src/plfa/Equality.lagda

@@ -528,7 +528,7 @@ and instead we write `_≐_ {A} x y` to provide access to the implicit
 parameter `A` which appears on the right-hand side.
 
 This is our first use of _levels_.  We cannot assign `Set` the type
-`Set`, since this would lead to contradictions such as Russel's
+`Set`, since this would lead to contradictions such as Russell's
 Paradox and Girard's Paradox.  Instead, there is a hierarchy of types,
 where `Set : Set₁`, `Set₁ : Set₂`, and so on.  In fact, `Set` itself
 is just an abbreviation for `Set₀`.  Since the equation defining `_≐_`

src/plfa/Induction.lagda

@@ -38,19 +38,19 @@ open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
 Operators pop up all the time, and mathematicians have agreed
 on names for some of the most common properties.
 
-* _Identity_ Operator `+` has left identity `0` if `0 + n ≡ n`, and
+* _Identity_.   Operator `+` has left identity `0` if `0 + n ≡ n`, and
   right identity `0` if `n + 0 ≡ n`, for all `n`. A value that is both
   a left and right identity is just called an identity. Identity is also
   sometimes called _unit_.
 
-* _Associativity_ Operator `+` is associative if the location
+* _Associativity_.   Operator `+` is associative if the location
   of parentheses does not matter: `(m + n) + p ≡ m + (n + p)`,
   for all `m`, `n`, and `p`.
 
-* _Commutatitivity_ Operator `+` is commutative if order or
+* _Commutatitivity_.   Operator `+` is commutative if order or
   arguments does not matter: `m + n ≡ n + m`, for all `m` and `n`.
 
-* _Distributivity_ Operator `*` distributes over operator `+` from the
+* _Distributivity_.   Operator `*` distributes over operator `+` from the
   left if `(m + n) * p ≡ (m * p) + (n * p)`, for all `m`, `n`, and `p`,
   and from the right if `m * (p + q) ≡ (m * p) + (m * q)`, for all `m`,
   `p`, and `q`.
@@ -248,7 +248,7 @@ We have named the proof `+-assoc`.  In Agda, identifiers can consist of
 any sequence of characters not including spaces or the characters `@.(){};_`.
 
 Let's unpack this code.  The signature states that we are
-defining the identifier `+-assoc` which provide evidence for the
+defining the identifier `+-assoc` which provides evidence for the
 proposition:
 
     ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)

src/plfa/Relations.lagda

@@ -713,7 +713,6 @@ and back is the identity.
     ---------------
     to (from x) ≡ x
 
-\end{code}
 (Hint: For each of these, you may first need to prove related
 properties of `One`.)