Define precedence levels and associativities for all binary operators (…

…#712)

CODINGSTYLE.md

@@ -387,6 +387,12 @@ the story. Here's how we handle indentation and line breaks in the
   Sometimes, however, `equation-n` is a short proof term that fits on the same
   line as `by` within the 80 character limit. In that case it is ok to do so.
 
+- Expressions involving mixfix operators are appropriately parenthesized when
+  the particular association bears relevance, or if there is any chance of
+  confusion from omitting the parentheses. A reader of the code should not be
+  expected to know the precedence levels or associativity of particular
+  operators.
+
 ## Coding practices we tend to avoid
 
 - Using Unicode characters in names is entirely permissible, but we recommend

MIXFIX-OPERATORS.md

@@ -0,0 +1,182 @@
+# Mixfix operators in agda-unimath
+
+This document outlines our choices of conventions for setting precedence levels
+and associativity of
+[mixfix operators in Agda](https://agda.readthedocs.io/en/v2.6.3.20230805/language/mixfix-operators.html),
+and provides guidelines for this.
+
+## Mixfix operators in Agda
+
+Infix operations in Agda are binary operations that take arguments on either
+side. For example, addition is commonly written in infix notation as `1 + 2`.
+Mixfix operations are operations with longer names potentially containing
+multiple components, where the arguments appear between the components. For
+example, the commutator `[a,b]` is a common mixfix operation. The purpose of
+introducing infix and mixfix operations in Agda is to make the code more
+readable by using commonly accepted notation for widely used operations.
+
+Mixfix operators can each be assigned a
+[precedence level](https://agda.readthedocs.io/en/v2.6.3.20230805/language/mixfix-operators.html#precedence).
+This can in principle be any signed fractional value, although we prefer them to
+be non-negative integral values. The higher this value is, the higher precedence
+the operator has, meaning it is evaluated before operators with lower
+precedence. By default in Agda, an operator is assigned a precedence level of
+`20`.
+
+For instance,
+[multiplication on natural numbers `_*ℕ_`](elementary-number-theory.multiplication-natural-numbers.md)
+is assigned the precedence level `40`, and
+[addition on natural numbers `_+ℕ_`](elementary-number-theory.addition-natural-numbers.md)
+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
+either left or right
+[associative](https://agda.readthedocs.io/en/v2.6.3.20230805/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.
+
+For instance, since the pairing operator
+[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.
+
+## Operator classes
+
+We divide the different operators into broad classes, each assigned a range of
+possible precedence levels. In broad terms, we discern between _parametric_ and
+_non-parametric_ operators. The general rule is that non-parametric operator has
+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
+[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)
+and
+[multiplication of Eisenstein integers `_*ℤ[ω]_`](commutative-algebra.eisenstein-integers.md).
+
+Within these two classes, we make a further distinction between _relational_,
+_additive_, _multiplicative_, _exponentiative_, and _unary_ operators, each with
+a higher precedence than the previous one. All together, we assign ranges as
+outlined below.
+
+|                          | Relations | Additive | Multiplicative | Exponentiative | Unary |
+| ------------------------ | --------- | -------- | -------------- | -------------- | ----- |
+| Parametric Operations    | 5-9       | 10-14    | 15-19          | 20-24          | 25-29 |
+| Nonparametric Operations | 30-34     | 35-39    | 40-44          | 45-49          | 50-54 |
+
+Note that the default precedence level (`20`) falls within the range of
+exponentiative parametric operations.
+
+As a rule of thumb, the lowest value in a range is assigned by default. The
+notable exceptions are outlined below.
+
+## Special rules for assigning precedence levels
+
+In this section, we outline special rules for assigning precedence levels to
+particular classes of operations. Please make sure to update this section if new
+rules are implemented.
+
+### Function type like formation operations
+
+In Agda, the arrow notation `_→_` for function type formation is directly
+handled by the parser, hence it has hardcoded precedence and right
+associativity. In particular, it has lower precedence than any user-declared
+operator. To make other directed arrow notations like
+[pointed function type formation `_→∗_`](structured-types.pointed-maps.md) and
+[embedding type formation `_↪_`](foundation-core.embeddings.md) consistent with
+this, we consider them as relational operators and assign them a precedence
+level of `5`, and usually define them to be _right associative_. Other
+relational operators are assigned the precedence level `6` by default.
+
+### Pairing operations
+
+The pairing operations [`_,_`](foundation.dependent-pair-types.md) and
+[`_,ω_`](foundation.large-dependent-pair-types.md) are assigned a low precedence
+level of `3`, below any of the above defined classes.
+
+### Reasoning syntaxes
+
+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.
+
+### 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`.
+
+## Assigning associativities
+
+Below, we outline a list of general rules when assigning associativities.
+
+- **Definitionally associative operators**, e.g.
+  [function composition `_∘_`](foundation-core.function-types.md), can be
+  assigned _any associativity_.
+
+- **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
+  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_.
+
+- **Arithmetic type formers** such as
+  [coproduct type formation `_+_`](foundation-core.coproduct-types.md) and
+  [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
+  `A + B + C`, one uses a single `inl`.
+
+- **Weakly associative operators**, meaning operators that are associative up to
+  [identification](foundation-core.identity-types.md), may still be practical to
+  define _an_ associativity for, for cases when the particular association does
+  not matter and you still want to apply the operator multiple times. For
+  instance, when performing an equality proof by a string of concatenations. For
+  this reason, we define
+  [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
+  associated regardless. For instance, one should never write
+
+  ```agda
+  assoc : p ∙ (q ∙ r) ＝ p ∙ q ∙ r
+  ```
+
+- **Unique well-typed associativity**. When an operator only has one well-typed
+  associativity, then one can define it to have that associativity. For
+  instance, with [homotopy left whiskering](foundation-core.homotopies.md),
+  `f ·l g ·l H` is only ever well-typed when associated to the _right_.
+
+## Full table of assigned precedences
+
+| Precedence level | Operators                                                                                                                                                                                                                                    |
+| ---------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
+| 50               | Unary non-parametric operators. This class is currently empty                                                                                                                                                                                |
+| 45               | Exponentiative arithmetic operators                                                                                                                                                                                                          |
+| 40               | Multiplicative arithmetic operators                                                                                                                                                                                                          |
+| 36               | Subtractive arithmetic operators                                                                                                                                                                                                             |
+| 35               | Additive arithmetic operators                                                                                                                                                                                                                |
+| 30               | Relational arithmetic operators, `_≤-ℕ_` and `_<-ℕ_`                                                                                                                                                                                         |
+| 25               | Parametric unary operators. This class is currently empty                                                                                                                                                                                    |
+| 20               | Parametric exponentiative operators. This class is currently empty                                                                                                                                                                           |
+| 15               | Parametric multiplicative operators like `_×_`,`_×∗_`, `_∧_`, `_∧∗_`, function composition operations like `_∘_`,`_∘∗_`, `_∘e_`, and `_∘iff_`, identification concatenation and whiskering operations like `_∙_`, `_∙h_`, `_·l_`, and `_·r_` |
+| 10               | Parametric additive operators like `_+_`, `_∨_`, `_∨∗_`, list concatenation, monadic bind operations for the type checking monad                                                                                                             |
+| 6                | Parametric relational operations like `_＝_`, `_~_`, `_≃_`, and `_↔_`, elementhood relations, subtype relations                                                                                                                              |
+| 5                | Directed function type-like formation operations, e.g. `_→∗_` and `_↪_`                                                                                                                                                                      |
+| 3                | The pairing operations `_,_` and `_,ω_`                                                                                                                                                                                                      |
+| 0-1              | Reasoning syntaxes                                                                                                                                                                                                                           |
+| -∞               | Function type formation `_→_`                                                                                                                                                                                                                |

Makefile

@@ -10,22 +10,24 @@ AGDAHTMLFLAGS ?= --html --html-highlight=code --html-dir=docs --css=Agda.css --o
 AGDA ?= agda $(AGDAVERBOSE)
 TIME ?= time
 
-METAFILES :=CITE-THIS-LIBRARY.md \
-			CODINGSTYLE.md \
-			CONTRIBUTING.md \
-			CONTRIBUTORS.md \
-			FILE-CONVENTIONS.md \
-			DESIGN-PRINCIPLES.md \
-			GRANT-ACKNOWLEDGEMENTS.md \
-			HOME.md \
-			HOWTO-INSTALL.md \
-			LICENSE.md \
-			MAINTAINERS.md \
-			README.md \
-			STATEMENT-OF-INCLUSION.md \
-			SUMMARY.md \
-			TEMPLATE.lagda.md \
-			USERS.md \
+METAFILES := \
+  CITE-THIS-LIBRARY.md \
+  CODINGSTYLE.md \
+  CONTRIBUTING.md \
+  CONTRIBUTORS.md \
+  FILE-CONVENTIONS.md \
+  DESIGN-PRINCIPLES.md \
+  GRANT-ACKNOWLEDGEMENTS.md \
+  HOME.md \
+  HOWTO-INSTALL.md \
+  LICENSE.md \
+  MIXFIX-OPERATORS.md \
+  MAINTAINERS.md \
+  README.md \
+  STATEMENT-OF-INCLUSION.md \
+  SUMMARY.md \
+  TEMPLATE.lagda.md \
+  USERS.md \
 
 .PHONY: agdaFiles
 agdaFiles:

scripts/generate_main_index_file.py

@@ -97,6 +97,7 @@ def generate_index(root, header):
     - [Structuring your file](FILE-CONVENTIONS.md)
         - [File template](TEMPLATE.lagda.md)
     - [The library coding style](CODINGSTYLE.md)
+    - [Guidelines for mixfix operations](MIXFIX-OPERATIONS.md)
     - [Citing the library](CITE-THIS-LIBRARY.md)
 
 {module_index}

src/commutative-algebra/eisenstein-integers.lagda.md

@@ -112,7 +112,7 @@ add-ℤ[ω] : ℤ[ω] → ℤ[ω] → ℤ[ω]
 pr1 (add-ℤ[ω] (a , b) (a' , b')) = a +ℤ a'
 pr2 (add-ℤ[ω] (a , b) (a' , b')) = b +ℤ b'
 
-infix 30 _+ℤ[ω]_
+infixl 35 _+ℤ[ω]_
 _+ℤ[ω]_ = add-ℤ[ω]
 
 ap-add-ℤ[ω] :
@@ -139,7 +139,7 @@ pr1 (mul-ℤ[ω] (a1 , b1) (a2 , b2)) =
 pr2 (mul-ℤ[ω] (a1 , b1) (a2 , b2)) =
   ((a1 *ℤ b2) +ℤ (a2 *ℤ b1)) +ℤ (neg-ℤ (b1 *ℤ b2))
 
-infix 30 _*ℤ[ω]_
+infixl 40 _*ℤ[ω]_
 _*ℤ[ω]_ = mul-ℤ[ω]
 
 ap-mul-ℤ[ω] :

src/commutative-algebra/euclidean-domains.lagda.md

@@ -74,7 +74,7 @@ is-euclidean-valuation R v =
     ( λ (q , r) →
       ( Id x (add-Integral-Domain R (mul-Integral-Domain R q y) r)) ×
         ( is-zero-Integral-Domain R r +
-        ( v r < v y)))
+        ( v r <-ℕ v y)))
 ```
 
 ### The condition of being a Euclidean domain
@@ -691,7 +691,7 @@ module _
     ( is-zero-Euclidean-Domain
       ( remainder-euclidean-division-Euclidean-Domain x y p)) +
     ( euclidean-valuation-Euclidean-Domain
-      ( remainder-euclidean-division-Euclidean-Domain x y p) <
+      ( remainder-euclidean-division-Euclidean-Domain x y p) <-ℕ
     ( euclidean-valuation-Euclidean-Domain y))
   remainder-condition-euclidean-division-Euclidean-Domain x y p =
     pr2 (pr2 (pr2 is-euclidean-domain-Euclidean-Domain x y p))

src/commutative-algebra/gaussian-integers.lagda.md

@@ -112,7 +112,7 @@ add-ℤ[i] : ℤ[i] → ℤ[i] → ℤ[i]
 pr1 (add-ℤ[i] (a , b) (a' , b')) = a +ℤ a'
 pr2 (add-ℤ[i] (a , b) (a' , b')) = b +ℤ b'
 
-infix 30 _+ℤ[i]_
+infixl 35 _+ℤ[i]_
 _+ℤ[i]_ = add-ℤ[i]
 
 ap-add-ℤ[i] :
@@ -135,7 +135,7 @@ mul-ℤ[i] : ℤ[i] → ℤ[i] → ℤ[i]
 pr1 (mul-ℤ[i] (a , b) (a' , b')) = (a *ℤ a') -ℤ (b *ℤ b')
 pr2 (mul-ℤ[i] (a , b) (a' , b')) = (a *ℤ b') +ℤ (a' *ℤ b)
 
-infix 30 _*ℤ[i]_
+infixl 40 _*ℤ[i]_
 _*ℤ[i]_ = mul-ℤ[i]
 
 ap-mul-ℤ[i] :

src/elementary-number-theory/addition-integer-fractions.lagda.md

@@ -37,7 +37,7 @@ pr2 (pr2 (add-fraction-ℤ (m , n , n-pos) (m' , n' , n'-pos))) =
 add-fraction-ℤ' : fraction-ℤ → fraction-ℤ → fraction-ℤ
 add-fraction-ℤ' x y = add-fraction-ℤ y x
 
-infix 30 _+fraction-ℤ_
+infixl 35 _+fraction-ℤ_
 _+fraction-ℤ_ = add-fraction-ℤ
 
 ap-add-fraction-ℤ :

src/elementary-number-theory/addition-integers.lagda.md

@@ -47,7 +47,7 @@ add-ℤ (inr (inr (succ-ℕ x))) l = succ-ℤ (add-ℤ (inr (inr x)) l)
 add-ℤ' : ℤ → ℤ → ℤ
 add-ℤ' x y = add-ℤ y x
 
-infix 30 _+ℤ_
+infixl 35 _+ℤ_
 _+ℤ_ = add-ℤ
 
 ap-add-ℤ :

src/elementary-number-theory/addition-natural-numbers.lagda.md

@@ -34,7 +34,7 @@ add-ℕ x (succ-ℕ y) = succ-ℕ (add-ℕ x y)
 add-ℕ' : ℕ → ℕ → ℕ
 add-ℕ' m n = add-ℕ n m
 
-infix 30 _+ℕ_
+infixl 35 _+ℕ_
 _+ℕ_ = add-ℕ
 
 ap-add-ℕ :

src/elementary-number-theory/addition-rational-numbers.lagda.md

@@ -36,7 +36,7 @@ add-ℚ (x , p) (y , q) = in-fraction-ℤ (add-fraction-ℤ x y)
 add-ℚ' : ℚ → ℚ → ℚ
 add-ℚ' x y = add-ℚ y x
 
-infix 30 _+ℚ_
+infixl 35 _+ℚ_
 _+ℚ_ = add-ℚ
 
 ap-add-ℚ :

src/elementary-number-theory/difference-integers.lagda.md

@@ -31,8 +31,8 @@ are derived there.
 diff-ℤ : ℤ → ℤ → ℤ
 diff-ℤ x y = x +ℤ (neg-ℤ y)
 
+infixl 36 _-ℤ_
 _-ℤ_ = diff-ℤ
-infix 30 _-ℤ_
 ```
 
 ## Properties

src/elementary-number-theory/exponentiation-natural-numbers.lagda.md

@@ -32,7 +32,7 @@ exp-ℕ : ℕ → ℕ → ℕ
 exp-ℕ m 0 = 1
 exp-ℕ m (succ-ℕ n) = (exp-ℕ m n) *ℕ m
 
-infix 30 _^ℕ_
+infixr 45 _^ℕ_
 _^ℕ_ = exp-ℕ
 ```
 

src/elementary-number-theory/half-integers.lagda.md

@@ -52,6 +52,6 @@ add-½ℤ (inl x) (inr y) = inl (x +ℤ y)
 add-½ℤ (inr x) (inl y) = inl (x +ℤ y)
 add-½ℤ (inr x) (inr y) = inr (x +ℤ y)
 
-infix 30 _+½ℤ_
+infixl 35 _+½ℤ_
 _+½ℤ_ = add-½ℤ
 ```

src/elementary-number-theory/inequality-natural-numbers.lagda.md

@@ -48,6 +48,7 @@ leq-ℕ zero-ℕ m = unit
 leq-ℕ (succ-ℕ n) zero-ℕ = empty
 leq-ℕ (succ-ℕ n) (succ-ℕ m) = leq-ℕ n m
 
+infix 30 _≤-ℕ_
 _≤-ℕ_ = leq-ℕ
 ```
 

src/elementary-number-theory/multiplication-integer-fractions.lagda.md

@@ -43,7 +43,7 @@ pr2 (pr2 (mul-fraction-ℤ (m , n , n-pos) (m' , n' , n'-pos))) =
 mul-fraction-ℤ' : fraction-ℤ → fraction-ℤ → fraction-ℤ
 mul-fraction-ℤ' x y = mul-fraction-ℤ y x
 
-infix 30 _*fraction-ℤ_
+infixl 40 _*fraction-ℤ_
 _*fraction-ℤ_ = mul-fraction-ℤ
 
 ap-mul-fraction-ℤ :

src/elementary-number-theory/multiplication-integers.lagda.md

@@ -44,7 +44,7 @@ mul-ℤ (inr (inl star)) l = zero-ℤ
 mul-ℤ (inr (inr zero-ℕ)) l = l
 mul-ℤ (inr (inr (succ-ℕ x))) l = l +ℤ (mul-ℤ (inr (inr x)) l)
 
-infix 30 _*ℤ_
+infixl 40 _*ℤ_
 _*ℤ_ = mul-ℤ
 
 mul-ℤ' : ℤ → ℤ → ℤ

src/elementary-number-theory/multiplication-natural-numbers.lagda.md

@@ -35,7 +35,7 @@ mul-ℕ : ℕ → ℕ → ℕ
 mul-ℕ 0 n = 0
 mul-ℕ (succ-ℕ m) n = (mul-ℕ m n) +ℕ n
 
-infix 30 _*ℕ_
+infixl 40 _*ℕ_
 _*ℕ_ = mul-ℕ
 
 mul-ℕ' : ℕ → ℕ → ℕ