From f980058472feb15cea6c77cc1a973b5abf0be0e4 Mon Sep 17 00:00:00 2001 From: Juhana Laurinharju Date: Thu, 10 May 2018 20:37:58 +0300 Subject: [PATCH 1/5] that they only -> that the only --- src/Equality.lagda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Equality.lagda b/src/Equality.lagda index bd553aa0..20780fdd 100644 --- a/src/Equality.lagda +++ b/src/Equality.lagda @@ -402,7 +402,7 @@ as earlier examples have shown. ## Extensionality {#extensionality} -Extensionality asserts that they only way to distinguish functions is +Extensionality asserts that the only way to distinguish functions is by applying them; if two functions applied to the same argument always yield the same result, then they are the same functions. It is the converse of `cong-app`, introduced earlier. From 5c513266f24db881419c095192d503d9ce65adcb Mon Sep 17 00:00:00 2001 From: Juhana Laurinharju Date: Sat, 12 May 2018 18:06:00 +0300 Subject: [PATCH 2/5] a principal known as -> a principle known as --- src/Connectives.lagda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Connectives.lagda b/src/Connectives.lagda index d8c7ebc4..156b5d02 100644 --- a/src/Connectives.lagda +++ b/src/Connectives.lagda @@ -6,7 +6,7 @@ permalink : /Connectives This chapter introduces the basic logical connectives, by observing a correspondence between connectives of logic and data types, -a principal known as *Propositions as Types*. +a principle known as *Propositions as Types*. + *conjunction* is *product* + *disjunction* is *sum* From e65eb3713f338087459e1ddb76c8fcaea35d8737 Mon Sep 17 00:00:00 2001 From: Michel Steuwer Date: Sun, 13 May 2018 16:26:23 +0100 Subject: [PATCH 3/5] Wrong equation references in the text of Monus --- src/Naturals.lagda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Naturals.lagda b/src/Naturals.lagda index 6479507b..39d8b111 100644 --- a/src/Naturals.lagda +++ b/src/Naturals.lagda @@ -522,7 +522,7 @@ _ = 1 ∎ \end{code} -We did not use the third equation at all, but it will be required +We did not use the second equation at all, but it will be required if we try to subtract a smaller number from a larger one. \begin{code} _ = From a664d66bd53630870f028c651a1864c736ed1d6a Mon Sep 17 00:00:00 2001 From: Michel Steuwer Date: Sun, 13 May 2018 16:35:05 +0100 Subject: [PATCH 4/5] Associativity of arrows and function application The associativity of arrows and function application seems to be mixed up. --- src/Naturals.lagda | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Naturals.lagda b/src/Naturals.lagda index 6479507b..a7ca660c 100644 --- a/src/Naturals.lagda +++ b/src/Naturals.lagda @@ -259,7 +259,8 @@ opens that module, that is, adds all the names specified in the `using` clause into the current scope. In this case the names added are `_≡_`, the equivalence operator, and `refl`, the name for evidence that two terms are equal. The third line takes a record that -specifies operators to support reasoning about equivalence, and adds +specifies operators to support reasoning about equivalence, +dds all the names specified in the `using` clause into the current scope. In this case, the names added are `begin_`, `_≡⟨⟩_`, and `_∎`. We will see how these are used below. We take all these as givens for now, @@ -575,7 +576,7 @@ second argument. This trick goes by the name *currying*. Agda, like other functional languages such as ML and Haskell, is designed to make currying easy to use. Function -arrows associate to the left and application associates to the right. +arrows associate to the right and application associates to the left. ℕ → ℕ → ℕ stands for ℕ → (ℕ → ℕ) From aefc56cd030bfe756617ab17d5182429d3c37902 Mon Sep 17 00:00:00 2001 From: Michel Steuwer Date: Sun, 13 May 2018 16:37:16 +0100 Subject: [PATCH 5/5] fixed typo --- src/Naturals.lagda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Naturals.lagda b/src/Naturals.lagda index a7ca660c..9e86c716 100644 --- a/src/Naturals.lagda +++ b/src/Naturals.lagda @@ -259,8 +259,7 @@ opens that module, that is, adds all the names specified in the `using` clause into the current scope. In this case the names added are `_≡_`, the equivalence operator, and `refl`, the name for evidence that two terms are equal. The third line takes a record that -specifies operators to support reasoning about equivalence, -dds +specifies operators to support reasoning about equivalence, and adds all the names specified in the `using` clause into the current scope. In this case, the names added are `begin_`, `_≡⟨⟩_`, and `_∎`. We will see how these are used below. We take all these as givens for now,