corrected spelling

src/Acknowledgements.lagda

@@ -27,6 +27,7 @@ For answering questions on the Agda mailing list.
 * Nils Anders Danielsson <nad@cse.gu.se>
 * Miëtek Bak <mietek@bak.io>
 * Gergő Érdi <gergo@erdi.hu>
+* Adam Sandberg Eriksson <adam@sandbergericsson.se>
 * David Janin <david.janin@labri.fr>
 * András Kovács <kovacsahun@hotmail.com>
 * Ulf Norell <ulf.norell@gmail.com>

src/Connectives.lagda

@@ -49,7 +49,7 @@ data _×_ : Set → Set → Set where
 Evidence that `A × B` holds is of the form
 `(M , N)`, where `M` is evidence that `A` holds and
 `N` is evidence that `B` holds.  By convention, we
-parenthesize pairs, even though `M , N` is also
+parenthesise pairs, even though `M , N` is also
 accepted by Agda.
 
 Given evidence that `A × B` holds, we can conclude that either
@@ -189,7 +189,7 @@ to `(aa , true)`, which is a member of the latter.
 For associativity, the `to` function reassociates two uses of pairing,
 taking `((x , y) , z)` to `(x , (y , z))`, and the `from` function does
 the inverse.  Again, the evidence of left and right inverse requires
-matching against a suitable pattern to enable simplificition.
+matching against a suitable pattern to enable simplification.
 \begin{code}
 ×-assoc : ∀ {A B C : Set} → ((A × B) × C) ≃ (A × (B × C))
 ×-assoc =
@@ -269,7 +269,7 @@ Having an *identity* is different from having an identity
 In the first case, we might have that `m` is `2`, and both
 `1 * m` and `m` are equal to `2`.  In the second
 case, we might have that `A` is `Bool`, and `⊤ × Bool` is *not* the
-same as `Bool`.  But there is an isomorphism betwee the two types.
+same as `Bool`.  But there is an isomorphism between the two types.
 For instance, `(tt, true)`, which is a member of the former,
 corresponds to `true`, which is a member of the latter.
 
@@ -304,7 +304,7 @@ is evidence that `A` holds, or `inj₂ N`, where `N` is evidence that
 `B` holds.
 
 Given evidence that `A → C` and `B → C` both hold, then given
-evidence that `A ⊎ B` holds we can conlude that `C` holds.
+evidence that `A ⊎ B` holds we can conclude that `C` holds.
 \begin{code}
 ⊎-elim : ∀ {A B C : Set} → (A → C) → (B → C) → (A ⊎ B → C)
 ⊎-elim f g (inj₁ x) = f x
@@ -317,7 +317,7 @@ When `inj₁` and `inj₂` appear on the right-hand side of an equation we
 refer to them as *constructors*, and when they appears on the
 left-hand side we refer to them as *destructors*.  We also refer
 to `⊎-elim` as a destructor, since it plays a similar role.
-Other terminology refers to constructorse as *introducing* a disjunction,
+Other terminology refers to constructors as *introducing* a disjunction,
 and to a destructors as *eliminating* a disjunction.
 
 Applying the destructor to each of the constructors is the identity.
@@ -411,7 +411,7 @@ former, corresponds to `inj₂ true`, which is a member of the latter.
 
 For associativity, the `to` function reassociates, and the `from` function does
 the inverse.  Again, the evidence of left and right inverse requires
-matching against a suitable pattern to enable simplificition.
+matching against a suitable pattern to enable simplification.
 \begin{code}
 ⊎-assoc : ∀ {A B C : Set} → ((A ⊎ B) ⊎ C) ≃ (A ⊎ (B ⊎ C))
 ⊎-assoc = record
@@ -487,7 +487,7 @@ enumerates all possible arguments of type `⊥`:
 Here again the absurd pattern `()` indicates that no value can match
 type `⊥`.
 
-For numbers, zero is the identity of additition. Correspondingly,
+For numbers, zero is the identity of addition. Correspondingly,
 empty is the identity of sums *up to isomorphism*.
 For left identity, the `to` function observes that `inj₁ ()` can never arise,
 and takes `inj₂ x` to `x`, and the `from` function
@@ -519,7 +519,7 @@ Having an *identity* is different from having an identity
 In the first case, we might have that `m` is `2`, and both `0 + m` and
 `m` are equal to `2`.  In the second case, we might have that `A` is
 `Bool`, and `⊥ ⊎ Bool` is *not* the same as `Bool`.  But there is an
-isomorphism betwee the two types.  For instance, `inj₂ true`, which is
+isomorphism between the two types.  For instance, `inj₂ true`, which is
 a member of the former, corresponds to `true`, which is a member of
 the latter.
 
@@ -594,7 +594,7 @@ Given two types `A` and `B`, we refer to `A → B` as the *function*
 space from `A` to `B`.  It is also sometimes called the *exponential*,
 with `B` raised to the `A` power.  Among other reasons for calling
 it the exponential, note that if type `A` has `m` distinct
-memebers, and type `B` has `n` distinct members, then the type
+members, and type `B` has `n` distinct members, then the type
 `A → B` has `n ^ m` distinct members.  For instance, consider a
 type `Bool` with two members and a type `Tri` with three members,
 as defined earlier. The the type `Bool → Tri` has nine (that is,

src/Equality.lagda

@@ -29,7 +29,7 @@ constructor `refl` provides evidence that `x ≡ x`. Hence, every value
 is equivalent to itself, and we have no other way of showing values
 are equivalent.  We have quantified over all levels, so that we can
 apply equivalence to types belonging to any level.  The definition
-features an asymetry, in that the first argument to `_≡_` is given by
+features an asymmetry, in that the first argument to `_≡_` is given by
 the parameter `x : A`, while the second is given by an index in `A → Set ℓ`.
 This follows our policy of using parameters wherever possible.
 The first argument to `_≡_` can be a parameter because it doesn't vary,
@@ -454,9 +454,9 @@ 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
-satsisfy Lebiniz equality if and only if they satisfy Martin Löf equivalence.
+satisfy Leibniz equality if and only if they satisfy Martin Löf equivalence.
 
-Leibniz equality is usually formalized to state that `x ≐ y`
+Leibniz equality is usually formalised to state that `x ≐ y`
 holds if every property `P` that holds of `x` also holds of
 `y`.  Perhaps surprisingly, this definition is
 sufficient to also ensure the converse, that every property `P` that

src/Isomorphism.lagda

@@ -52,7 +52,7 @@ of four things:
 + Evidence `to∘from` asserting that `to` is a *left-identity* for `from`.
 In particular, the third asserts that `from ∘ to` is the identity, and
 the fourth that `to ∘ from` is the identity, hence the names.
-The declaration `open _≃_` makes avaialable the names `to`, `from`,
+The declaration `open _≃_` makes available the names `to`, `from`,
 `from∘to`, and `to∘from`, otherwise we would need to write `_≃_.to` and so on.
 
 The above is our first use of records. A record declaration is equivalent
@@ -184,7 +184,7 @@ equational reasoning to combine the inverses.
 
 It is straightforward to support a variant of equational reasoning for
 isomorphism.  We essentially copy the previous definition for
-of equivality.  We omit the form that corresponds to `_≡⟨⟩_`, since
+of equality.  We omit the form that corresponds to `_≡⟨⟩_`, since
 trivial isomorphisms arise far less often than trivial equalities.
 
 \begin{code}
@@ -317,7 +317,7 @@ import Function using (_∘_)
 import Function.Inverse using (_↔_)
 import Function.LeftInverse using (_↞_)
 \end{code}
-Here `_↔_` correpsonds to our `_≃_`, and `_↞_` corresponds to our `_≲_`.
+Here `_↔_` corresponds to our `_≃_`, and `_↞_` corresponds to our `_≲_`.
 However, we stick with the definitions given here, mainly because `_↔_` is
 specified as a nested record, rather than the flat records used here.
 

src/Naturals.lagda

@@ -592,7 +592,7 @@ When I first learned about currying, I was told it was misattributed,
 since the same idea was previously proposed by Moses Schönfinkel in
 the 1920's.  I was told a joke: "It should be called schönfinkeling,
 but currying is tastier". Only later did I learn that the explanation
-of the misattribution was itself a misattribution.  The idea actully
+of the misattribution was itself a misattribution.  The idea actually
 appears in the *Begriffschrift* of Gottlob Frege, published in 1879.
 We should call it frigging!
 

src/Negation.lagda

@@ -270,7 +270,7 @@ The devil paused.  "I choose (b)."
 The man was disappointed but not surprised.  That was that, he thought.
 But the offer gnawed at him.  Imagine what he could do with his wish!
 Many years passed, and the man began to accumulate money.  To get the
-money he sometimes did bad things, and dimly he realized that
+money he sometimes did bad things, and dimly he realised that
 this must be what the devil had in mind.
 Eventually he had his billion dollars, and the devil appeared again.
 

src/Properties.lagda

@@ -75,7 +75,7 @@ Proof by induction follows the structure of this definition.  To prove
 a property of natural numbers by induction, we need prove two cases.
 First is the *base case*, where we show the property holds for `zero`.
 Second is the *inductive case*, where we assume the the property holds for
-an arbitary natural `m` (we call this the *inductive hypothesis*), and
+an arbitrary natural `m` (we call this the *inductive hypothesis*), and
 then show that the property must also hold for `suc m`.
 
 If we write `P m` for a property of `m`, then what we need to
@@ -149,7 +149,7 @@ In order to prove associativity, we take `P m` to be the property
 
     (m + n) + p ≡ m + (n + p)
 
-Here `n` and `p` are arbitary natural numbers, so if we can show the
+Here `n` and `p` are arbitrary natural numbers, so if we can show the
 equation holds for all `m` it will also hold for all `n` and `p`.
 The appropriate instances of the inference rules are:
 
@@ -247,7 +247,7 @@ preserved by applying that function.  If `e` is evidence that `x ≡ y`,
 then `cong f e` is evidence that `f x ≡ f y`, for any function `f`.
 
 Here the inductive hypothesis is not assumed, but instead proved by a
-recursive invocation of the function we are definining, `+-assoc m n p`.
+recursive invocation of the function we are defining, `+-assoc m n p`.
 As with addition, this is well founded because associativity of
 larger numbers is proved in terms of associativity of smaller numbers.
 In this case, `assoc (suc m) n p` is proved using `assoc m n p`.
@@ -462,7 +462,7 @@ We show this in two steps.  First, we have:
 
     m + suc n ≡ suc (m + n)
 
-which is justifed by the second lemma, `⟨ +-suc m n ⟩`.  Then we
+which is justified by the second lemma, `⟨ +-suc m n ⟩`.  Then we
 have
 
     suc (m + n) ≡ suc (n + m)
@@ -480,7 +480,7 @@ will suggest what lemmas to prove.
 
 ## Creation, one last time
 
-Returing to the proof of associativity, it may be helpful to view the inductive
+Returning to the proof of associativity, it may be helpful to view the inductive
 proof (or, equivalently, the recursive definition) as a creation story.  This
 time we are concerned with judgements asserting associativity.
 

src/Quantifiers.lagda

@@ -4,7 +4,7 @@ layout    : page
 permalink : /Quantifiers
 ---
 
-This chapter introduces universal and existential quatification.
+This chapter introduces universal and existential quantification.
 
 ## Imports
 
@@ -238,11 +238,11 @@ We will show that a number is even if and only if it is twice some
 other number, and odd if and only if it is one more than twice
 some other number.  In other words, we will show
 
-> `even n`  *iff*  `∃[ m ] (    2 * m ≡ n)`
+    even n   iff   ∃[ m ] (    2 * m ≡ n)
-> `odd  n`  *iff*  `∃[ m ] (1 + 2 * m ≡ n)`
+    odd  n   iff   ∃[ m ] (1 + 2 * m ≡ n)
 
-First, we need a lemma, which allows us to simplify twice the
+First, we need a lemma, which states that twice the successor of `m`
-successor of `m` to two more than twice `m`.
+is two more than twice `m`.
 \begin{code}
 lemma : ∀ (m : ℕ) → 2 * suc m ≡ 2 + 2 * m
 lemma m =
@@ -294,7 +294,7 @@ from our lemma.
 
 - If the number is odd because it is the successor of an even
 number, then we apply the induction hypothesis to give a number `m`
-and evidence that `2 * m ≡ n`. We return a pair conisting of `suc m`
+and evidence that `2 * m ≡ n`. We return a pair consisting of `suc m`
 and evidence that `1 + 2 * m = suc n`, which is immediate
 after substituting for `n`.
 
@@ -331,9 +331,9 @@ This completes the proof in the backward direction.
 
 Negation of an existential is isomorphic to universal
 of a negation.  Considering that existentials are generalised
-disjuntion and universals are generalised conjunction, this
+disjunction and universals are generalised conjunction, this
 result is analogous to the one which tells us that negation
-of a disjuntion is isomorphic to a conjunction of negations.
+of a disjunction is isomorphic to a conjunction of negations.
 \begin{code}
 ¬∃∀ : ∀ {A : Set} {B : A → Set} → (¬ ∃[ x ] B x) ≃ ∀ x → ¬ B x
 ¬∃∀ =

src/Relations.lagda

@@ -184,7 +184,7 @@ using holes and the `^C ^C`, `^C ^,`, and `^C ^R` commands.
 ## Transitivity
 
 The second property to prove about comparison is that it is
-transitive: for any naturals `m`, `n`, andl `p`, if `m ≤ n` and `n ≤
+transitive: for any naturals `m`, `n`, and `p`, if `m ≤ n` and `n ≤
 p` hold, then `m ≤ p` holds.
 \begin{code}
 ≤-trans : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p
@@ -195,7 +195,7 @@ Here the proof is most easily thought of as by induction on the
 *evidence* that `m ≤ n`, so we have left `m`, `n`, and `p` implicit.
 
 In the base case, the first inequality holds by `z≤n`, and so
-arwe are given `zero ≤ n` and `n ≤ p` and must show `zero ≤ p`,
+we are given `zero ≤ n` and `n ≤ p` and must show `zero ≤ p`,
 which follows immediately by `z≤n`.  In this
 case, the fact that `n ≤ p` is irrelevant, and we write `_` as the
 pattern to indicate that the corresponding evidence is unused.