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*
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.
diff --git a/src/Naturals.lagda b/src/Naturals.lagda
index 6479507b..86f95c3f 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}
 _ =
@@ -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    ℕ → (ℕ → ℕ)