Merge branch 'master' into min-max-lower-upper

UniMath · Mar 4, 2025 · 8f059f3 · 8f059f3
2 parents 70959e0 + 54a5397
commit 8f059f3
Show file tree

Hide file tree

Showing 49 changed files with 1,391 additions and 368 deletions.
diff --git a/.github/workflows/pages.yaml b/.github/workflows/pages.yaml
@@ -84,6 +84,9 @@ jobs:
           crate: mdbook-catppuccin
           version: '1.2.0'
 
+      - name: Install Graphviz
+        run: sudo apt-get install -y graphviz
+
       - uses: actions/setup-python@v5
         with:
           python-version: '3.8'

diff --git a/.gitignore b/.gitignore
@@ -430,3 +430,4 @@ SUMMARY.md
 CONTRIBUTORS.md
 MAINTAINERS.md
 /website/css/Agda-highlight.css
+/website/images/agda_dependency_graph.svg
diff --git a/HOWTO-INSTALL.md b/HOWTO-INSTALL.md
@@ -21,8 +21,8 @@ In order to contribute to the agda-unimath library you will additionally need:
 1. `git`
 2. `make`
 3. `python` version 3.8 or newer
-4. The python libraries `pre-commit`, `pybtex`, `requests` and `tomli`. Those
-   can be installed by running
+4. The python libraries `pre-commit`, `pybtex`, `requests`, `tomli`, and
+   `graphviz`. These can be installed by running
    ```shell
    python3 -m pip install -r scripts/requirements.txt
    ```
@@ -33,6 +33,7 @@ In order to contribute to the agda-unimath library you will additionally need:
    ```shell
    make install-website-dev
    ```
+7. `graphviz`
 
 All of these can also be installed in one go by using `nix`. In the section
 [Creating a setup for contributors](#contributor-setup) we will walk you through

diff --git a/Makefile b/Makefile
@@ -145,8 +145,12 @@ CONTRIBUTORS.md: ${AGDAFILES} ${CONTRIBUTORS_FILE} ./scripts/generate_contributo
 website/css/Agda-highlight.css: ./scripts/generate_agda_css.py ./theme/catppuccin.css
 	@python3 ./scripts/generate_agda_css.py
 
+website/images/agda_dependency_graph.svg: ${AGDAFILES}
+	@python3 ./scripts/generate_dependency_graph_rendering.py website/images/agda_dependency_graph svg || true
+
 .PHONY: website-prepare
-website-prepare: agda-html ./SUMMARY.md ./CONTRIBUTORS.md ./MAINTAINERS.md ./website/css/Agda-highlight.css
+website-prepare: agda-html ./SUMMARY.md ./CONTRIBUTORS.md ./MAINTAINERS.md \
+								 ./website/css/Agda-highlight.css ./website/images/agda_dependency_graph.svg
 	@cp $(METAFILES) ./docs/
 	@mkdir -p ./docs/website
 	@cp -r ./website/images ./docs/website/
@@ -157,7 +161,6 @@ website-prepare: agda-html ./SUMMARY.md ./CONTRIBUTORS.md ./MAINTAINERS.md ./web
 .PHONY: website
 website: website-prepare
 	@mdbook build
-	@python3 ./scripts/generate_dependency_graph_rendering.py website/images/agda_dependency_graph svg || true
 
 .PHONY: serve-website
 serve-website: website-prepare

diff --git a/scripts/generate_dependency_graph_rendering.py b/scripts/generate_dependency_graph_rendering.py
@@ -99,7 +99,7 @@ def count_imports(graph):
             import_counts[dep] += 1
     return import_counts
 
-def build_dependency_graph(root_dir, min_rank_imports=20):
+def build_dependency_graph(root_dir, most_imported_drop_count=20):
     """Construct a dependency graph from Agda files."""
     graph = defaultdict(set)
     file_sizes = {}
@@ -117,7 +117,7 @@ def build_dependency_graph(root_dir, min_rank_imports=20):
 
     # Count imports and find top imported modules
     import_counts = count_imports(graph)
-    _top_imports = sorted(import_counts, key=import_counts.get, reverse=True)[:min_rank_imports]
+    _top_imports = sorted(import_counts, key=import_counts.get, reverse=True)[:most_imported_drop_count]
     top_imports = set(_top_imports)
 
     eprint("Excluding modules:")
@@ -143,6 +143,7 @@ def render_graph(graph, file_sizes, output_file, format, repo):
     dot.attr(splines="false", overlap="prism10000", bgcolor="#FFFFFF00", K="0.3", repulsiveforce="0.3") #sfdp
 
     max_lines = max(file_sizes.values(), default=1)
+    eprint("Maximum lines of code:", max_lines)
     node_sizes = {node: max(0.05, 0.3 * math.sqrt(file_sizes.get(node, 0) / max_lines)) for node in graph}
     node_colors = {node: module_based_color(node[:node.rfind(".")], label_colors) for node in graph}
 
@@ -158,14 +159,14 @@ def render_graph(graph, file_sizes, output_file, format, repo):
 
 if __name__ == "__main__":
     root_dir = "src"
-    min_rank_imports = 20
+    most_imported_drop_count = 20
 
     parser = argparse.ArgumentParser(description="Generate Agda dependency graph.")
     parser.add_argument("output_file", type=str, help="Path to save the output graph.")
     parser.add_argument("format", type=str, choices=["svg", "png", "pdf"], help="Output format of the graph.")
 
     args = parser.parse_args()
 
-    graph, file_sizes = build_dependency_graph(root_dir, min_rank_imports=min_rank_imports)
+    graph, file_sizes = build_dependency_graph(root_dir, most_imported_drop_count=most_imported_drop_count)
     render_graph(graph, file_sizes, args.output_file, format=args.format, repo=GITHUB_REPO)
     eprint(f"Graph saved as {args.output_file}.{args.format}")
diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md
@@ -20,6 +20,7 @@ open import elementary-number-theory.additive-group-of-rational-numbers public
 open import elementary-number-theory.archimedean-property-integer-fractions public
 open import elementary-number-theory.archimedean-property-integers public
 open import elementary-number-theory.archimedean-property-natural-numbers public
+open import elementary-number-theory.archimedean-property-positive-rational-numbers public
 open import elementary-number-theory.archimedean-property-rational-numbers public
 open import elementary-number-theory.arithmetic-functions public
 open import elementary-number-theory.based-induction-natural-numbers public
@@ -59,6 +60,7 @@ open import elementary-number-theory.divisibility-standard-finite-types public
 open import elementary-number-theory.equality-conatural-numbers public
 open import elementary-number-theory.equality-integers public
 open import elementary-number-theory.equality-natural-numbers public
+open import elementary-number-theory.equality-rational-numbers public
 open import elementary-number-theory.euclid-mullin-sequence public
 open import elementary-number-theory.euclidean-division-natural-numbers public
 open import elementary-number-theory.eulers-totient-function public
@@ -174,6 +176,7 @@ open import elementary-number-theory.triangular-numbers public
 open import elementary-number-theory.twin-prime-conjecture public
 open import elementary-number-theory.type-arithmetic-natural-numbers public
 open import elementary-number-theory.unit-elements-standard-finite-types public
+open import elementary-number-theory.unit-fractions-rational-numbers public
 open import elementary-number-theory.unit-similarity-standard-finite-types public
 open import elementary-number-theory.universal-property-conatural-numbers public
 open import elementary-number-theory.universal-property-integers public

diff --git a/src/elementary-number-theory/archimedean-property-integer-fractions.lagda.md b/src/elementary-number-theory/archimedean-property-integer-fractions.lagda.md
@@ -23,6 +23,7 @@ open import elementary-number-theory.strict-inequality-integers
 open import foundation.dependent-pair-types
 open import foundation.existential-quantification
 open import foundation.identity-types
+open import foundation.propositional-truncations
 open import foundation.transport-along-identifications
 ```
 
@@ -36,28 +37,31 @@ than `n` as an integer fraction times `x`.
 
 ```agda
 abstract
+  bound-archimedean-property-fraction-ℤ :
+    (x y : fraction-ℤ) →
+    is-positive-fraction-ℤ x →
+    Σ ℕ (λ n → le-fraction-ℤ y (in-fraction-ℤ (int-ℕ n) *fraction-ℤ x))
+  bound-archimedean-property-fraction-ℤ
+    x@(px , qx , pos-qx) y@(py , qy , pos-qy) pos-px =
+      let
+        (n , H) =
+          bound-archimedean-property-ℤ
+            ( px *ℤ qy)
+            ( py *ℤ qx)
+            ( is-positive-mul-ℤ pos-px pos-qy)
+      in
+        n ,
+        tr
+          ( le-ℤ (py *ℤ qx))
+          ( inv (associative-mul-ℤ (int-ℕ n) px qy))
+          ( H)
+
   archimedean-property-fraction-ℤ :
     (x y : fraction-ℤ) →
     is-positive-fraction-ℤ x →
     exists
       ℕ
       (λ n → le-fraction-ℤ-Prop y (in-fraction-ℤ (int-ℕ n) *fraction-ℤ x))
-  archimedean-property-fraction-ℤ
-    x@(px , qx , pos-qx) y@(py , qy , pos-qy) pos-px =
-      elim-exists
-        (∃
-          ( ℕ)
-          ( λ n →
-            le-fraction-ℤ-Prop y (in-fraction-ℤ (int-ℕ n) *fraction-ℤ x)))
-        ( λ n H →
-          intro-exists
-            ( n)
-            ( tr
-              ( le-ℤ (py *ℤ qx))
-              ( inv (associative-mul-ℤ (int-ℕ n) px qy))
-              ( H)))
-        ( archimedean-property-ℤ
-          ( px *ℤ qy)
-          ( py *ℤ qx)
-          ( is-positive-mul-ℤ pos-px pos-qy))
+  archimedean-property-fraction-ℤ x y pos-x =
+    unit-trunc-Prop (bound-archimedean-property-fraction-ℤ x y pos-x)
 ```
diff --git a/src/elementary-number-theory/archimedean-property-integers.lagda.md b/src/elementary-number-theory/archimedean-property-integers.lagda.md
@@ -24,8 +24,8 @@ open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.existential-quantification
 open import foundation.identity-types
+open import foundation.propositional-truncations
 open import foundation.transport-along-identifications
-open import foundation.unit-type
 ```
 
 </details>
@@ -40,35 +40,40 @@ integer `y`, there is an `n : ℕ` such that `y < int-ℕ n *ℤ x`.
 
 ```agda
 abstract
+  bound-archimedean-property-ℤ :
+    (x y : ℤ) → is-positive-ℤ x → Σ ℕ (λ n → le-ℤ y (int-ℕ n *ℤ x))
+  bound-archimedean-property-ℤ x y pos-x
+    with decide-is-negative-is-nonnegative-ℤ {y}
+  ... | inl neg-y = zero-ℕ , le-zero-is-negative-ℤ y neg-y
+  ... | inr nonneg-y =
+      let
+        (nx , nonzero-nx , nx=x) = pos-ℤ-to-ℕ x pos-x
+        (n , ny<n*nx) =
+          bound-archimedean-property-ℕ
+            ( nx)
+            ( nat-nonnegative-ℤ (y , nonneg-y))
+            ( nonzero-nx)
+      in
+        n ,
+        binary-tr
+          ( le-ℤ)
+          ( ap pr1 (is-section-nat-nonnegative-ℤ (y , nonneg-y)))
+          ( inv (mul-int-ℕ n nx) ∙ ap (int-ℕ n *ℤ_) nx=x)
+          ( le-natural-le-ℤ
+            ( nat-nonnegative-ℤ (y , nonneg-y))
+            ( n *ℕ nx)
+            ( ny<n*nx))
+    where
+      pos-ℤ-to-ℕ :
+        (z : ℤ) →
+        is-positive-ℤ z →
+        Σ ℕ (λ n → is-nonzero-ℕ n × (int-ℕ n ＝ z))
+      pos-ℤ-to-ℕ (inr (inr n)) H = succ-ℕ n , (λ ()) , refl
+
   archimedean-property-ℤ :
     (x y : ℤ) → is-positive-ℤ x → exists ℕ (λ n → le-ℤ-Prop y (int-ℕ n *ℤ x))
-  archimedean-property-ℤ x y pos-x with decide-is-negative-is-nonnegative-ℤ {y}
-  ... | inl neg-y = intro-exists zero-ℕ (le-zero-is-negative-ℤ y neg-y)
-  ... | inr nonneg-y =
-      ind-Σ
-        ( λ nx (nonzero-nx , nx=x) →
-          elim-exists
-            (∃ ℕ (λ n → le-ℤ-Prop y (int-ℕ n *ℤ x)))
-            ( λ n ny<n*nx →
-              intro-exists
-                ( n)
-                ( binary-tr
-                  ( le-ℤ)
-                  ( ap pr1 (is-section-nat-nonnegative-ℤ (y , nonneg-y)))
-                  ( inv (mul-int-ℕ n nx) ∙ ap (int-ℕ n *ℤ_) nx=x)
-                  ( le-natural-le-ℤ
-                    ( nat-nonnegative-ℤ (y , nonneg-y))
-                    ( n *ℕ nx)
-                    ( ny<n*nx))))
-            ( archimedean-property-ℕ
-              ( nx)
-              ( nat-nonnegative-ℤ (y , nonneg-y)) nonzero-nx))
-        (pos-ℤ-to-ℕ x pos-x)
-    where pos-ℤ-to-ℕ :
-            (z : ℤ) →
-              is-positive-ℤ z →
-              Σ ℕ (λ n → is-nonzero-ℕ n × (int-ℕ n ＝ z))
-          pos-ℤ-to-ℕ (inr (inr n)) H = succ-ℕ n , (λ ()) , refl
+  archimedean-property-ℤ x y pos-x =
+    unit-trunc-Prop (bound-archimedean-property-ℤ x y pos-x)
 ```
 
 ## External links

diff --git a/src/elementary-number-theory/archimedean-property-natural-numbers.lagda.md b/src/elementary-number-theory/archimedean-property-natural-numbers.lagda.md
@@ -7,7 +7,6 @@ module elementary-number-theory.archimedean-property-natural-numbers where
 <details><summary>Imports</summary>
 
 ```agda
-open import elementary-number-theory.equality-natural-numbers
 open import elementary-number-theory.euclidean-division-natural-numbers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
@@ -16,6 +15,7 @@ open import elementary-number-theory.strict-inequality-natural-numbers
 
 open import foundation.dependent-pair-types
 open import foundation.existential-quantification
+open import foundation.propositional-truncations
 open import foundation.transport-along-identifications
 ```
 
@@ -31,19 +31,23 @@ for any nonzero natural number `x` and any natural number `y`, there is an
 
 ```agda
 abstract
+  bound-archimedean-property-ℕ :
+    (x y : ℕ) → is-nonzero-ℕ x → Σ ℕ (λ n → le-ℕ y (n *ℕ x))
+  bound-archimedean-property-ℕ x y nonzero-x =
+    succ-ℕ (quotient-euclidean-division-ℕ x y) ,
+    tr
+      ( λ z → z <-ℕ succ-ℕ (quotient-euclidean-division-ℕ x y) *ℕ x)
+      ( eq-euclidean-division-ℕ x y)
+      ( preserves-le-left-add-ℕ
+        ( quotient-euclidean-division-ℕ x y *ℕ x)
+        ( remainder-euclidean-division-ℕ x y)
+        ( x)
+        ( strict-upper-bound-remainder-euclidean-division-ℕ x y nonzero-x))
+
   archimedean-property-ℕ :
     (x y : ℕ) → is-nonzero-ℕ x → exists ℕ (λ n → le-ℕ-Prop y (n *ℕ x))
   archimedean-property-ℕ x y nonzero-x =
-    intro-exists
-      (succ-ℕ (quotient-euclidean-division-ℕ x y))
-      ( tr
-        ( λ z → z <-ℕ succ-ℕ (quotient-euclidean-division-ℕ x y) *ℕ x)
-        ( eq-euclidean-division-ℕ x y)
-        ( preserves-le-left-add-ℕ
-          ( quotient-euclidean-division-ℕ x y *ℕ x)
-          ( remainder-euclidean-division-ℕ x y)
-          ( x)
-          ( strict-upper-bound-remainder-euclidean-division-ℕ x y nonzero-x)))
+    unit-trunc-Prop (bound-archimedean-property-ℕ x y nonzero-x)
 ```
 
 ## External links

diff --git a/...lementary-number-theory/archimedean-property-positive-rational-numbers.lagda.md b/...lementary-number-theory/archimedean-property-positive-rational-numbers.lagda.md
@@ -0,0 +1,74 @@
+# The Archimedean property of the positive rational numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module elementary-number-theory.archimedean-property-positive-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.archimedean-property-rational-numbers
+open import elementary-number-theory.integers
+open import elementary-number-theory.multiplication-rational-numbers
+open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.nonzero-natural-numbers
+open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.strict-inequality-rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.identity-types
+open import foundation.propositional-truncations
+open import foundation.transport-along-identifications
+```
+
+</details>
+
+## Definition
+
+The
+{{#concept "Archimedean property" Disambiguation="positive rational numbers" Agda=archimedean-property-ℚ⁺}}
+of `ℚ⁺` is that for any two
+[positive rational numbers](elementary-number-theory.positive-rational-numbers.md)
+`x y : ℚ⁺`, there is a
+[nonzero natural number](elementary-number-theory.nonzero-natural-numbers.md)
+`n` such that `y` is
+[less than](elementary-number-theory.strict-inequality-rational-numbers.md) `n`
+times `x`.
+
+```agda
+abstract
+  bound-archimedean-property-ℚ⁺ :
+    (x y : ℚ⁺) →
+    Σ ℕ⁺ (λ n → le-ℚ⁺ y (positive-rational-ℕ⁺ n *ℚ⁺ x))
+  bound-archimedean-property-ℚ⁺ (x , pos-x) (y , pos-y) =
+    let
+      (n , y<nx) = bound-archimedean-property-ℚ x y pos-x
+      n≠0 : is-nonzero-ℕ n
+      n≠0 n=0 =
+        asymmetric-le-ℚ
+          ( zero-ℚ)
+          ( y)
+          ( le-zero-is-positive-ℚ y pos-y)
+          ( tr
+            ( le-ℚ y)
+            ( equational-reasoning
+              rational-ℤ (int-ℕ n) *ℚ x
+              ＝ rational-ℤ (int-ℕ 0) *ℚ x
+                by ap (λ m → rational-ℤ (int-ℕ m) *ℚ x) n=0
+              ＝ zero-ℚ by left-zero-law-mul-ℚ x)
+            y<nx)
+    in (n , n≠0) , y<nx
+
+  archimedean-property-ℚ⁺ :
+    (x y : ℚ⁺) →
+    exists ℕ⁺ (λ n → le-prop-ℚ⁺ y (positive-rational-ℕ⁺ n *ℚ⁺ x))
+  archimedean-property-ℚ⁺ x y =
+    unit-trunc-Prop (bound-archimedean-property-ℚ⁺ x y)
+```