Fix some typos in the mixfix guide (#928)

MIXFIX-OPERATORS.md

@@ -30,14 +30,15 @@ is assigned the precedence level `40`, and
 is assigned the precedence level `35`. Therefore, the expression `x +ℕ y *ℕ z`
 is parsed as `x +ℕ (y *ℕ z)`.
 
-In addition to a precedence level, every mixfix operator can be defined to be
+In addition to a precedence level, every infix operator can be defined to be
 either left or right
-[associative](https://agda.readthedocs.io/en/latest/language/mixfix-operators.html#associativity).
-It can be beneficial to define associativity of operators, to avoid excessively
-parenthesized expressions. The parenthization should, however, never be omitted
-when this can make the code more ambiguous or harder to read.
+[associative](https://agda.readthedocs.io/en/latest/language/mixfix-operators.html#associativity)
+using the keywords `infixl` and `infixr`. It can be beneficial to define
+associativity of operators to avoid excessively parenthesized expressions. The
+parenthization should, however, never be omitted when this can make the code
+more ambiguous or harder to read.
 
-For instance, since the pairing operator
+For instance, since the
 [pairing operator `_,_`](foundation.dependent-pair-types.md) is defined to
 associate to the right, the expression `a , b , c` is parsed as `a , (b , c)`.
 By default, an operator does not associate to either side.
@@ -51,12 +52,12 @@ higher precedence than parametric operators. Parametric operators are operators
 that take a universe level as one of their arguments. We consider an operator to
 be parametric even if it only takes a universe level as an implicit argument.
 Examples are the
-[cartesian product type former`_×_`](foundation-core.cartesian-product-types.md)
-, the [identity type former `_＝_`](foundation-core.identity-types.md) and the
+[cartesian product type former`_×_`](foundation-core.cartesian-product-types.md),
+the [identity type former `_＝_`](foundation-core.identity-types.md), and the
 [pairing operator `_,_`](foundation.dependent-pair-types.md). Examples of
 non-parametric operators are
-[difference of integers `_-ℤ_`](elementary-number-theory.difference-integers.md)
-[strict inequality on natural numbers `_<-ℕ_`](elementary-number-theory.strict-inequality-natural-numbers.md)
+[difference of integers `_-ℤ_`](elementary-number-theory.difference-integers.md),
+[strict inequality on natural numbers `_<-ℕ_`](elementary-number-theory.strict-inequality-natural-numbers.md),
 and
 [multiplication of Eisenstein integers `_*ℤ[ω]_`](commutative-algebra.eisenstein-integers.md).
 
@@ -105,17 +106,16 @@ level of `3`, below any of the above defined classes.
 Reasoning syntaxes, like
 [`equational-reasoning`](foundation-core.identity-types.md), is defined using
 Agda's mixfix operators, and should have lower precedence than all other
-operators (notably except for `_→_`). The precedence value range `0-1` is
-reserved for these.
+operators (notably except for the built-in `_→_`). The precedence value range
+`0-1` is reserved for these.
 
 ### Subtractive operators
 
 We consider the class of subtractive operators as a subclass of additive
 operators. These include operators like
-[difference of integers `_-ℤ_`](elementary-number-theory.difference-integers.md)
-and . Subtractive operators will usually have higher precedence than normal
-additive operators, so that expressions like `a - b + c` are parsed as
-`(a - b) + c`.
+[difference of integers `_-ℤ_`](elementary-number-theory.difference-integers.md).
+Subtractive operators will usually have higher precedence than additive
+operators, so that expressions like `a - b + c` are parsed as `(a - b) + c`.
 
 ## Assigning associativities
 
@@ -128,7 +128,7 @@ Below, we outline a list of general rules when assigning associativities.
 - **Non-parametric arithmetic operators** are often naturally computed from left
   to right. For instance, the expression `1 - 2 - 3` is computed as
   `(1 - 2) - 3 = -1 - 3 = -4`, hence should be _left associative_. This applies
-  to addition, subtraction, multiplication and division. Note that for
+  to addition, subtraction, multiplication, and division. Note that for
   non-parametric exponentiation, we compute from right to left. I.e. `2 ^ 3 ^ 4`
   should compute as `2 ^ (3 ^ 4)`. Hence it will usually be _right associative_.
 
@@ -137,7 +137,7 @@ Below, we outline a list of general rules when assigning associativities.
   [cartesian product type formation `_×_`](foundation-core.cartesian-product-types.md),
   are natural to parse from left to right in terms of their
   introduction/elimination rules. Therefore, they are commonly associated to the
-  _right_. This means that for instance to map into the left hand argument of
+  _right_. This means that for instance to map into the left-hand argument of
   `A + B + C`, one uses a single `inl`.
 
 - **Weakly associative operators**, meaning operators that are associative up to
@@ -149,7 +149,7 @@ Below, we outline a list of general rules when assigning associativities.
   [identification concatenation `_∙_`](foundation-core.identity-types.md) and
   [homotopy concatenation `_∙h_`](foundation-core.homotopies.md) to be _left
   associative_. Please note that parenthization should still only be omitted
-  when the association is completely irrelevant, even if your expression is left
+  when the association is of no importance, even if your expression is left
   associated regardless. For instance, one should never write
 
   ```agda