Refactor the natural numbers and integers up to present code standards

src/commutative-algebra/polynomials-commutative-semirings.lagda.md

@@ -704,7 +704,7 @@ module _
                     rec-coproduct
                       ( λ j<Nq →
                         ex-falso
-                          ( anti-reflexive-le-ℕ
+                          ( irreflexive-le-ℕ
                             ( n)
                             ( tr
                               ( λ m → le-ℕ m n)
@@ -948,10 +948,10 @@ module _
                             ( rearrange)
                             ( eq-type-subtype
                               ( λ (i , j , n) →
-                                ( ( le-ℕ-Prop i Np) ∧
-                                  ( le-ℕ-Prop j Nq) ∧
+                                ( ( le-prop-ℕ i Np) ∧
+                                  ( le-prop-ℕ j Nq) ∧
                                   ( Id-Prop ℕ-Set (j +ℕ i) n) ∧
-                                  ( le-ℕ-Prop n (Nq +ℕ Np))))
+                                  ( le-prop-ℕ n (Nq +ℕ Np))))
                               refl)))
                 ( _)
           ＝

src/elementary-number-theory.lagda.md

@@ -44,7 +44,6 @@ open import elementary-number-theory.closed-intervals-rational-numbers public
 open import elementary-number-theory.cofibonacci public
 open import elementary-number-theory.collatz-bijection public
 open import elementary-number-theory.collatz-conjecture public
-open import elementary-number-theory.commutative-semiring-of-natural-numbers public
 open import elementary-number-theory.conatural-numbers public
 open import elementary-number-theory.congruence-integers public
 open import elementary-number-theory.congruence-natural-numbers public
@@ -181,6 +180,7 @@ open import elementary-number-theory.retracts-of-natural-numbers public
 open import elementary-number-theory.ring-extension-rational-numbers-of-rational-numbers public
 open import elementary-number-theory.ring-of-integers public
 open import elementary-number-theory.ring-of-rational-numbers public
+open import elementary-number-theory.semiring-of-natural-numbers public
 open import elementary-number-theory.sieve-of-eratosthenes public
 open import elementary-number-theory.square-free-natural-numbers public
 open import elementary-number-theory.squares-integers public

src/elementary-number-theory/absolute-value-integers.lagda.md

@@ -214,36 +214,39 @@ multiplicative-abs-ℤ x y =
 ### `|(-x)y| ＝ |xy|`
 
 ```agda
-left-negative-law-mul-abs-ℤ :
-  (x y : ℤ) → abs-ℤ (x *ℤ y) ＝ abs-ℤ ((neg-ℤ x) *ℤ y)
-left-negative-law-mul-abs-ℤ x y =
-  equational-reasoning
-    abs-ℤ (x *ℤ y)
-    ＝ abs-ℤ (neg-ℤ (x *ℤ y))
-      by (inv (negative-law-abs-ℤ (x *ℤ y)))
-    ＝ abs-ℤ ((neg-ℤ x) *ℤ y)
-      by (ap abs-ℤ (inv (left-negative-law-mul-ℤ x y)))
+abstract
+  left-negative-law-mul-abs-ℤ :
+    (x y : ℤ) → abs-ℤ (x *ℤ y) ＝ abs-ℤ ((neg-ℤ x) *ℤ y)
+  left-negative-law-mul-abs-ℤ x y =
+    equational-reasoning
+      abs-ℤ (x *ℤ y)
+      ＝ abs-ℤ (neg-ℤ (x *ℤ y))
+        by (inv (negative-law-abs-ℤ (x *ℤ y)))
+      ＝ abs-ℤ ((neg-ℤ x) *ℤ y)
+        by (ap abs-ℤ (inv (left-negative-law-mul-ℤ x y)))
 ```
 
 ### `|x(-y)| ＝ |xy|`
 
 ```agda
-right-negative-law-mul-abs-ℤ :
-  (x y : ℤ) → abs-ℤ (x *ℤ y) ＝ abs-ℤ (x *ℤ (neg-ℤ y))
-right-negative-law-mul-abs-ℤ x y =
-  equational-reasoning
-    abs-ℤ (x *ℤ y)
-    ＝ abs-ℤ (neg-ℤ (x *ℤ y))
-      by (inv (negative-law-abs-ℤ (x *ℤ y)))
-    ＝ abs-ℤ (x *ℤ (neg-ℤ y))
-      by (ap abs-ℤ (inv (right-negative-law-mul-ℤ x y)))
+abstract
+  right-negative-law-mul-abs-ℤ :
+    (x y : ℤ) → abs-ℤ (x *ℤ y) ＝ abs-ℤ (x *ℤ (neg-ℤ y))
+  right-negative-law-mul-abs-ℤ x y =
+    equational-reasoning
+      abs-ℤ (x *ℤ y)
+      ＝ abs-ℤ (neg-ℤ (x *ℤ y))
+        by (inv (negative-law-abs-ℤ (x *ℤ y)))
+      ＝ abs-ℤ (x *ℤ (neg-ℤ y))
+        by (ap abs-ℤ (inv (right-negative-law-mul-ℤ x y)))
 ```
 
 ### `|(-x)(-y)| ＝ |xy|`
 
 ```agda
-double-negative-law-mul-abs-ℤ :
-  (x y : ℤ) → abs-ℤ (x *ℤ y) ＝ abs-ℤ ((neg-ℤ x) *ℤ (neg-ℤ y))
-double-negative-law-mul-abs-ℤ x y =
-  (right-negative-law-mul-abs-ℤ x y) ∙ (left-negative-law-mul-abs-ℤ x (neg-ℤ y))
+abstract
+  double-negative-law-mul-abs-ℤ :
+    (x y : ℤ) → abs-ℤ (x *ℤ y) ＝ abs-ℤ ((neg-ℤ x) *ℤ (neg-ℤ y))
+  double-negative-law-mul-abs-ℤ x y =
+    ap abs-ℤ (inv (double-negative-law-mul-ℤ x y))
 ```

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

@@ -367,10 +367,11 @@ abstract
 
 abstract
   is-equiv-left-add-ℤ : (x : ℤ) → is-equiv (x +ℤ_)
-  pr1 (pr1 (is-equiv-left-add-ℤ x)) = add-ℤ (neg-ℤ x)
-  pr2 (pr1 (is-equiv-left-add-ℤ x)) = is-section-left-add-neg-ℤ x
-  pr1 (pr2 (is-equiv-left-add-ℤ x)) = add-ℤ (neg-ℤ x)
-  pr2 (pr2 (is-equiv-left-add-ℤ x)) = is-retraction-left-add-neg-ℤ x
+  is-equiv-left-add-ℤ x =
+    is-equiv-is-invertible
+      ( add-ℤ (neg-ℤ x))
+      ( is-section-left-add-neg-ℤ x)
+      ( is-retraction-left-add-neg-ℤ x)
 
 equiv-left-add-ℤ : ℤ → (ℤ ≃ ℤ)
 pr1 (equiv-left-add-ℤ x) = add-ℤ x
@@ -403,10 +404,11 @@ abstract
 
 abstract
   is-equiv-right-add-ℤ : (y : ℤ) → is-equiv (_+ℤ y)
-  pr1 (pr1 (is-equiv-right-add-ℤ y)) = _+ℤ (neg-ℤ y)
-  pr2 (pr1 (is-equiv-right-add-ℤ y)) = is-section-right-add-neg-ℤ y
-  pr1 (pr2 (is-equiv-right-add-ℤ y)) = _+ℤ (neg-ℤ y)
-  pr2 (pr2 (is-equiv-right-add-ℤ y)) = is-retraction-right-add-neg-ℤ y
+  is-equiv-right-add-ℤ y =
+    is-equiv-is-invertible
+      ( _+ℤ (neg-ℤ y))
+      ( is-section-right-add-neg-ℤ y)
+      ( is-retraction-right-add-neg-ℤ y)
 
 equiv-right-add-ℤ : ℤ → (ℤ ≃ ℤ)
 pr1 (equiv-right-add-ℤ y) = _+ℤ y

src/elementary-number-theory/archimedean-property-integers.lagda.md

@@ -59,7 +59,7 @@ abstract
           ( le-ℤ)
           ( ap pr1 (is-section-nat-nonnegative-ℤ (y , nonneg-y)))
           ( inv (mul-int-ℕ n nx) ∙ ap (int-ℕ n *ℤ_) nx=x)
-          ( le-natural-le-ℤ
+          ( preserves-le-int-ℕ
             ( nat-nonnegative-ℤ (y , nonneg-y))
             ( n *ℕ nx)
             ( ny<n*nx))
@@ -71,7 +71,7 @@ abstract
       pos-ℤ-to-ℕ (inr (inr n)) H = succ-ℕ n , (λ ()) , refl
 
   archimedean-property-ℤ :
-    (x y : ℤ) → is-positive-ℤ x → exists ℕ (λ n → le-ℤ-Prop y (int-ℕ n *ℤ x))
+    (x y : ℤ) → is-positive-ℤ x → exists ℕ (λ n → le-prop-ℤ y (int-ℕ n *ℤ x))
   archimedean-property-ℤ x y pos-x =
     unit-trunc-Prop (bound-archimedean-property-ℤ x y pos-x)
 ```

src/elementary-number-theory/archimedean-property-natural-numbers.lagda.md

@@ -45,7 +45,7 @@ abstract
         ( strict-upper-bound-remainder-euclidean-division-ℕ x y nonzero-x))
 
   archimedean-property-ℕ :
-    (x y : ℕ) → is-nonzero-ℕ x → exists ℕ (λ n → le-ℕ-Prop y (n *ℕ x))
+    (x y : ℕ) → is-nonzero-ℕ x → exists ℕ (λ n → le-prop-ℕ y (n *ℕ x))
   archimedean-property-ℕ x y nonzero-x =
     unit-trunc-Prop (bound-archimedean-property-ℕ x y nonzero-x)
 ```

src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md

@@ -92,7 +92,7 @@ is-distance-between-multiples-sym-ℕ :
   (x y z : ℕ) → is-distance-between-multiples-ℕ x y z →
   is-distance-between-multiples-ℕ y x z
 is-distance-between-multiples-sym-ℕ x y z (pair k (pair l eqn)) =
-  pair l (pair k (symmetric-dist-ℕ (l *ℕ y) (k *ℕ x) ∙ eqn))
+  pair l (pair k (commutative-dist-ℕ (l *ℕ y) (k *ℕ x) ∙ eqn))
 ```
 
 ## Lemmas
@@ -600,7 +600,7 @@ is-distance-between-multiples-div-mod-ℕ (succ-ℕ x) y z (u , p) =
         dist-ℕ ((abs-ℤ a) *ℕ (succ-ℕ x)) ((nat-Fin (succ-ℕ x) u) *ℕ y)
         ＝ dist-ℕ ((nat-Fin (succ-ℕ x) u) *ℕ y) ((abs-ℤ a) *ℕ (succ-ℕ x))
           by
-          symmetric-dist-ℕ
+          commutative-dist-ℕ
             ( (abs-ℤ a) *ℕ (succ-ℕ x))
             ( (nat-Fin (succ-ℕ x) u) *ℕ y)
         ＝ dist-ℤ
@@ -1304,7 +1304,7 @@ remainder-min-dist-succ-x-is-distance x y =
         ( s *ℕ (succ-ℕ x))
         ( tysx)
         ( inv (dist-sx-ty-eq-d) ∙
-          symmetric-dist-ℕ (s *ℕ (succ-ℕ x)) (t *ℕ y))
+          commutative-dist-ℕ (s *ℕ (succ-ℕ x)) (t *ℕ y))
 
     quotient-min-dist-succ-x-nonzero : is-nonzero-ℕ q
     quotient-min-dist-succ-x-nonzero iszero =
@@ -1708,7 +1708,7 @@ remainder-min-dist-succ-x-is-distance x y =
           ((abs-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ))) *ℕ
             (succ-ℕ x))
             ((q *ℕ t) *ℕ y)
-          by symmetric-dist-ℕ
+          by commutative-dist-ℕ
             ((q *ℕ t) *ℕ y)
             (mul-ℕ (abs-ℤ (add-ℤ (mul-ℤ (int-ℕ q)
               (int-ℕ s)) (neg-ℤ one-ℤ)))
@@ -1914,7 +1914,7 @@ gcd-ℕ-div-dist-between-mult x y z dist =
     rewrite-dist =
       rewrite-right-dist-add-ℕ (t *ℕ y) z (s *ℕ x) tysx
         ( inv (is-distance-between-multiples-eqn-ℕ dist) ∙
-          symmetric-dist-ℕ (s *ℕ x) (t *ℕ y))
+          commutative-dist-ℕ (s *ℕ x) (t *ℕ y))
 
     div-gcd-x : div-ℕ (gcd-ℕ x y) (s *ℕ x)
     div-gcd-x = div-mul-ℕ s (gcd-ℕ x y) x (pr1 (is-common-divisor-gcd-ℕ x y))

src/elementary-number-theory/binomial-coefficients.lagda.md

@@ -10,11 +10,11 @@ module elementary-number-theory.binomial-coefficients where
 open import commutative-algebra.commutative-semirings
 
 open import elementary-number-theory.addition-natural-numbers
-open import elementary-number-theory.commutative-semiring-of-natural-numbers
 open import elementary-number-theory.factorials
 open import elementary-number-theory.inequality-natural-numbers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.semiring-of-natural-numbers
 open import elementary-number-theory.strict-inequality-natural-numbers
 
 open import foundation.action-on-identifications-binary-functions

src/elementary-number-theory/binomial-theorem-natural-numbers.lagda.md

@@ -10,11 +10,11 @@ module elementary-number-theory.binomial-theorem-natural-numbers where
 open import commutative-algebra.binomial-theorem-commutative-semirings
 
 open import elementary-number-theory.addition-natural-numbers
-open import elementary-number-theory.commutative-semiring-of-natural-numbers
 open import elementary-number-theory.distance-natural-numbers
 open import elementary-number-theory.exponentiation-natural-numbers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.semiring-of-natural-numbers
 
 open import foundation.homotopies
 open import foundation.identity-types

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

@@ -28,6 +28,14 @@ open import foundation.universe-levels
 
 </details>
 
+## Idea
+
+Two [integers](elementary-number-theory.integers.md) are
+{{#concept "congruent" WDID=Q3773677 WD="congruence of integers" Agda=cong-ℤ}}
+mod an integer `k` if their
+[difference](elementary-number-theory.difference-integers.md) is
+[divisible](elementary-number-theory.divisibility-integers.md) by `k`.
+
 ## Definitions
 
 ```agda
@@ -40,6 +48,8 @@ is-cong-zero-ℤ k x = cong-ℤ k x zero-ℤ
 
 ## Properties
 
+### `k | x` if and only if `x` is congruent to zero mod `k`
+
 ```agda
 is-cong-zero-div-ℤ : (k x : ℤ) → div-ℤ k x → is-cong-zero-ℤ k x
 pr1 (is-cong-zero-div-ℤ k x (pair d p)) = d
@@ -48,33 +58,55 @@ pr2 (is-cong-zero-div-ℤ k x (pair d p)) = p ∙ inv (right-unit-law-add-ℤ x)
 div-is-cong-zero-ℤ : (k x : ℤ) → is-cong-zero-ℤ k x → div-ℤ k x
 pr1 (div-is-cong-zero-ℤ k x (pair d p)) = d
 pr2 (div-is-cong-zero-ℤ k x (pair d p)) = p ∙ right-unit-law-add-ℤ x
+```
 
+### If `k` is a unit, all integers are congruent mod `k`
+
+```agda
 is-indiscrete-cong-ℤ : (k : ℤ) → is-unit-ℤ k → (x y : ℤ) → cong-ℤ k x y
 is-indiscrete-cong-ℤ k H x y = div-is-unit-ℤ k (x -ℤ y) H
+```
 
+### If `k` is zero and `x` and `y` are congruent mod `k`, `x = y`
+
+```agda
 is-discrete-cong-ℤ : (k : ℤ) → is-zero-ℤ k → (x y : ℤ) → cong-ℤ k x y → x ＝ y
 is-discrete-cong-ℤ .zero-ℤ refl x y K =
   eq-diff-ℤ (is-zero-div-zero-ℤ (x -ℤ y) K)
+```
+
+### If `x` and `succ-ℤ x` are congruent mod `k`, `k` is a unit
+
+```agda
+abstract
+  is-unit-cong-succ-ℤ : (k x : ℤ) → cong-ℤ k x (succ-ℤ x) → is-unit-ℤ k
+  pr1 (is-unit-cong-succ-ℤ k x (pair y p)) = neg-ℤ y
+  pr2 (is-unit-cong-succ-ℤ k x (pair y p)) =
+    ( left-negative-law-mul-ℤ y k) ∙
+    ( is-injective-neg-ℤ
+      ( ( neg-neg-ℤ (y *ℤ k)) ∙
+        ( ( p) ∙
+          ( ( ap (x +ℤ_) (neg-succ-ℤ x)) ∙
+            ( ( right-predecessor-law-add-ℤ x (neg-ℤ x)) ∙
+              ( ap pred-ℤ (right-inverse-law-add-ℤ x)))))))
+```
+
+### If `x` and `pred-ℤ x` are congruent mod `k`, `k` is a unit
 
-is-unit-cong-succ-ℤ : (k x : ℤ) → cong-ℤ k x (succ-ℤ x) → is-unit-ℤ k
-pr1 (is-unit-cong-succ-ℤ k x (pair y p)) = neg-ℤ y
-pr2 (is-unit-cong-succ-ℤ k x (pair y p)) =
-  ( left-negative-law-mul-ℤ y k) ∙
-  ( is-injective-neg-ℤ
-    ( ( neg-neg-ℤ (y *ℤ k)) ∙
-      ( ( p) ∙
-        ( ( ap (x +ℤ_) (neg-succ-ℤ x)) ∙
-          ( ( right-predecessor-law-add-ℤ x (neg-ℤ x)) ∙
-            ( ap pred-ℤ (right-inverse-law-add-ℤ x)))))))
-
-is-unit-cong-pred-ℤ : (k x : ℤ) → cong-ℤ k x (pred-ℤ x) → is-unit-ℤ k
-pr1 (is-unit-cong-pred-ℤ k x (pair y p)) = y
-pr2 (is-unit-cong-pred-ℤ k x (pair y p)) =
-  ( p) ∙
-  ( ( ap (x +ℤ_) (neg-pred-ℤ x)) ∙
-    ( ( right-successor-law-add-ℤ x (neg-ℤ x)) ∙
-      ( ap succ-ℤ (right-inverse-law-add-ℤ x))))
+```agda
+abstract
+  is-unit-cong-pred-ℤ : (k x : ℤ) → cong-ℤ k x (pred-ℤ x) → is-unit-ℤ k
+  pr1 (is-unit-cong-pred-ℤ k x (pair y p)) = y
+  pr2 (is-unit-cong-pred-ℤ k x (pair y p)) =
+    ( p) ∙
+    ( ( ap (x +ℤ_) (neg-pred-ℤ x)) ∙
+      ( ( right-successor-law-add-ℤ x (neg-ℤ x)) ∙
+        ( ap succ-ℤ (right-inverse-law-add-ℤ x))))
+```
 
+### Congruence mod `k` is an equivalence relation
+
+```agda
 refl-cong-ℤ : (k : ℤ) → is-reflexive (cong-ℤ k)
 pr1 (refl-cong-ℤ k x) = zero-ℤ
 pr2 (refl-cong-ℤ k x) = left-zero-law-mul-ℤ k ∙ inv (is-zero-diff-ℤ' x)
@@ -92,7 +124,11 @@ pr2 (transitive-cong-ℤ k x y z (pair e q) (pair d p)) =
   ( right-distributive-mul-add-ℤ d e k) ∙
   ( ( ap-add-ℤ p q) ∙
     ( triangle-diff-ℤ x y z))
+```
 
+### Concatenating congruence and equality
+
+```agda
 concatenate-eq-cong-ℤ :
   (k x x' y : ℤ) → x ＝ x' → cong-ℤ k x' y → cong-ℤ k x y
 concatenate-eq-cong-ℤ k x .x y refl = id
@@ -114,7 +150,11 @@ concatenate-cong-cong-cong-ℤ :
   (k x y z w : ℤ) → cong-ℤ k x y → cong-ℤ k y z → cong-ℤ k z w → cong-ℤ k x w
 concatenate-cong-cong-cong-ℤ k x y z w H K L =
   transitive-cong-ℤ k x y w (transitive-cong-ℤ k y z w L K) H
+```
 
+### If `-x` and `-y` are congruent mod `k`, so are `x` and `y`
+
+```agda
 cong-cong-neg-ℤ : (k x y : ℤ) → cong-ℤ k (neg-ℤ x) (neg-ℤ y) → cong-ℤ k x y
 pr1 (cong-cong-neg-ℤ k x y (pair d p)) = neg-ℤ d
 pr2 (cong-cong-neg-ℤ k x y (pair d p)) =
@@ -131,6 +171,8 @@ pr2 (cong-neg-cong-ℤ k x y (pair d p)) =
     ( distributive-neg-add-ℤ x (neg-ℤ y)))
 ```
 
+### The canonical embedding of natural numbers preserves and reflects congruence
+
 ```agda
 cong-int-cong-ℕ :
   (k x y : ℕ) → cong-ℕ k x y → cong-ℤ (int-ℕ k) (int-ℕ x) (int-ℕ y)

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

@@ -80,7 +80,7 @@ cong-identification-ℕ k {x} refl = refl-cong-ℕ k x
 
 symmetric-cong-ℕ : (k : ℕ) → is-symmetric (cong-ℕ k)
 pr1 (symmetric-cong-ℕ k x y (pair d p)) = d
-pr2 (symmetric-cong-ℕ k x y (pair d p)) = p ∙ (symmetric-dist-ℕ x y)
+pr2 (symmetric-cong-ℕ k x y (pair d p)) = p ∙ (commutative-dist-ℕ x y)
 
 cong-zero-ℕ' : (k : ℕ) → cong-ℕ k zero-ℕ k
 cong-zero-ℕ' k =