@@ -132,7 +132,7 @@ equalities between values in different types:
132132
133133 idris_not_php : 2 = "2"
134134
135−Obviously, in Idris the type ``2 = 2`` is uninhabited, and one might
135+Obviously, in Idris the type ``2 = "2"`` is uninhabited, and one might
136136wonder why it is useful to be able to propose equalities between values
137137in different types. However, with dependent types, such equalities can
138138arise naturally. For example, if two vectors are equal, their lengths
@@ -177,7 +177,7 @@ given above as Idris type declarations:
177177Both of these properties (and many others) are proved for natural number
178178addition in the Idris standard library, using ``(+)`` from the ``Num``
179179type class rather than using ``plus`` directly. They have the names
180−``plusCommutative`` and ``plusAssociatie`` respectively.
180+``plusCommutative`` and ``plusAssociative`` respectively.
181181
182182In the remainder of this tutorial, we will explore several different
183183ways of proving ``plus_commutes`` (or, to put it another way, writing