diff --git a/src/Acknowledgements.lagda b/src/Acknowledgements.lagda index dac93614..e3527853 100644 --- a/src/Acknowledgements.lagda +++ b/src/Acknowledgements.lagda @@ -27,6 +27,7 @@ For answering questions on the Agda mailing list. * Nils Anders Danielsson * Miëtek Bak * Gergő Érdi +* Adam Sandberg Eriksson * David Janin * András Kovács * Ulf Norell diff --git a/src/Connectives.lagda b/src/Connectives.lagda index 95430720..9b2f897d 100644 --- a/src/Connectives.lagda +++ b/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, diff --git a/src/Equality.lagda b/src/Equality.lagda index 72f0606c..814550ef 100644 --- a/src/Equality.lagda +++ b/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 diff --git a/src/Isomorphism.lagda b/src/Isomorphism.lagda index f637d714..7850c032 100644 --- a/src/Isomorphism.lagda +++ b/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. diff --git a/src/Naturals.lagda b/src/Naturals.lagda index 512ff3ae..464abd87 100644 --- a/src/Naturals.lagda +++ b/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! diff --git a/src/Negation.lagda b/src/Negation.lagda index c1b1ad0d..a3234d80 100644 --- a/src/Negation.lagda +++ b/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. diff --git a/src/Properties.lagda b/src/Properties.lagda index cba6ac4d..ab5caf6f 100644 --- a/src/Properties.lagda +++ b/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. diff --git a/src/Quantifiers.lagda b/src/Quantifiers.lagda index 8bcc0281..e0c8f71b 100644 --- a/src/Quantifiers.lagda +++ b/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)` -> `odd n` *iff* `∃[ m ] (1 + 2 * m ≡ n)` + even n iff ∃[ m ] ( 2 * m ≡ n) + odd n iff ∃[ m ] (1 + 2 * m ≡ n) -First, we need a lemma, which allows us to simplify twice the -successor of `m` to two more than twice `m`. +First, we need a lemma, which states that twice the successor of `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 ¬∃∀ = diff --git a/src/Relations.lagda b/src/Relations.lagda index 76a33a49..57d47b6c 100644 --- a/src/Relations.lagda +++ b/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.