Merge branch 'master' of github.com:wenkokke/sf

Merging in pull requests for typo fixes.

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*

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.

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}
 _ =
@@ -575,7 +575,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    ℕ → (ℕ → ℕ)