From b5ec17ab5587f14c3ce8656f9478bdfcb2c960f6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Vojt=C4=9Bch=20=C5=A0t=C4=9Bpan=C4=8D=C3=ADk?= Date: Tue, 27 Feb 2024 17:13:25 +0100 Subject: [PATCH 1/5] Add netlify environment variables to benchmark deployment action (#1044) This _should_ enable deployments of the benchmarking website --- .github/workflows/profiling.yaml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.github/workflows/profiling.yaml b/.github/workflows/profiling.yaml index 6f2beafcd0..5f265e1e34 100644 --- a/.github/workflows/profiling.yaml +++ b/.github/workflows/profiling.yaml @@ -74,5 +74,8 @@ jobs: echo 'window.BENCHMARK_DATA =' | cat - ../benchmark-cache/data.json > benchmark-website/data.js - name: Deploy the new profiling website + env: + NETLIFY_SITE_ID: ${{ secrets.PERF_SITE_ID }} + NETLIFY_AUTH_TOKEN: ${{ secrets.PERF_SITE_KEY }} run: | - npx netlify-cli deploy --dir=benchmark-website + npx netlify-cli deploy --prod --dir=benchmark-website From d5f63de0ff6f01f6df97a4c1909aa1dd012f2553 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 27 Feb 2024 17:16:58 +0100 Subject: [PATCH 2/5] Track user analytics for website (#1035) This simple addition tracks some anonymous user data using GoatCounter. - [x] Create `agda-unimath` user at [GoatCounter](https://www.goatcounter.com/) - [x] Inject GoatCounter script Resolves #1029 --- theme/index.hbs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/theme/index.hbs b/theme/index.hbs index 13935f31c1..fb365846a4 100644 --- a/theme/index.hbs +++ b/theme/index.hbs @@ -332,6 +332,8 @@ {{/if}} + + From b5985b52cb65fa9b2da4b961983ee1a1f5c4f6dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Vojt=C4=9Bch=20=C5=A0t=C4=9Bpan=C4=8D=C3=ADk?= Date: Tue, 27 Feb 2024 17:34:04 +0100 Subject: [PATCH 3/5] Fix benchmark deployment directory (#1045) --- .github/workflows/profiling.yaml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/.github/workflows/profiling.yaml b/.github/workflows/profiling.yaml index 5f265e1e34..e153d46398 100644 --- a/.github/workflows/profiling.yaml +++ b/.github/workflows/profiling.yaml @@ -67,11 +67,10 @@ jobs: - name: Prepare new revision of the profiling website run: | - cd repo mkdir -p benchmark-website - cp website/benchmarks/index.html benchmark-website/ - cp ../benchmark-cache/data.* benchmark-website/ - echo 'window.BENCHMARK_DATA =' | cat - ../benchmark-cache/data.json > benchmark-website/data.js + cp repo/website/benchmarks/index.html benchmark-website/ + cp benchmark-cache/data.* benchmark-website/ + echo 'window.BENCHMARK_DATA =' | cat - benchmark-cache/data.json > benchmark-website/data.js - name: Deploy the new profiling website env: From 053072398cd5a6a50c82518dfa0caa60c8342969 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 27 Feb 2024 17:52:21 +0100 Subject: [PATCH 4/5] A small optimization to equivalence relations (#1040) - Makes equivalence relations typecheck in about half the time. I also had a look at `category-of-functors-from-small-to-large-categories`, and I really can't find anything wrong, so I'm a bit puzzled. - Adds a make hook for more streamlined profiling of individual modules. --- .vscode/settings.json | 10 +- Makefile | 77 ++++++-- .../abstract-quaternion-group.lagda.md | 32 +-- .../descent-coproduct-types.lagda.md | 2 + src/foundation/equivalence-relations.lagda.md | 184 ++++++++---------- src/foundation/partitions.lagda.md | 179 ++++++++--------- .../type-arithmetic-unit-type.lagda.md | 40 ++-- .../higher-modalities.lagda.md | 2 +- .../universal-cover-circle.lagda.md | 2 + ...tations-complete-undirected-graph.lagda.md | 100 +++++----- 10 files changed, 335 insertions(+), 293 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index b26a54f715..c4b4244f33 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -27,10 +27,7 @@ "files.exclude": { "MAlonzo/": true, "**/MAlonzo/": true, - "_build/": true, - "**/_build/": true, - "agdaFiles": true, - "src/temp/": true + "agdaFiles": true }, // Snippet setup @@ -94,6 +91,11 @@ "editor.autoClosingBrackets": "never" }, + "[makefile]": { + "editor.insertSpaces": false, + "editor.detectIndentation": true + }, + "[markdown]": { "editor.rulers": [80], "editor.quickSuggestions": { diff --git a/Makefile b/Makefile index 91e96b4c5c..02ea8b2885 100644 --- a/Makefile +++ b/Makefile @@ -25,24 +25,24 @@ AGDA ?= agda $(AGDAVERBOSE) $(AGDARTS) TIME ?= time METAFILES := \ - ART.md \ - 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 \ + ART.md \ + 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: @@ -75,6 +75,47 @@ check: ./src/everything.lagda.md check-profile: ./src/everything.lagda.md ${AGDA} ${AGDAPROFILEFLAGS} $? +# Base directory where Agda interface files are stored +BUILD_DIR := ./_build +# Directory for temporary files +TEMP_DIR := ./temp +# Convert module path to directory path (replace dots with slashes) +MODULE_DIR = $(subst .,/,$(MODULE)) + + +# Default agda arguments for `profile-module` +PROFILE_MODULE_AGDA_ARGS ?= --profile=definitions +# Target for profiling the typechecking a single module +.PHONY: profile-module +profile-module: + @if [ -z "$(MODULE)" ]; then \ + echo "\033[0;31mError: MODULE variable is not set.\033[0m"; \ + echo "\033[0;31mUsage: make check-module MODULE=\"YourModuleName\"\033[0m"; \ + exit 1; \ + fi + @# Attempt to delete the interface file only if the build directory exists + @echo "\033[0;32mAttempting to delete interface file for $(MODULE)\033[0m" + @find $(BUILD_DIR) -type f -path "*/agda/src/$(MODULE_DIR).agdai" -exec rm -f {} \+ 2>/dev/null || \ + echo "\033[0;31m$(BUILD_DIR) directory does not exist, skipping deletion of interface files.\033[0m" + @# Ensure the temporary directory exists + @mkdir -p $(TEMP_DIR) + @# Profile typechecking the module and capture the output in the temp directory, also display on terminal + @echo "\033[0;32mProfiling typechecking of $(MODULE)\033[0m" + @$(AGDA) $(PROFILE_MODULE_AGDA_ARGS) src/$(MODULE_DIR).lagda.md 2>&1 | tee $(TEMP_DIR)/typecheck_output.txt + @# Check for additional modules being typechecked by looking for any indented "Checking" line + @if grep -E "^\s+Checking " $(TEMP_DIR)/typecheck_output.txt > /dev/null; then \ + echo "\033[0;31mOther modules were also checked. Repeating profiling after deleting interface file again.\033[0m"; \ + find $(BUILD_DIR) -type f -path "*/agda/src/$(MODULE_DIR).agdai" -exec rm -f {} \+; \ + $(AGDA) $(PROFILE_MODULE_AGDA_ARGS) src/$(MODULE_DIR).lagda.md; \ + else \ + echo "\033[0;32mOnly $(MODULE) was checked. Profiling complete.\033[0m"; \ + fi + + @# Cleanup + @rm -f $(TEMP_DIR)/typecheck_output.txt + + + agda-html: ./src/everything.lagda.md @rm -rf ./docs/ @mkdir -p ./docs/ diff --git a/src/finite-group-theory/abstract-quaternion-group.lagda.md b/src/finite-group-theory/abstract-quaternion-group.lagda.md index e995599b64..e550600c66 100644 --- a/src/finite-group-theory/abstract-quaternion-group.lagda.md +++ b/src/finite-group-theory/abstract-quaternion-group.lagda.md @@ -866,14 +866,14 @@ is-noncommutative-mul-Q8 : is-noncommutative-mul-Q8 f = Eq-eq-Q8 (f i-Q8 j-Q8) map-equiv-count-Q8 : Fin 8 → Q8 -map-equiv-count-Q8 (inl (inl (inl (inl (inl (inl (inl (inr star)))))))) = e-Q8 -map-equiv-count-Q8 (inl (inl (inl (inl (inl (inl (inr star))))))) = -e-Q8 -map-equiv-count-Q8 (inl (inl (inl (inl (inl (inr star)))))) = i-Q8 -map-equiv-count-Q8 (inl (inl (inl (inl (inr star))))) = -i-Q8 -map-equiv-count-Q8 (inl (inl (inl (inr star)))) = j-Q8 -map-equiv-count-Q8 (inl (inl (inr star))) = -j-Q8 -map-equiv-count-Q8 (inl (inr star)) = k-Q8 -map-equiv-count-Q8 (inr star) = -k-Q8 +map-equiv-count-Q8 (inl (inl (inl (inl (inl (inl (inl (inr _)))))))) = e-Q8 +map-equiv-count-Q8 (inl (inl (inl (inl (inl (inl (inr _))))))) = -e-Q8 +map-equiv-count-Q8 (inl (inl (inl (inl (inl (inr _)))))) = i-Q8 +map-equiv-count-Q8 (inl (inl (inl (inl (inr _))))) = -i-Q8 +map-equiv-count-Q8 (inl (inl (inl (inr _)))) = j-Q8 +map-equiv-count-Q8 (inl (inl (inr _))) = -j-Q8 +map-equiv-count-Q8 (inl (inr _)) = k-Q8 +map-equiv-count-Q8 (inr _) = -k-Q8 map-inv-equiv-count-Q8 : Q8 → Fin 8 map-inv-equiv-count-Q8 e-Q8 = inl (inl (inl (inl (inl (inl (inl (inr star))))))) @@ -899,16 +899,16 @@ is-section-map-inv-equiv-count-Q8 -k-Q8 = refl is-retraction-map-inv-equiv-count-Q8 : ( map-inv-equiv-count-Q8 ∘ map-equiv-count-Q8) ~ id is-retraction-map-inv-equiv-count-Q8 - (inl (inl (inl (inl (inl (inl (inl (inr star)))))))) = refl + (inl (inl (inl (inl (inl (inl (inl (inr _)))))))) = refl is-retraction-map-inv-equiv-count-Q8 - (inl (inl (inl (inl (inl (inl (inr star))))))) = refl -is-retraction-map-inv-equiv-count-Q8 (inl (inl (inl (inl (inl (inr star)))))) = + (inl (inl (inl (inl (inl (inl (inr _))))))) = refl +is-retraction-map-inv-equiv-count-Q8 (inl (inl (inl (inl (inl (inr _)))))) = refl -is-retraction-map-inv-equiv-count-Q8 (inl (inl (inl (inl (inr star))))) = refl -is-retraction-map-inv-equiv-count-Q8 (inl (inl (inl (inr star)))) = refl -is-retraction-map-inv-equiv-count-Q8 (inl (inl (inr star))) = refl -is-retraction-map-inv-equiv-count-Q8 (inl (inr star)) = refl -is-retraction-map-inv-equiv-count-Q8 (inr star) = refl +is-retraction-map-inv-equiv-count-Q8 (inl (inl (inl (inl (inr _))))) = refl +is-retraction-map-inv-equiv-count-Q8 (inl (inl (inl (inr _)))) = refl +is-retraction-map-inv-equiv-count-Q8 (inl (inl (inr _))) = refl +is-retraction-map-inv-equiv-count-Q8 (inl (inr _)) = refl +is-retraction-map-inv-equiv-count-Q8 (inr _) = refl is-equiv-map-equiv-count-Q8 : is-equiv map-equiv-count-Q8 is-equiv-map-equiv-count-Q8 = diff --git a/src/foundation/descent-coproduct-types.lagda.md b/src/foundation/descent-coproduct-types.lagda.md index 830753d53c..03c1a582ba 100644 --- a/src/foundation/descent-coproduct-types.lagda.md +++ b/src/foundation/descent-coproduct-types.lagda.md @@ -1,6 +1,8 @@ # Descent for coproduct types ```agda +{-# OPTIONS --lossy-unification #-} + module foundation.descent-coproduct-types where ``` diff --git a/src/foundation/equivalence-relations.lagda.md b/src/foundation/equivalence-relations.lagda.md index 127b324232..821a14f484 100644 --- a/src/foundation/equivalence-relations.lagda.md +++ b/src/foundation/equivalence-relations.lagda.md @@ -126,24 +126,26 @@ module _ is-block-partition-equivalence-relation Q = type-Prop (is-block-prop-partition-equivalence-relation Q) - is-partition-is-equivalence-class-inhabited-subtype-equivalence-relation : - is-partition (is-equivalence-class-inhabited-subtype-equivalence-relation R) - is-partition-is-equivalence-class-inhabited-subtype-equivalence-relation x = - is-contr-equiv - ( Σ ( Σ ( equivalence-class R) - ( λ C → is-in-equivalence-class R C x)) - ( λ t → is-inhabited-subtype (subtype-equivalence-class R (pr1 t)))) - ( ( equiv-right-swap-Σ) ∘e - ( equiv-Σ - ( λ Q → is-in-subtype (subtype-equivalence-class R (pr1 Q)) x) - ( equiv-right-swap-Σ) - ( λ Q → id-equiv))) - ( is-contr-Σ - ( is-torsorial-is-in-equivalence-class R x) - ( center-total-is-in-equivalence-class R x) - ( is-proof-irrelevant-is-prop - ( is-prop-type-trunc-Prop) - ( is-inhabited-subtype-equivalence-class R (class R x)))) + abstract + is-partition-is-equivalence-class-inhabited-subtype-equivalence-relation : + is-partition + ( is-equivalence-class-inhabited-subtype-equivalence-relation R) + is-partition-is-equivalence-class-inhabited-subtype-equivalence-relation x = + is-contr-equiv + ( Σ ( Σ ( equivalence-class R) + ( λ C → is-in-equivalence-class R C x)) + ( λ t → is-inhabited-subtype (subtype-equivalence-class R (pr1 t)))) + ( ( equiv-right-swap-Σ) ∘e + ( equiv-Σ + ( λ Q → is-in-subtype (subtype-equivalence-class R (pr1 Q)) x) + ( equiv-right-swap-Σ) + ( λ Q → id-equiv))) + ( is-contr-Σ + ( is-torsorial-is-in-equivalence-class R x) + ( center-total-is-in-equivalence-class R x) + ( is-proof-irrelevant-is-prop + ( is-prop-type-trunc-Prop) + ( is-inhabited-subtype-equivalence-class R (class R x)))) partition-equivalence-relation : partition l2 (l1 ⊔ l2) A pr1 partition-equivalence-relation = @@ -333,79 +335,64 @@ module _ {l1 l2 : Level} {A : UU l1} (P : partition l1 l2 A) where - is-block-is-equivalence-class-equivalence-relation-partition : - (Q : inhabited-subtype l1 A) → - is-equivalence-class - ( equivalence-relation-partition P) - ( subtype-inhabited-subtype Q) → - is-block-partition P Q - is-block-is-equivalence-class-equivalence-relation-partition Q H = - apply-universal-property-trunc-Prop H - ( subtype-partition P Q) - ( λ (a , K) → - tr - ( is-block-partition P) - ( inv - ( eq-has-same-elements-inhabited-subtype Q - ( inhabited-subtype-block-partition P (class-partition P a)) - ( λ x → - logical-equivalence-reasoning - is-in-inhabited-subtype Q x - ↔ Σ ( block-partition P) - ( λ B → - is-in-block-partition P B a × - is-in-block-partition P B x) - by K x - ↔ is-in-block-partition P (class-partition P a) x - by - iff-equiv - ( ( left-unit-law-Σ-is-contr - ( is-contr-block-containing-element-partition P a) - ( center-block-containing-element-partition P a)) ∘e - ( inv-associative-Σ - ( block-partition P) - ( λ B → is-in-block-partition P B a) - ( λ B → is-in-block-partition P (pr1 B) x)))))) - ( is-block-class-partition P a)) - - is-equivalence-class-is-block-partition : - (Q : inhabited-subtype l1 A) → - is-block-partition P Q → - is-equivalence-class - ( equivalence-relation-partition P) - ( subtype-inhabited-subtype Q) - is-equivalence-class-is-block-partition Q H = - apply-universal-property-trunc-Prop - ( is-inhabited-subtype-inhabited-subtype Q) - ( is-equivalence-class-Prop + abstract + is-block-is-equivalence-class-equivalence-relation-partition : + (Q : inhabited-subtype l1 A) → + is-equivalence-class ( equivalence-relation-partition P) - ( subtype-inhabited-subtype Q)) - ( λ (a , q) → - unit-trunc-Prop - ( pair - ( a) - ( λ x → - iff-equiv - ( equivalence-reasoning - is-in-inhabited-subtype Q x - ≃ is-in-block-partition P (make-block-partition P Q H) x - by - compute-is-in-block-partition P Q H x - ≃ Σ ( block-partition P) - ( λ B → - is-in-block-partition P B a × - is-in-block-partition P B x) - by - inv-equiv - ( ( left-unit-law-Σ-is-contr - ( is-contr-block-containing-element-partition P a) - ( pair - ( make-block-partition P Q H) - ( make-is-in-block-partition P Q H a q))) ∘e - ( inv-associative-Σ - ( block-partition P) - ( λ B → is-in-block-partition P B a) - ( λ B → is-in-block-partition P (pr1 B) x))))))) + ( subtype-inhabited-subtype Q) → + is-block-partition P Q + is-block-is-equivalence-class-equivalence-relation-partition Q H = + apply-universal-property-trunc-Prop H + ( subtype-partition P Q) + ( λ (a , K) → + tr + ( is-block-partition P) + ( inv + ( eq-has-same-elements-inhabited-subtype Q + ( inhabited-subtype-block-partition P (class-partition P a)) + ( λ x → + ( iff-equiv + ( ( left-unit-law-Σ-is-contr + ( is-contr-block-containing-element-partition P a) + ( center-block-containing-element-partition P a)) ∘e + ( inv-associative-Σ + ( block-partition P) + ( λ B → is-in-block-partition P B a) + ( λ B → is-in-block-partition P (pr1 B) x)))) ∘iff + ( K x)))) + ( is-block-class-partition P a)) + + abstract + is-equivalence-class-is-block-partition : + (Q : inhabited-subtype l1 A) → + is-block-partition P Q → + is-equivalence-class + ( equivalence-relation-partition P) + ( subtype-inhabited-subtype Q) + is-equivalence-class-is-block-partition Q H = + apply-universal-property-trunc-Prop + ( is-inhabited-subtype-inhabited-subtype Q) + ( is-equivalence-class-Prop + ( equivalence-relation-partition P) + ( subtype-inhabited-subtype Q)) + ( λ (a , q) → + unit-trunc-Prop + ( pair + ( a) + ( λ x → + iff-equiv + ( ( inv-equiv + ( ( left-unit-law-Σ-is-contr + ( is-contr-block-containing-element-partition P a) + ( pair + ( make-block-partition P Q H) + ( make-is-in-block-partition P Q H a q))) ∘e + ( inv-associative-Σ + ( block-partition P) + ( λ B → is-in-block-partition P B a) + ( λ B → is-in-block-partition P (pr1 B) x)))) ∘e + ( compute-is-in-block-partition P Q H x))))) has-same-elements-partition-equivalence-relation-partition : has-same-elements-subtype @@ -430,14 +417,15 @@ is-retraction-equivalence-relation-partition-equivalence-relation P = #### The map `equivalence-relation-partition` is an equivalence ```agda -is-equiv-equivalence-relation-partition : - {l : Level} {A : UU l} → - is-equiv (equivalence-relation-partition {l} {l} {l} {A}) -is-equiv-equivalence-relation-partition = - is-equiv-is-invertible - partition-equivalence-relation - is-section-equivalence-relation-partition-equivalence-relation - is-retraction-equivalence-relation-partition-equivalence-relation +abstract + is-equiv-equivalence-relation-partition : + {l : Level} {A : UU l} → + is-equiv (equivalence-relation-partition {l} {l} {l} {A}) + is-equiv-equivalence-relation-partition = + is-equiv-is-invertible + partition-equivalence-relation + is-section-equivalence-relation-partition-equivalence-relation + is-retraction-equivalence-relation-partition-equivalence-relation equiv-equivalence-relation-partition : {l : Level} {A : UU l} → partition l l A ≃ equivalence-relation l A diff --git a/src/foundation/partitions.lagda.md b/src/foundation/partitions.lagda.md index 9f37022516..414d0edeca 100644 --- a/src/foundation/partitions.lagda.md +++ b/src/foundation/partitions.lagda.md @@ -286,40 +286,43 @@ will have no more use for the large type of blocks of a partition. is-prop-is-in-block-partition-Large-Type ( map-inv-compute-block-partition B) - compute-is-in-block-partition : - (B : inhabited-subtype l2 A) (H : is-block-partition B) (x : A) → - is-in-inhabited-subtype B x ≃ - is-in-block-partition (make-block-partition B H) x - compute-is-in-block-partition B H x = - equiv-tr - ( λ C → is-in-block-partition-Large-Type C x) - ( inv (is-retraction-map-inv-compute-block-partition (B , H))) - - make-is-in-block-partition : - (B : inhabited-subtype l2 A) (H : is-block-partition B) (x : A) → - is-in-inhabited-subtype B x → - is-in-block-partition (make-block-partition B H) x - make-is-in-block-partition B H x K = - map-equiv (compute-is-in-block-partition B H x) K + abstract + compute-is-in-block-partition : + (B : inhabited-subtype l2 A) (H : is-block-partition B) (x : A) → + is-in-inhabited-subtype B x ≃ + is-in-block-partition (make-block-partition B H) x + compute-is-in-block-partition B H x = + equiv-tr + ( λ C → is-in-block-partition-Large-Type C x) + ( inv (is-retraction-map-inv-compute-block-partition (B , H))) + + abstract + make-is-in-block-partition : + (B : inhabited-subtype l2 A) (H : is-block-partition B) (x : A) → + is-in-inhabited-subtype B x → + is-in-block-partition (make-block-partition B H) x + make-is-in-block-partition B H x K = + map-equiv (compute-is-in-block-partition B H x) K block-containing-element-partition : A → UU (l1 ⊔ l2) block-containing-element-partition a = Σ block-partition (λ B → is-in-block-partition B a) - is-contr-block-containing-element-partition : - (a : A) → is-contr (block-containing-element-partition a) - is-contr-block-containing-element-partition a = - is-contr-equiv' - ( Σ block-partition-Large-Type - ( λ B → is-in-block-partition-Large-Type B a)) - ( equiv-Σ - ( λ B → is-in-block-partition B a) - ( compute-block-partition) - ( λ B → - equiv-tr - ( λ C → is-in-block-partition-Large-Type C a) - ( inv (is-retraction-map-inv-compute-block-partition B)))) - ( is-partition-subtype-partition a) + abstract + is-contr-block-containing-element-partition : + (a : A) → is-contr (block-containing-element-partition a) + is-contr-block-containing-element-partition a = + is-contr-equiv' + ( Σ block-partition-Large-Type + ( λ B → is-in-block-partition-Large-Type B a)) + ( equiv-Σ + ( λ B → is-in-block-partition B a) + ( compute-block-partition) + ( λ B → + equiv-tr + ( λ C → is-in-block-partition-Large-Type C a) + ( inv (is-retraction-map-inv-compute-block-partition B)))) + ( is-partition-subtype-partition a) center-block-containing-element-partition : (a : A) → block-containing-element-partition a @@ -415,22 +418,23 @@ module _ refl-has-same-elements-inhabited-subtype ( inhabited-subtype-block-partition P B) - is-torsorial-has-same-elements-block-partition : - is-torsorial has-same-elements-block-partition - is-torsorial-has-same-elements-block-partition = - is-contr-equiv' - ( Σ ( block-partition P) + abstract + is-torsorial-has-same-elements-block-partition : + is-torsorial has-same-elements-block-partition + is-torsorial-has-same-elements-block-partition = + is-contr-equiv' + ( Σ ( block-partition P) + ( λ C → + inhabited-subtype-block-partition P B ＝ + inhabited-subtype-block-partition P C)) + ( equiv-tot ( λ C → - inhabited-subtype-block-partition P B ＝ - inhabited-subtype-block-partition P C)) - ( equiv-tot - ( λ C → - extensionality-inhabited-subtype - ( inhabited-subtype-block-partition P B) - ( inhabited-subtype-block-partition P C))) - ( fundamental-theorem-id' - ( λ C → ap (inhabited-subtype-block-partition P)) - ( is-emb-inhabited-subtype-block-partition P B)) + extensionality-inhabited-subtype + ( inhabited-subtype-block-partition P B) + ( inhabited-subtype-block-partition P C))) + ( fundamental-theorem-id' + ( λ C → ap (inhabited-subtype-block-partition P)) + ( is-emb-inhabited-subtype-block-partition P B)) has-same-elements-eq-block-partition : (C : block-partition P) → (B ＝ C) → @@ -615,50 +619,51 @@ module _ pr2 (subtype-partition-Set-Indexed-Σ-Decomposition Q) = is-prop-is-block-partition-Set-Indexed-Σ-Decomposition Q - is-partition-subtype-partition-Set-Indexed-Σ-Decomposition : - is-partition (subtype-partition-Set-Indexed-Σ-Decomposition {l2}) - is-partition-subtype-partition-Set-Indexed-Σ-Decomposition a = - is-contr-equiv - ( Σ ( inhabited-subtype l2 A) - ( has-same-elements-inhabited-subtype - ( pair - ( λ x → - Id-Prop - ( indexing-set-Set-Indexed-Σ-Decomposition D) - ( index-Set-Indexed-Σ-Decomposition D x) - ( index-Set-Indexed-Σ-Decomposition D a)) - ( unit-trunc-Prop (pair a refl))))) - ( ( equiv-tot - ( λ Q → - ( ( ( equiv-Π-equiv-family + abstract + is-partition-subtype-partition-Set-Indexed-Σ-Decomposition : + is-partition (subtype-partition-Set-Indexed-Σ-Decomposition {l2}) + is-partition-subtype-partition-Set-Indexed-Σ-Decomposition a = + is-contr-equiv + ( Σ ( inhabited-subtype l2 A) + ( has-same-elements-inhabited-subtype + ( pair ( λ x → - inv-equiv - ( equiv-equiv-iff - ( Id-Prop - ( indexing-set-Set-Indexed-Σ-Decomposition D) - ( index-Set-Indexed-Σ-Decomposition D x) - ( index-Set-Indexed-Σ-Decomposition D a)) - ( subtype-inhabited-subtype Q x)) ∘e - ( equiv-inv-equiv))) ∘e - ( left-unit-law-Σ-is-contr - ( is-torsorial-Id (index-Set-Indexed-Σ-Decomposition D a)) - ( pair - ( index-Set-Indexed-Σ-Decomposition D a) - ( refl)))) ∘e - ( equiv-right-swap-Σ)) ∘e - ( equiv-tot (λ ie → pr2 ie a)))) ∘e - ( associative-Σ - ( inhabited-subtype l2 A) - ( is-block-partition-Set-Indexed-Σ-Decomposition) - ( λ B → is-in-inhabited-subtype (pr1 B) a))) - ( is-torsorial-has-same-elements-inhabited-subtype - ( pair - ( λ x → - Id-Prop - ( indexing-set-Set-Indexed-Σ-Decomposition D) - ( index-Set-Indexed-Σ-Decomposition D x) - ( index-Set-Indexed-Σ-Decomposition D a)) - ( unit-trunc-Prop (pair a refl)))) + Id-Prop + ( indexing-set-Set-Indexed-Σ-Decomposition D) + ( index-Set-Indexed-Σ-Decomposition D x) + ( index-Set-Indexed-Σ-Decomposition D a)) + ( unit-trunc-Prop (pair a refl))))) + ( ( equiv-tot + ( λ Q → + ( ( ( equiv-Π-equiv-family + ( λ x → + inv-equiv + ( equiv-equiv-iff + ( Id-Prop + ( indexing-set-Set-Indexed-Σ-Decomposition D) + ( index-Set-Indexed-Σ-Decomposition D x) + ( index-Set-Indexed-Σ-Decomposition D a)) + ( subtype-inhabited-subtype Q x)) ∘e + ( equiv-inv-equiv))) ∘e + ( left-unit-law-Σ-is-contr + ( is-torsorial-Id (index-Set-Indexed-Σ-Decomposition D a)) + ( pair + ( index-Set-Indexed-Σ-Decomposition D a) + ( refl)))) ∘e + ( equiv-right-swap-Σ)) ∘e + ( equiv-tot (λ ie → pr2 ie a)))) ∘e + ( associative-Σ + ( inhabited-subtype l2 A) + ( is-block-partition-Set-Indexed-Σ-Decomposition) + ( λ B → is-in-inhabited-subtype (pr1 B) a))) + ( is-torsorial-has-same-elements-inhabited-subtype + ( pair + ( λ x → + Id-Prop + ( indexing-set-Set-Indexed-Σ-Decomposition D) + ( index-Set-Indexed-Σ-Decomposition D x) + ( index-Set-Indexed-Σ-Decomposition D a)) + ( unit-trunc-Prop (pair a refl)))) partition-Set-Indexed-Σ-Decomposition : {l1 l2 l3 : Level} {A : UU l1} → diff --git a/src/foundation/type-arithmetic-unit-type.lagda.md b/src/foundation/type-arithmetic-unit-type.lagda.md index 508c3f20b6..7f3e6fc73e 100644 --- a/src/foundation/type-arithmetic-unit-type.lagda.md +++ b/src/foundation/type-arithmetic-unit-type.lagda.md @@ -17,6 +17,8 @@ open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types +open import foundation-core.retractions +open import foundation-core.sections ``` @@ -35,7 +37,7 @@ module _ where map-left-unit-law-Σ : Σ unit A → A star - map-left-unit-law-Σ (pair star a) = a + map-left-unit-law-Σ (_ , a) = a map-inv-left-unit-law-Σ : A star → Σ unit A pr1 (map-inv-left-unit-law-Σ a) = star @@ -43,11 +45,11 @@ module _ is-section-map-inv-left-unit-law-Σ : ( map-left-unit-law-Σ ∘ map-inv-left-unit-law-Σ) ~ id - is-section-map-inv-left-unit-law-Σ a = refl + is-section-map-inv-left-unit-law-Σ = refl-htpy is-retraction-map-inv-left-unit-law-Σ : ( map-inv-left-unit-law-Σ ∘ map-left-unit-law-Σ) ~ id - is-retraction-map-inv-left-unit-law-Σ (pair star a) = refl + is-retraction-map-inv-left-unit-law-Σ = refl-htpy is-equiv-map-left-unit-law-Σ : is-equiv map-left-unit-law-Σ is-equiv-map-left-unit-law-Σ = @@ -83,16 +85,16 @@ module _ map-left-unit-law-product = pr2 map-inv-left-unit-law-product : A → unit × A - map-inv-left-unit-law-product = map-inv-left-unit-law-Σ (λ x → A) + map-inv-left-unit-law-product = map-inv-left-unit-law-Σ (λ _ → A) is-section-map-inv-left-unit-law-product : - ( map-left-unit-law-product ∘ map-inv-left-unit-law-product) ~ id + is-section map-left-unit-law-product map-inv-left-unit-law-product is-section-map-inv-left-unit-law-product = - is-section-map-inv-left-unit-law-Σ (λ x → A) + is-section-map-inv-left-unit-law-Σ (λ _ → A) is-retraction-map-inv-left-unit-law-product : - ( map-inv-left-unit-law-product ∘ map-left-unit-law-product) ~ id - is-retraction-map-inv-left-unit-law-product (pair star a) = refl + is-retraction map-left-unit-law-product map-inv-left-unit-law-product + is-retraction-map-inv-left-unit-law-product = refl-htpy is-equiv-map-left-unit-law-product : is-equiv map-left-unit-law-product is-equiv-map-left-unit-law-product = @@ -129,12 +131,12 @@ module _ pr2 (map-inv-right-unit-law-product a) = star is-section-map-inv-right-unit-law-product : - (map-right-unit-law-product ∘ map-inv-right-unit-law-product) ~ id - is-section-map-inv-right-unit-law-product a = refl + is-section map-right-unit-law-product map-inv-right-unit-law-product + is-section-map-inv-right-unit-law-product = refl-htpy is-retraction-map-inv-right-unit-law-product : - (map-inv-right-unit-law-product ∘ map-right-unit-law-product) ~ id - is-retraction-map-inv-right-unit-law-product (pair a star) = refl + is-retraction map-right-unit-law-product map-inv-right-unit-law-product + is-retraction-map-inv-right-unit-law-product = refl-htpy is-equiv-map-right-unit-law-product : is-equiv map-right-unit-law-product is-equiv-map-right-unit-law-product = @@ -159,15 +161,15 @@ module _ map-left-unit-law-Π f = f star map-inv-left-unit-law-Π : A star → ((t : unit) → A t) - map-inv-left-unit-law-Π a star = a + map-inv-left-unit-law-Π a _ = a is-section-map-inv-left-unit-law-Π : - ( map-left-unit-law-Π ∘ map-inv-left-unit-law-Π) ~ id - is-section-map-inv-left-unit-law-Π a = refl + is-section map-left-unit-law-Π map-inv-left-unit-law-Π + is-section-map-inv-left-unit-law-Π = refl-htpy is-retraction-map-inv-left-unit-law-Π : - ( map-inv-left-unit-law-Π ∘ map-left-unit-law-Π) ~ id - is-retraction-map-inv-left-unit-law-Π f = eq-htpy (λ star → refl) + is-retraction map-left-unit-law-Π map-inv-left-unit-law-Π + is-retraction-map-inv-left-unit-law-Π = refl-htpy is-equiv-map-left-unit-law-Π : is-equiv map-left-unit-law-Π is-equiv-map-left-unit-law-Π = @@ -208,12 +210,12 @@ module _ is-equiv-map-left-unit-law-function-type : is-equiv map-left-unit-law-function-type is-equiv-map-left-unit-law-function-type = - is-equiv-map-left-unit-law-Π λ _ → A + is-equiv-map-left-unit-law-Π (λ _ → A) is-equiv-map-inv-left-unit-law-function-type : is-equiv map-inv-left-unit-law-function-type is-equiv-map-inv-left-unit-law-function-type = - is-equiv-map-inv-left-unit-law-Π λ _ → A + is-equiv-map-inv-left-unit-law-Π (λ _ → A) left-unit-law-function-type : (unit → A) ≃ A left-unit-law-function-type = left-unit-law-Π (λ _ → A) diff --git a/src/orthogonal-factorization-systems/higher-modalities.lagda.md b/src/orthogonal-factorization-systems/higher-modalities.lagda.md index b44ca06b76..268ae3b349 100644 --- a/src/orthogonal-factorization-systems/higher-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/higher-modalities.lagda.md @@ -55,7 +55,7 @@ modalities in their most general form only make sense for ### Closure under identity type formers -We say that the [locally small type](foundation-core.identity-types.md) of a +We say that the [identity types](foundation-core.identity-types.md) of a [locally small type](foundation.locally-small-types.md) are **modal** if their [small equivalent](foundation-core.small-types.md) is modal. We say that a modality is closed under [identity type](foundation-core.identity-types.md) diff --git a/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md b/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md index 8991458d44..a5b4c0921e 100644 --- a/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md +++ b/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md @@ -1,6 +1,8 @@ # The universal cover of the circle ```agda +{-# OPTIONS --lossy-unification #-} + module synthetic-homotopy-theory.universal-cover-circle where ``` diff --git a/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md b/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md index 5497bc58c2..54fb5a7daa 100644 --- a/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md +++ b/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md @@ -1345,20 +1345,20 @@ module _ λ s → np ( ( tr - ( λ y → - Id - ( i) - ( map-equiv - ( transposition - ( standard-2-Element-Decidable-Subtype - ( has-decidable-equality-count eX) - ( np))) - ( y))) - ( inv r1) - ( inv - ( right-computation-standard-transposition - ( has-decidable-equality-count eX) - ( np))) ∙ + ( λ y → + Id + ( i) + ( map-equiv + ( transposition + ( standard-2-Element-Decidable-Subtype + ( has-decidable-equality-count eX) + ( np))) + ( y))) + ( inv r1) + ( inv + ( right-computation-standard-transposition + ( has-decidable-equality-count eX) + ( np))) ∙ ( s ∙ r1)))) ( inl ( tr @@ -2334,13 +2334,13 @@ module _ ( tr ( λ Y' → type-Decidable-Prop - ( ( pr1 Y' ∘ - ( map-inv-equiv - ( transposition - ( standard-2-Element-Decidable-Subtype - ( has-decidable-equality-count eX) - ( np))))) - ( y))) + ( ( pr1 Y' + ( map-inv-equiv + ( transposition + ( standard-2-Element-Decidable-Subtype + ( has-decidable-equality-count eX) + ( np))) + ( y))))) ( P) ( inr ( inv @@ -2353,13 +2353,13 @@ module _ ( tr ( λ Y' → type-Decidable-Prop - ( ( pr1 Y' ∘ + ( pr1 Y' ( map-inv-equiv ( transposition ( standard-2-Element-Decidable-Subtype ( has-decidable-equality-count eX) - ( np))))) - ( j))) + ( np))) + ( j)))) ( P) ( inl ( q ∙ @@ -2463,13 +2463,13 @@ module _ ( tr ( λ Y' → type-Decidable-Prop - ( ( pr1 Y' ∘ + ( pr1 Y' ( map-inv-equiv ( transposition ( standard-2-Element-Decidable-Subtype ( has-decidable-equality-count eX) - ( np))))) - ( y))) + ( np))) + ( y)))) ( P) ( inr ( inv @@ -2482,13 +2482,13 @@ module _ ( tr ( λ Y' → type-Decidable-Prop - ( ( ( pr1 Y') ∘ - ( map-inv-equiv - ( transposition - ( standard-2-Element-Decidable-Subtype - ( has-decidable-equality-count eX) - ( np))))) - ( i))) + ( pr1 Y' + ( map-inv-equiv + ( transposition + ( standard-2-Element-Decidable-Subtype + ( has-decidable-equality-count eX) + ( np))) + ( i)))) ( P) ( inl ( r ∙ @@ -2529,13 +2529,13 @@ module _ ( tr ( λ Y' → type-Decidable-Prop - ( ( ( pr1 Y') ∘ + ( pr1 Y' ( map-inv-equiv ( transposition ( standard-2-Element-Decidable-Subtype ( has-decidable-equality-count eX) - ( np))))) - ( x))) + ( np))) + ( x)))) ( P) ( inl ( inv @@ -2548,13 +2548,13 @@ module _ ( tr ( λ Y' → type-Decidable-Prop - ( ( ( pr1 Y') ∘ - ( map-inv-equiv - ( transposition - ( standard-2-Element-Decidable-Subtype - ( has-decidable-equality-count eX) - ( np))))) - ( j))) + ( pr1 Y' + ( map-inv-equiv + ( transposition + ( standard-2-Element-Decidable-Subtype + ( has-decidable-equality-count eX) + ( np))) + ( j)))) ( P) ( inr ( s ∙ @@ -2597,13 +2597,13 @@ module _ ( tr ( λ Y' → type-Decidable-Prop - ( ( pr1 Y' ∘ + ( pr1 Y' ( map-inv-equiv ( transposition ( standard-2-Element-Decidable-Subtype ( has-decidable-equality-count eX) - ( np))))) - ( x))) + ( np))) + ( x)))) ( P) ( inl ( inv @@ -2616,13 +2616,13 @@ module _ ( tr ( λ Y' → type-Decidable-Prop - ( ( pr1 Y' ∘ + ( pr1 Y' ( map-inv-equiv ( transposition ( standard-2-Element-Decidable-Subtype ( has-decidable-equality-count eX) - ( np))))) - ( i))) + ( np))) + ( i)))) ( P) ( inr ( t ∙ From bfb898ff2d815db3a4913fd31a7f1116b62d44f5 Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 27 Feb 2024 20:01:48 +0100 Subject: [PATCH 5/5] Rational real numbers (#1034) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR introduces the cannonical map from `ℚ` to `ℝ` as well as a characterisation of its image in terms of Dedekind cuts. To do so, I had to introduce a few properties on (strict) inequalities on the rational numbers, integer fractions and integers. - modified: elementary-number-theory/addition-integers.lagda.md - the sum of a nonnegative and a positive integer is positive - new file: elementary-number-theory/cross-mul-diff-integer-fractions.lagda.md - define the cross-multiplication difference of two integer fractions - computing properties (useful to work with comparison of integer fractions) - modified: elementary-number-theory/inequality-integer-fractions.lagda.md - generic properties of the (strict) order on integer fractions (asymmetricity, transitivity, etc.) - helper functions to construct inequal fractions - modified: elementary-number-theory/inequality-integers.lagda.md - fix the definition of `le-ℤ` - generic properties of `le-ℤ` - preservation/reflection properties of `le-ℤ` w.r.t `add-ℤ` - modified: elementary-number-theory/inequality-rational-numbers.lagda.md - generic properties of the (strict) order on rational numbers - compatibility between the orderings on integer fractions and rational numbers - no lower/upper bounds, decidability, trichotomy principle - density and of strict inequality on rational numbers - modified: elementary-number-theory/integers.lagda.md - decide positivity of integers - new file: elementary-number-theory/mediant-integer-fractions.lagda.md - define the mediant of two integer fractions - the mediant preserves cross-multiplication difference - modified: elementary-number-theory/multiplication-integers.lagda.md - multiplication by a positive integer preserves strict ordering - modified: elementary-number-theory/rational-numbers.lagda.md - accessor functions for rational numbers - define the mediant of two rational numbers - modified: real-numbers/dedekind-real-numbers.lagda.md - contructor and accessor functions for real numbers - properties of Dedekind cuts - real numbers are determined by their lower/upper cuts - new file: real-numbers/rational-real-numbers.lagda.md - define the Dedekind cut given by a rational number - define the subtype of rational real numbers - `ℚ` embeds in `ℝ` as the subtype of rational real numbers --- src/elementary-number-theory.lagda.md | 2 + .../addition-integers.lagda.md | 14 + ...tion-difference-integer-fractions.lagda.md | 219 ++++++++++ .../inequality-integer-fractions.lagda.md | 221 ++++++++++ .../inequality-integers.lagda.md | 79 +++- .../inequality-rational-numbers.lagda.md | 240 +++++++++++ .../integers.lagda.md | 56 +++ .../mediant-integer-fractions.lagda.md | 86 ++++ .../multiplication-integers.lagda.md | 14 + .../rational-numbers.lagda.md | 36 +- src/real-numbers.lagda.md | 1 + .../dedekind-real-numbers.lagda.md | 391 ++++++++++++++++++ .../rational-real-numbers.lagda.md | 256 ++++++++++++ 13 files changed, 1610 insertions(+), 5 deletions(-) create mode 100644 src/elementary-number-theory/cross-multiplication-difference-integer-fractions.lagda.md create mode 100644 src/elementary-number-theory/mediant-integer-fractions.lagda.md create mode 100644 src/real-numbers/rational-real-numbers.lagda.md diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index 8dfdb41987..8548212757 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -27,6 +27,7 @@ open import elementary-number-theory.collatz-conjecture public open import elementary-number-theory.commutative-semiring-of-natural-numbers public open import elementary-number-theory.congruence-integers public open import elementary-number-theory.congruence-natural-numbers public +open import elementary-number-theory.cross-multiplication-difference-integer-fractions public open import elementary-number-theory.cubes-natural-numbers public open import elementary-number-theory.decidable-dependent-function-types public open import elementary-number-theory.decidable-total-order-natural-numbers public @@ -73,6 +74,7 @@ open import elementary-number-theory.legendre-symbol public open import elementary-number-theory.lower-bounds-natural-numbers public open import elementary-number-theory.maximum-natural-numbers public open import elementary-number-theory.maximum-standard-finite-types public +open import elementary-number-theory.mediant-integer-fractions public open import elementary-number-theory.mersenne-primes public open import elementary-number-theory.minimum-natural-numbers public open import elementary-number-theory.minimum-standard-finite-types public diff --git a/src/elementary-number-theory/addition-integers.lagda.md b/src/elementary-number-theory/addition-integers.lagda.md index f8fd31eb59..8b93313e77 100644 --- a/src/elementary-number-theory/addition-integers.lagda.md +++ b/src/elementary-number-theory/addition-integers.lagda.md @@ -536,6 +536,20 @@ is-positive-add-ℤ {inr (inr (succ-ℕ x))} {inr (inr y)} H K = is-positive-succ-ℤ ( is-nonnegative-is-positive-ℤ ( is-positive-add-ℤ {inr (inr x)} {inr (inr y)} star star)) + +is-positive-add-nonnegative-positive-ℤ : + {x y : ℤ} → is-nonnegative-ℤ x → is-positive-ℤ y → is-positive-ℤ (x +ℤ y) +is-positive-add-nonnegative-positive-ℤ {inr (inl x)} {y} H H' = + is-positive-eq-ℤ refl H' +is-positive-add-nonnegative-positive-ℤ {inr (inr x)} {y} H H' = + is-positive-add-ℤ {inr (inr x)} {y} H H' + +is-positive-add-positive-nonnegative-ℤ : + {x y : ℤ} → is-positive-ℤ x → is-nonnegative-ℤ y → is-positive-ℤ (x +ℤ y) +is-positive-add-positive-nonnegative-ℤ {x} {y} H H' = + is-positive-eq-ℤ + ( commutative-add-ℤ y x) + ( is-positive-add-nonnegative-positive-ℤ H' H) ``` ### The inclusion of ℕ into ℤ preserves addition diff --git a/src/elementary-number-theory/cross-multiplication-difference-integer-fractions.lagda.md b/src/elementary-number-theory/cross-multiplication-difference-integer-fractions.lagda.md new file mode 100644 index 0000000000..8fb4af6bbc --- /dev/null +++ b/src/elementary-number-theory/cross-multiplication-difference-integer-fractions.lagda.md @@ -0,0 +1,219 @@ +# The cross-multiplication difference of two integer fractions + +```agda +module elementary-number-theory.cross-multiplication-difference-integer-fractions where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-integers +open import elementary-number-theory.difference-integers +open import elementary-number-theory.integer-fractions +open import elementary-number-theory.integers +open import elementary-number-theory.multiplication-integers + +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.negation +open import foundation.propositions +``` + +
+ +## Idea + +The +{{#concept "cross-multiplication difference" Agda=cross-mul-diff-fraction-ℤ}} of +two [integer fractions](elementary-number-theory.integer-fractions.md) `a/b` and +`c/d` is the [difference](elementary-number-theory.difference-integers.md) of +the [products](elementary-number-theory.multiplication-integers.md) of the +numerator of each fraction with the denominator of the other: `c * b - a * d`. + +## Definitions + +### The cross-multiplication difference of two fractions + +```agda +cross-mul-diff-fraction-ℤ : fraction-ℤ → fraction-ℤ → ℤ +cross-mul-diff-fraction-ℤ x y = + diff-ℤ + ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x) + ( numerator-fraction-ℤ x *ℤ denominator-fraction-ℤ y) +``` + +## Properties + +### Swapping the fractions changes the sign of the cross-multiplication difference + +```agda +skew-commutative-cross-mul-diff-fraction-ℤ : + (x y : fraction-ℤ) → + Id + ( neg-ℤ (cross-mul-diff-fraction-ℤ x y)) + ( cross-mul-diff-fraction-ℤ y x) +skew-commutative-cross-mul-diff-fraction-ℤ x y = + distributive-neg-diff-ℤ + ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x) + ( numerator-fraction-ℤ x *ℤ denominator-fraction-ℤ y) +``` + +### Two fractions are similar when their cross-multiplication difference is zero + +```agda +module _ + (x y : fraction-ℤ) + where + + is-zero-cross-mul-diff-sim-fraction-ℤ : + sim-fraction-ℤ x y → + is-zero-ℤ (cross-mul-diff-fraction-ℤ x y) + is-zero-cross-mul-diff-sim-fraction-ℤ H = + is-zero-diff-ℤ (inv H) + + sim-is-zero-coss-mul-diff-fraction-ℤ : + is-zero-ℤ (cross-mul-diff-fraction-ℤ x y) → + sim-fraction-ℤ x y + sim-is-zero-coss-mul-diff-fraction-ℤ H = inv (eq-diff-ℤ H) +``` + +## The transitive-additive property for the cross-multiplication difference + +Given three fractions `a/b`, `x/y` and `m/n`, the pairwise cross-multiplication +differences satisfy a transitive-additive property: + +```text + y * (m * b - a * n) = b * (m * y - x * n) + n * (x * b - a * y) +``` + +```agda +lemma-add-cross-mul-diff-fraction-ℤ : + (p q r : fraction-ℤ) → + Id + ( add-ℤ + ( denominator-fraction-ℤ p *ℤ cross-mul-diff-fraction-ℤ q r) + ( denominator-fraction-ℤ r *ℤ cross-mul-diff-fraction-ℤ p q)) + ( denominator-fraction-ℤ q *ℤ cross-mul-diff-fraction-ℤ p r) +lemma-add-cross-mul-diff-fraction-ℤ + (np , dp , hp) + (nq , dq , hq) + (nr , dr , hr) = + equational-reasoning + add-ℤ + (dp *ℤ (nr *ℤ dq -ℤ nq *ℤ dr)) + (dr *ℤ (nq *ℤ dp -ℤ np *ℤ dq)) + ＝ add-ℤ + (dp *ℤ (nr *ℤ dq) -ℤ dp *ℤ (nq *ℤ dr)) + (dr *ℤ (nq *ℤ dp) -ℤ dr *ℤ (np *ℤ dq)) + by + ap-add-ℤ + ( inv (linear-diff-left-mul-ℤ dp (nr *ℤ dq) (nq *ℤ dr))) + ( inv (linear-diff-left-mul-ℤ dr (nq *ℤ dp) (np *ℤ dq))) + ＝ diff-ℤ + (dp *ℤ (nr *ℤ dq) +ℤ dr *ℤ (nq *ℤ dp)) + (dp *ℤ (nq *ℤ dr) +ℤ dr *ℤ (np *ℤ dq)) + by + interchange-law-add-diff-ℤ + ( mul-ℤ dp ( mul-ℤ nr dq)) + ( mul-ℤ dp ( mul-ℤ nq dr)) + ( mul-ℤ dr ( mul-ℤ nq dp)) + ( mul-ℤ dr ( mul-ℤ np dq)) + ＝ diff-ℤ + (dq *ℤ (nr *ℤ dp) +ℤ dr *ℤ (nq *ℤ dp)) + (dr *ℤ (nq *ℤ dp) +ℤ dq *ℤ (np *ℤ dr)) + by + ap-diff-ℤ + ( ap-add-ℤ + ( lemma-interchange-mul-ℤ dp nr dq) + ( refl)) + ( ap-add-ℤ + ( lemma-interchange-mul-ℤ dp nq dr) + ( lemma-interchange-mul-ℤ dr np dq)) + ＝ diff-ℤ + (dq *ℤ (nr *ℤ dp) +ℤ dr *ℤ (nq *ℤ dp)) + ((dq *ℤ (np *ℤ dr)) +ℤ (dr *ℤ (nq *ℤ dp))) + by + ap + ( diff-ℤ (dq *ℤ (nr *ℤ dp) +ℤ dr *ℤ (nq *ℤ dp))) + ( commutative-add-ℤ (dr *ℤ (nq *ℤ dp)) (dq *ℤ (np *ℤ dr))) + ＝ (dq *ℤ (nr *ℤ dp)) -ℤ (dq *ℤ (np *ℤ dr)) + by + right-translation-diff-ℤ + (dq *ℤ (nr *ℤ dp)) + (dq *ℤ (np *ℤ dr)) + (dr *ℤ (nq *ℤ dp)) + ＝ dq *ℤ (nr *ℤ dp -ℤ np *ℤ dr) + by linear-diff-left-mul-ℤ dq (nr *ℤ dp) (np *ℤ dr) + where + lemma-interchange-mul-ℤ : (a b c : ℤ) → (a *ℤ (b *ℤ c)) ＝ (c *ℤ (b *ℤ a)) + lemma-interchange-mul-ℤ a b c = + inv (associative-mul-ℤ a b c) ∙ + ap (mul-ℤ' c) (commutative-mul-ℤ a b) ∙ + commutative-mul-ℤ (b *ℤ a) c + +lemma-left-sim-cross-mul-diff-fraction-ℤ : + (a a' b : fraction-ℤ) → + sim-fraction-ℤ a a' → + Id + ( denominator-fraction-ℤ a *ℤ cross-mul-diff-fraction-ℤ a' b) + ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b) +lemma-left-sim-cross-mul-diff-fraction-ℤ a a' b H = + equational-reasoning + ( denominator-fraction-ℤ a *ℤ cross-mul-diff-fraction-ℤ a' b) + ＝ ( add-ℤ + ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b) + ( denominator-fraction-ℤ b *ℤ cross-mul-diff-fraction-ℤ a' a)) + by inv (lemma-add-cross-mul-diff-fraction-ℤ a' a b) + ＝ ( add-ℤ + ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b) + ( zero-ℤ)) + by + ap + ( add-ℤ + ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b)) + ( ( ap + ( mul-ℤ (denominator-fraction-ℤ b)) + ( is-zero-cross-mul-diff-sim-fraction-ℤ a' a H')) ∙ + ( right-zero-law-mul-ℤ (denominator-fraction-ℤ b))) + ＝ denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b + by + right-unit-law-add-ℤ + ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b) + where + H' : sim-fraction-ℤ a' a + H' = symmetric-sim-fraction-ℤ a a' H + +lemma-right-sim-cross-mul-diff-fraction-ℤ : + (a b b' : fraction-ℤ) → + sim-fraction-ℤ b b' → + Id + ( denominator-fraction-ℤ b *ℤ cross-mul-diff-fraction-ℤ a b') + ( denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b) +lemma-right-sim-cross-mul-diff-fraction-ℤ a b b' H = + equational-reasoning + ( denominator-fraction-ℤ b *ℤ cross-mul-diff-fraction-ℤ a b') + ＝ ( add-ℤ + ( denominator-fraction-ℤ a *ℤ cross-mul-diff-fraction-ℤ b b') + ( denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b)) + by inv (lemma-add-cross-mul-diff-fraction-ℤ a b b') + ＝ ( add-ℤ + ( zero-ℤ) + ( denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b)) + by + ap + ( add-ℤ' (denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b)) + ( ( ap + ( mul-ℤ (denominator-fraction-ℤ a)) + ( is-zero-cross-mul-diff-sim-fraction-ℤ b b' H)) ∙ + ( right-zero-law-mul-ℤ (denominator-fraction-ℤ a))) + ＝ denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b + by + left-unit-law-add-ℤ + ( denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b) +``` + +## External links + +- [Cross-multiplication](https://en.wikipedia.org/wiki/Cross-multiplication) at + Wikipedia diff --git a/src/elementary-number-theory/inequality-integer-fractions.lagda.md b/src/elementary-number-theory/inequality-integer-fractions.lagda.md index 9515686192..72408db7b4 100644 --- a/src/elementary-number-theory/inequality-integer-fractions.lagda.md +++ b/src/elementary-number-theory/inequality-integer-fractions.lagda.md @@ -7,12 +7,24 @@ module elementary-number-theory.inequality-integer-fractions where
Imports ```agda +open import elementary-number-theory.addition-integers +open import elementary-number-theory.cross-multiplication-difference-integer-fractions +open import elementary-number-theory.difference-integers open import elementary-number-theory.inequality-integers open import elementary-number-theory.integer-fractions +open import elementary-number-theory.integers +open import elementary-number-theory.mediant-integer-fractions open import elementary-number-theory.multiplication-integers +open import foundation.action-on-identifications-functions +open import foundation.cartesian-product-types +open import foundation.coproduct-types open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.identity-types +open import foundation.negation open import foundation.propositions +open import foundation.transport-along-identifications open import foundation.universe-levels ``` @@ -52,3 +64,212 @@ le-fraction-ℤ x y = type-Prop (le-fraction-ℤ-Prop x y) is-prop-le-fraction-ℤ : (x y : fraction-ℤ) → is-prop (le-fraction-ℤ x y) is-prop-le-fraction-ℤ x y = is-prop-type-Prop (le-fraction-ℤ-Prop x y) ``` + +## Properties + +### Inequality on integer fractions is antisymmetric with respect to the similarity relation + +```agda +module _ + (x y : fraction-ℤ) + where + + is-sim-antisymmetric-leq-fraction-ℤ : + leq-fraction-ℤ x y → + leq-fraction-ℤ y x → + sim-fraction-ℤ x y + is-sim-antisymmetric-leq-fraction-ℤ H H' = + sim-is-zero-coss-mul-diff-fraction-ℤ x y + ( is-zero-is-nonnegative-ℤ + ( H) + ( is-nonnegative-eq-ℤ + ( inv ( skew-commutative-cross-mul-diff-fraction-ℤ x y)) + ( H'))) +``` + +### Strict inequality on integer fractions is asymmetric + +```agda +module _ + (x y : fraction-ℤ) + where + + asymmetric-le-fraction-ℤ : + le-fraction-ℤ x y → ¬ (le-fraction-ℤ y x) + asymmetric-le-fraction-ℤ = + asymmetric-le-ℤ + ( mul-ℤ + ( numerator-fraction-ℤ x) + ( denominator-fraction-ℤ y)) + ( mul-ℤ + ( numerator-fraction-ℤ y) + ( denominator-fraction-ℤ x)) +``` + +### Inequality on integer fractions is transitive + +```agda +transitive-leq-fraction-ℤ : + (p q r : fraction-ℤ) → + leq-fraction-ℤ p q → + leq-fraction-ℤ q r → + leq-fraction-ℤ p r +transitive-leq-fraction-ℤ p q r H H' = + is-nonnegative-right-factor-mul-ℤ + ( is-nonnegative-eq-ℤ + ( lemma-add-cross-mul-diff-fraction-ℤ p q r) + (is-nonnegative-add-ℤ + ( denominator-fraction-ℤ p *ℤ cross-mul-diff-fraction-ℤ q r) + ( denominator-fraction-ℤ r *ℤ cross-mul-diff-fraction-ℤ p q) + ( is-nonnegative-mul-ℤ + ( is-nonnegative-is-positive-ℤ + ( is-positive-denominator-fraction-ℤ p)) + ( H')) + ( is-nonnegative-mul-ℤ + ( is-nonnegative-is-positive-ℤ + ( is-positive-denominator-fraction-ℤ r)) + ( H)))) + ( is-positive-denominator-fraction-ℤ q) +``` + +### Strict inequality on integer fractions is transitive + +```agda +transitive-le-fraction-ℤ : + (p q r : fraction-ℤ) → + le-fraction-ℤ p q → + le-fraction-ℤ q r → + le-fraction-ℤ p r +transitive-le-fraction-ℤ p q r H H' = + is-positive-right-factor-mul-ℤ + ( is-positive-eq-ℤ + ( lemma-add-cross-mul-diff-fraction-ℤ p q r) + ( is-positive-add-ℤ + ( is-positive-mul-ℤ + ( is-positive-denominator-fraction-ℤ p) + ( H')) + ( is-positive-mul-ℤ + ( is-positive-denominator-fraction-ℤ r) + ( H)))) + ( is-positive-denominator-fraction-ℤ q) +``` + +### Chaining rules for inequality and strict inequality on integer fractions + +```agda +module _ + (p q r : fraction-ℤ) + where + + concatenate-le-leq-fraction-ℤ : + le-fraction-ℤ p q → + leq-fraction-ℤ q r → + le-fraction-ℤ p r + concatenate-le-leq-fraction-ℤ H H' = + is-positive-right-factor-mul-ℤ + ( is-positive-eq-ℤ + ( lemma-add-cross-mul-diff-fraction-ℤ p q r) + ( is-positive-add-nonnegative-positive-ℤ + ( is-nonnegative-mul-ℤ + ( is-nonnegative-is-positive-ℤ + ( is-positive-denominator-fraction-ℤ p)) + ( H')) + ( is-positive-mul-ℤ + ( is-positive-denominator-fraction-ℤ r) + ( H)))) + ( is-positive-denominator-fraction-ℤ q) + + concatenate-leq-le-fraction-ℤ : + leq-fraction-ℤ p q → + le-fraction-ℤ q r → + le-fraction-ℤ p r + concatenate-leq-le-fraction-ℤ H H' = + is-positive-right-factor-mul-ℤ + ( is-positive-eq-ℤ + ( lemma-add-cross-mul-diff-fraction-ℤ p q r) + ( is-positive-add-positive-nonnegative-ℤ + ( is-positive-mul-ℤ + ( is-positive-denominator-fraction-ℤ p) + ( H')) + ( is-nonnegative-mul-ℤ + ( is-nonnegative-is-positive-ℤ + ( is-positive-denominator-fraction-ℤ r)) + ( H)))) + ( is-positive-denominator-fraction-ℤ q) +``` + +### Chaining rules for similarity and strict inequality on integer fractions + +```agda +module _ + (p q r : fraction-ℤ) + where + + concatenate-sim-le-fraction-ℤ : + sim-fraction-ℤ p q → + le-fraction-ℤ q r → + le-fraction-ℤ p r + concatenate-sim-le-fraction-ℤ H H' = + is-positive-right-factor-mul-ℤ + ( is-positive-eq-ℤ + ( lemma-left-sim-cross-mul-diff-fraction-ℤ p q r H) + ( is-positive-mul-ℤ + ( is-positive-denominator-fraction-ℤ p) H')) + ( is-positive-denominator-fraction-ℤ q) + + concatenate-le-sim-fraction-ℤ : + le-fraction-ℤ p q → + sim-fraction-ℤ q r → + le-fraction-ℤ p r + concatenate-le-sim-fraction-ℤ H H' = + is-positive-right-factor-mul-ℤ + ( is-positive-eq-ℤ + ( inv ( lemma-right-sim-cross-mul-diff-fraction-ℤ p q r H')) + ( is-positive-mul-ℤ (is-positive-denominator-fraction-ℤ r) H)) + ( is-positive-denominator-fraction-ℤ q) +``` + +### Fractions with equal denominator compare the same as their numerators + +```agda +module _ + (x y : fraction-ℤ) (H : denominator-fraction-ℤ x ＝ denominator-fraction-ℤ y) + where + + le-fraction-le-numerator-fraction-ℤ : + le-ℤ (numerator-fraction-ℤ x) (numerator-fraction-ℤ y) → + le-fraction-ℤ x y + le-fraction-le-numerator-fraction-ℤ H' = + tr + ( λ (k : ℤ) → + le-ℤ + ( numerator-fraction-ℤ x *ℤ k) + ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x)) + ( H) + ( preserves-strict-order-mul-positive-ℤ' + { numerator-fraction-ℤ x} + { numerator-fraction-ℤ y} + ( denominator-fraction-ℤ x) + ( is-positive-denominator-fraction-ℤ x) + ( H')) +``` + +### The mediant of two fractions is between them + +```agda +module _ + (x y : fraction-ℤ) + where + + le-left-mediant-fraction-ℤ : + le-fraction-ℤ x y → + le-fraction-ℤ x (mediant-fraction-ℤ x y) + le-left-mediant-fraction-ℤ = + is-positive-eq-ℤ (cross-mul-diff-left-mediant-fraction-ℤ x y) + + le-right-mediant-fraction-ℤ : + le-fraction-ℤ x y → + le-fraction-ℤ (mediant-fraction-ℤ x y) y + le-right-mediant-fraction-ℤ = + is-positive-eq-ℤ (cross-mul-diff-right-mediant-fraction-ℤ x y) +``` diff --git a/src/elementary-number-theory/inequality-integers.lagda.md b/src/elementary-number-theory/inequality-integers.lagda.md index 84668302c9..3eb990d983 100644 --- a/src/elementary-number-theory/inequality-integers.lagda.md +++ b/src/elementary-number-theory/inequality-integers.lagda.md @@ -18,6 +18,8 @@ open import foundation.coproduct-types open import foundation.function-types open import foundation.functoriality-coproduct-types open import foundation.identity-types +open import foundation.negated-equality +open import foundation.negation open import foundation.propositions open import foundation.transport-along-identifications open import foundation.unit-type @@ -100,7 +102,7 @@ concatenate-eq-leq-ℤ y refl H = H ```agda le-ℤ-Prop : ℤ → ℤ → Prop lzero -le-ℤ-Prop x y = is-positive-ℤ-Prop (x -ℤ y) +le-ℤ-Prop x y = is-positive-ℤ-Prop (y -ℤ x) le-ℤ : ℤ → ℤ → UU lzero le-ℤ x y = type-Prop (le-ℤ-Prop x y) @@ -109,6 +111,47 @@ is-prop-le-ℤ : (x y : ℤ) → is-prop (le-ℤ x y) is-prop-le-ℤ x y = is-prop-type-Prop (le-ℤ-Prop x y) ``` +## Properties + +```agda +transitive-le-ℤ : (k l m : ℤ) → le-ℤ k l → le-ℤ l m → le-ℤ k m +transitive-le-ℤ k l m p q = + tr is-positive-ℤ + ( triangle-diff-ℤ m l k) + ( is-positive-add-ℤ q p) + +asymmetric-le-ℤ : (x y : ℤ) → le-ℤ x y → ¬ (le-ℤ y x) +asymmetric-le-ℤ x y p q = + not-is-nonpositive-is-positive-ℤ + ( y -ℤ x) + ( p) + ( is-nonnegative-is-positive-ℤ + ( is-positive-eq-ℤ + ( inv ( distributive-neg-diff-ℤ y x)) + ( q))) + +connected-le-ℤ : (x y : ℤ) → x ≠ y → le-ℤ x y + le-ℤ y x +connected-le-ℤ x y H = + map-coproduct + ( id) + ( is-positive-eq-ℤ ( distributive-neg-diff-ℤ y x)) + ( decide-is-positive-is-nonzero-ℤ (y -ℤ x) (H ∘ inv ∘ eq-diff-ℤ)) + +le-pred-ℤ : (x : ℤ) → le-ℤ (pred-ℤ x) x +le-pred-ℤ x = + is-positive-eq-ℤ + ( inv + ( right-predecessor-law-diff-ℤ x x ∙ ap succ-ℤ (is-zero-diff-ℤ' x))) + ( is-positive-one-ℤ) + +le-succ-ℤ : (x : ℤ) → le-ℤ x (succ-ℤ x) +le-succ-ℤ x = + is-positive-eq-ℤ + ( inv + ( left-successor-law-diff-ℤ x x ∙ ap succ-ℤ (is-zero-diff-ℤ' x))) + ( is-positive-one-ℤ) +``` + ### ℤ is an ordered ring ```agda @@ -143,6 +186,40 @@ reflects-order-add-ℤ {x} {y} {z} = is-nonnegative-eq-ℤ (left-translation-diff-ℤ y x z) ``` +### Addition on the integers preserves and reflects the strict ordering + +```agda +preserves-strict-order-add-ℤ' : + {x y : ℤ} (z : ℤ) → le-ℤ x y → le-ℤ (x +ℤ z) (y +ℤ z) +preserves-strict-order-add-ℤ' {x} {y} z = + is-positive-eq-ℤ (inv (right-translation-diff-ℤ y x z)) + +preserves-strict-order-add-ℤ : + {x y : ℤ} (z : ℤ) → le-ℤ x y → le-ℤ (z +ℤ x) (z +ℤ y) +preserves-strict-order-add-ℤ {x} {y} z = + is-positive-eq-ℤ (inv (left-translation-diff-ℤ y x z)) + +preserves-le-add-ℤ : + {a b c d : ℤ} → le-ℤ a b → le-ℤ c d → le-ℤ (a +ℤ c) (b +ℤ d) +preserves-le-add-ℤ {a} {b} {c} {d} H K = + transitive-le-ℤ + ( a +ℤ c) + ( b +ℤ c) + ( b +ℤ d) + ( preserves-strict-order-add-ℤ' {a} {b} c H) + ( preserves-strict-order-add-ℤ b K) + +reflects-strict-order-add-ℤ' : + {x y z : ℤ} → le-ℤ (x +ℤ z) (y +ℤ z) → le-ℤ x y +reflects-strict-order-add-ℤ' {x} {y} {z} = + is-positive-eq-ℤ (right-translation-diff-ℤ y x z) + +reflects-strict-order-add-ℤ : + {x y z : ℤ} → le-ℤ (z +ℤ x) (z +ℤ y) → le-ℤ x y +reflects-strict-order-add-ℤ {x} {y} {z} = + is-positive-eq-ℤ (left-translation-diff-ℤ y x z) +``` + ### Inclusion of ℕ into ℤ preserves order ```agda diff --git a/src/elementary-number-theory/inequality-rational-numbers.lagda.md b/src/elementary-number-theory/inequality-rational-numbers.lagda.md index aa52e54c68..12c55dad2c 100644 --- a/src/elementary-number-theory/inequality-rational-numbers.lagda.md +++ b/src/elementary-number-theory/inequality-rational-numbers.lagda.md @@ -7,10 +7,27 @@ module elementary-number-theory.inequality-rational-numbers where
Imports ```agda +open import elementary-number-theory.cross-multiplication-difference-integer-fractions open import elementary-number-theory.inequality-integer-fractions +open import elementary-number-theory.inequality-integers +open import elementary-number-theory.integer-fractions +open import elementary-number-theory.integers +open import elementary-number-theory.mediant-integer-fractions +open import elementary-number-theory.multiplication-integers open import elementary-number-theory.rational-numbers +open import elementary-number-theory.reduced-integer-fractions +open import foundation.binary-relations +open import foundation.cartesian-product-types +open import foundation.coproduct-types open import foundation.dependent-pair-types +open import foundation.disjunction +open import foundation.existential-quantification +open import foundation.function-types +open import foundation.functoriality-coproduct-types +open import foundation.identity-types +open import foundation.negation +open import foundation.propositional-truncations open import foundation.propositions open import foundation.universe-levels ``` @@ -53,3 +70,226 @@ le-ℚ x y = type-Prop (le-ℚ-Prop x y) is-prop-le-ℚ : (x y : ℚ) → is-prop (le-ℚ x y) is-prop-le-ℚ x y = is-prop-type-Prop (le-ℚ-Prop x y) ``` + +## Properties + +### Inequality on rational numbers is reflexive + +```agda +refl-leq-ℚ : (x : ℚ) → leq-ℚ x x +refl-leq-ℚ x = + refl-leq-ℤ (numerator-ℚ x *ℤ denominator-ℚ x) +``` + +### Inequality on rational numbers is antisymmetric + +```agda +antisymmetric-leq-ℚ : (x y : ℚ) → leq-ℚ x y → leq-ℚ y x → x ＝ y +antisymmetric-leq-ℚ x y H H' = + ( inv (in-fraction-fraction-ℚ x)) ∙ + ( eq-ℚ-sim-fractions-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + ( is-sim-antisymmetric-leq-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + ( H) + ( H'))) ∙ + ( in-fraction-fraction-ℚ y) +``` + +### Strict inequality on rationals is asymmetric + +```agda +asymmetric-le-ℚ : (x y : ℚ) → le-ℚ x y → ¬ (le-ℚ y x) +asymmetric-le-ℚ x y = + asymmetric-le-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + +irreflexive-le-ℚ : (x : ℚ) → ¬ (le-ℚ x x) +irreflexive-le-ℚ = + is-irreflexive-is-asymmetric le-ℚ asymmetric-le-ℚ +``` + +### Transitivity properties + +```agda +module _ + (x y z : ℚ) + where + + transitive-leq-ℚ : leq-ℚ x y → leq-ℚ y z → leq-ℚ x z + transitive-leq-ℚ = + transitive-leq-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + ( fraction-ℚ z) + + transitive-le-ℚ : le-ℚ x y → le-ℚ y z → le-ℚ x z + transitive-le-ℚ = + transitive-le-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + ( fraction-ℚ z) + + concatenate-le-leq-ℚ : le-ℚ x y → leq-ℚ y z → le-ℚ x z + concatenate-le-leq-ℚ = + concatenate-le-leq-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + ( fraction-ℚ z) + + concatenate-leq-le-ℚ : leq-ℚ x y → le-ℚ y z → le-ℚ x z + concatenate-leq-le-ℚ = + concatenate-leq-le-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + ( fraction-ℚ z) +``` + +### Strict inequality on the rational numbers reflects strict inequality on the underlying fractions + +```agda +module _ + (x : ℚ) (p : fraction-ℤ) + where + + right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ : + le-fraction-ℤ (fraction-ℚ x) p → + le-ℚ x (in-fraction-ℤ p) + right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ H = + concatenate-le-sim-fraction-ℤ + ( fraction-ℚ x) + ( p) + ( fraction-ℚ ( in-fraction-ℤ p)) + ( H) + ( sim-reduced-fraction-ℤ p) + + left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ : + le-fraction-ℤ p (fraction-ℚ x) → + le-ℚ (in-fraction-ℤ p) x + left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ = + concatenate-sim-le-fraction-ℤ + ( fraction-ℚ ( in-fraction-ℤ p)) + ( p) + ( fraction-ℚ x) + ( symmetric-sim-fraction-ℤ + ( p) + ( fraction-ℚ ( in-fraction-ℤ p)) + ( sim-reduced-fraction-ℤ p)) +``` + +### The rational numbers have no lower or upper bound + +```agda +module _ + (x : ℚ) + where + + left-∃-le-ℚ : ∃ ℚ (λ q → le-ℚ q x) + left-∃-le-ℚ = intro-∃ + ( in-fraction-ℤ frac) + ( left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x frac + ( le-fraction-le-numerator-fraction-ℤ + ( frac) + ( fraction-ℚ x) + ( refl) + ( le-pred-ℤ (numerator-ℚ x)))) + where + frac : fraction-ℤ + frac = pred-ℤ (numerator-ℚ x) , positive-denominator-ℚ x + + right-∃-le-ℚ : ∃ ℚ (λ r → le-ℚ x r) + right-∃-le-ℚ = intro-∃ + ( in-fraction-ℤ frac) + ( right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x frac + ( le-fraction-le-numerator-fraction-ℤ + ( fraction-ℚ x) + ( frac) + ( refl) + ( le-succ-ℤ (numerator-ℚ x)))) + where + frac : fraction-ℤ + frac = succ-ℤ (numerator-ℚ x) , positive-denominator-ℚ x +``` + +### Decidability of strict inequality on the rationals + +```agda +decide-le-leq-ℚ : (x y : ℚ) → le-ℚ x y + leq-ℚ y x +decide-le-leq-ℚ x y = + map-coproduct + ( id) + ( is-nonnegative-eq-ℤ + ( skew-commutative-cross-mul-diff-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y))) + ( decide-is-positive-ℤ + { cross-mul-diff-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y)}) +``` + +It remains to fully formalize that strict inequality is decidable. + +### Trichotomy on the rationals + +```agda +trichotomy-le-ℚ : + {l : Level} {A : UU l} (x y : ℚ) → + ( le-ℚ x y → A) → + ( Id x y → A) → + ( le-ℚ y x → A) → + A +trichotomy-le-ℚ x y left eq right with decide-le-leq-ℚ x y | decide-le-leq-ℚ y x +... | inl I | _ = left I +... | inr I | inl I' = right I' +... | inr I | inr I' = eq (antisymmetric-leq-ℚ x y I' I) +``` + +### The mediant of two rationals is between them + +```agda +module _ + (x y : ℚ) (H : le-ℚ x y) + where + + le-left-mediant-ℚ : le-ℚ x (mediant-ℚ x y) + le-left-mediant-ℚ = + right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x + ( mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)) + ( le-left-mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) H) + + le-right-mediant-ℚ : le-ℚ (mediant-ℚ x y) y + le-right-mediant-ℚ = + left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ y + ( mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)) + ( le-right-mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) H) +``` + +### Strict inequality on the rationals is dense + +```agda +module _ + (x y : ℚ) (H : le-ℚ x y) + where + + dense-le-ℚ : ∃ ℚ (λ r → le-ℚ x r × le-ℚ r y) + dense-le-ℚ = + intro-∃ + ( mediant-ℚ x y) + ( le-left-mediant-ℚ x y H , le-right-mediant-ℚ x y H) +``` + +### The strict order on the rationals is located + +```agda +located-le-ℚ : (x y z : ℚ) → le-ℚ y z → (le-ℚ-Prop y x) ∨ (le-ℚ-Prop x z) +located-le-ℚ x y z H = + unit-trunc-Prop + ( map-coproduct + ( id) + ( λ p → concatenate-leq-le-ℚ x y z p H) + ( decide-le-leq-ℚ y x)) +``` diff --git a/src/elementary-number-theory/integers.lagda.md b/src/elementary-number-theory/integers.lagda.md index 853f8a3981..9c8b2a6150 100644 --- a/src/elementary-number-theory/integers.lagda.md +++ b/src/elementary-number-theory/integers.lagda.md @@ -22,6 +22,7 @@ open import foundation.homotopies open import foundation.identity-types open import foundation.injective-maps open import foundation.negated-equality +open import foundation.negation open import foundation.propositions open import foundation.retractions open import foundation.sections @@ -426,16 +427,71 @@ is-zero-is-nonnegative-neg-is-nonnegative-ℤ (inr (inl star)) nonneg nonpos = refl ``` +### Properties of positive integers + +#### The positivity predicate on integers is decidable + +```agda +decide-is-positive-ℤ : {x : ℤ} → (is-positive-ℤ x) + is-nonnegative-ℤ (neg-ℤ x) +decide-is-positive-ℤ {inl x} = inr star +decide-is-positive-ℤ {inr (inl x)} = inr star +decide-is-positive-ℤ {inr (inr x)} = inl star + +decide-is-positive-is-nonzero-ℤ : + (x : ℤ) → (x ≠ zero-ℤ) → + (is-positive-ℤ x) + is-positive-ℤ (neg-ℤ x) +decide-is-positive-is-nonzero-ℤ (inl x) H = inr star +decide-is-positive-is-nonzero-ℤ (inr (inl x)) H = ex-falso (H refl) +decide-is-positive-is-nonzero-ℤ (inr (inr x)) H = inl star +``` + +This remains to be fully formalized. + +### The nonpositive integers + +```agda +is-nonpositive-ℤ : ℤ → UU lzero +is-nonpositive-ℤ x = is-nonnegative-ℤ (neg-ℤ x) +``` + +#### Positive integers are not nonpositive + +```agda +not-is-nonpositive-is-positive-ℤ : + (x : ℤ) → is-positive-ℤ x → ¬ (is-nonpositive-ℤ x) +not-is-nonpositive-is-positive-ℤ (inr (inl x)) x-is-pos _ = x-is-pos +not-is-nonpositive-is-positive-ℤ (inr (inr x)) x-is-pos neg-x-is-nonneg = + neg-x-is-nonneg +``` + +#### An integer that is not positive is nonpositive + +```agda +is-nonpositive-not-is-positive-ℤ : + (x : ℤ) → ¬ (is-positive-ℤ x) → is-nonpositive-ℤ x +is-nonpositive-not-is-positive-ℤ x H with decide-is-positive-ℤ {x} +... | inl K = ex-falso (H K) +... | inr K = K +``` + +#### Relation between successors of natural numbers and integers + ```agda succ-int-ℕ : (x : ℕ) → succ-ℤ (int-ℕ x) ＝ int-ℕ (succ-ℕ x) succ-int-ℕ zero-ℕ = refl succ-int-ℕ (succ-ℕ x) = refl ``` +#### The negative function is injective + ```agda is-injective-neg-ℤ : is-injective neg-ℤ is-injective-neg-ℤ {x} {y} p = inv (neg-neg-ℤ x) ∙ ap neg-ℤ p ∙ neg-neg-ℤ y +``` +#### An integer is zero if its negative is zero + +```agda is-zero-is-zero-neg-ℤ : (x : ℤ) → is-zero-ℤ (neg-ℤ x) → is-zero-ℤ x is-zero-is-zero-neg-ℤ (inr (inl star)) H = refl ``` diff --git a/src/elementary-number-theory/mediant-integer-fractions.lagda.md b/src/elementary-number-theory/mediant-integer-fractions.lagda.md new file mode 100644 index 0000000000..56ee67d080 --- /dev/null +++ b/src/elementary-number-theory/mediant-integer-fractions.lagda.md @@ -0,0 +1,86 @@ +# The mediant fraction of two integer fractions + +```agda +module elementary-number-theory.mediant-integer-fractions where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-integers +open import elementary-number-theory.cross-multiplication-difference-integer-fractions +open import elementary-number-theory.difference-integers +open import elementary-number-theory.integer-fractions +open import elementary-number-theory.multiplication-integers + +open import foundation.dependent-pair-types +open import foundation.identity-types +``` + +
+ +## Idea + +The +{{#concept "mediant" Disambiguation="integer fractions" Agda=mediant-fraction-ℤ}} +of two fractions is the quotient of the sum of the numerators by the sum of the +denominators. + +## Definitions + +### The mediant of two fractions + +```agda +mediant-fraction-ℤ : fraction-ℤ → fraction-ℤ → fraction-ℤ +mediant-fraction-ℤ (a , b , p) (c , d , q) = + (a +ℤ c , b +ℤ d , is-positive-add-ℤ p q) +``` + +## Properties + +### The mediant preserves the cross-multiplication difference + +```agda +cross-mul-diff-left-mediant-fraction-ℤ : + (x y : fraction-ℤ) → + Id + ( cross-mul-diff-fraction-ℤ x y) + ( cross-mul-diff-fraction-ℤ x ( mediant-fraction-ℤ x y)) +cross-mul-diff-left-mediant-fraction-ℤ (nx , dx , px) (ny , dy , py) = + equational-reasoning + (ny *ℤ dx -ℤ nx *ℤ dy) + ＝ (nx *ℤ dx +ℤ ny *ℤ dx) -ℤ (nx *ℤ dx +ℤ nx *ℤ dy) + by inv + ( left-translation-diff-ℤ + ( mul-ℤ ny dx) + ( mul-ℤ nx dy) + ( mul-ℤ nx dx)) + ＝ (nx +ℤ ny) *ℤ dx -ℤ nx *ℤ (dx +ℤ dy) + by ap-diff-ℤ + ( inv (right-distributive-mul-add-ℤ nx ny dx)) + ( inv (left-distributive-mul-add-ℤ nx dx dy)) + +cross-mul-diff-right-mediant-fraction-ℤ : + (x y : fraction-ℤ) → + Id + ( cross-mul-diff-fraction-ℤ x y) + ( cross-mul-diff-fraction-ℤ (mediant-fraction-ℤ x y) y) +cross-mul-diff-right-mediant-fraction-ℤ (nx , dx , px) (ny , dy , py) = + equational-reasoning + (ny *ℤ dx -ℤ nx *ℤ dy) + ＝ (ny *ℤ dx +ℤ ny *ℤ dy) -ℤ (nx *ℤ dy +ℤ ny *ℤ dy) + by inv + ( right-translation-diff-ℤ + ( mul-ℤ ny dx) + ( mul-ℤ nx dy) + ( mul-ℤ ny dy)) + ＝ ny *ℤ (dx +ℤ dy) -ℤ (nx +ℤ ny) *ℤ dy + by ap-diff-ℤ + ( inv (left-distributive-mul-add-ℤ ny dx dy)) + ( inv (right-distributive-mul-add-ℤ nx ny dy)) +``` + +## External links + +- [Mediant fraction]() at + Wikipedia diff --git a/src/elementary-number-theory/multiplication-integers.lagda.md b/src/elementary-number-theory/multiplication-integers.lagda.md index b0b1f81d70..e9b7690aa8 100644 --- a/src/elementary-number-theory/multiplication-integers.lagda.md +++ b/src/elementary-number-theory/multiplication-integers.lagda.md @@ -536,4 +536,18 @@ preserves-leq-right-mul-ℤ x y z H K = ( commutative-mul-ℤ x z) ( preserves-leq-left-mul-ℤ x y z H K) ( commutative-mul-ℤ z y) + +preserves-strict-order-mul-positive-ℤ' : + {x y : ℤ} (z : ℤ) → is-positive-ℤ z → le-ℤ x y → le-ℤ (x *ℤ z) (y *ℤ z) +preserves-strict-order-mul-positive-ℤ' {x} {y} z H p = + is-positive-eq-ℤ + ( inv ( linear-diff-right-mul-ℤ y x z)) + ( is-positive-mul-ℤ p H) + +preserves-strict-order-mul-positive-ℤ : + {x y : ℤ} (z : ℤ) → is-positive-ℤ z → le-ℤ x y → le-ℤ (z *ℤ x) (z *ℤ y) +preserves-strict-order-mul-positive-ℤ {x} {y} z H p = + is-positive-eq-ℤ + ( inv ( linear-diff-left-mul-ℤ z y x)) + ( is-positive-mul-ℤ H p) ``` diff --git a/src/elementary-number-theory/rational-numbers.lagda.md b/src/elementary-number-theory/rational-numbers.lagda.md index 00c52582bc..b04a7d7592 100644 --- a/src/elementary-number-theory/rational-numbers.lagda.md +++ b/src/elementary-number-theory/rational-numbers.lagda.md @@ -11,6 +11,7 @@ open import elementary-number-theory.divisibility-integers open import elementary-number-theory.greatest-common-divisor-integers open import elementary-number-theory.integer-fractions open import elementary-number-theory.integers +open import elementary-number-theory.mediant-integer-fractions open import elementary-number-theory.reduced-integer-fractions open import foundation.dependent-pair-types @@ -39,11 +40,27 @@ equivalence relation given by `(n/m) ~ (n'/m') := Id (n *ℤ m') (n' *ℤ m)`. ℚ : UU lzero ℚ = Σ fraction-ℤ is-reduced-fraction-ℤ -fraction-ℚ : ℚ → fraction-ℤ -fraction-ℚ x = pr1 x +module _ + (x : ℚ) + where -is-reduced-fraction-ℚ : (x : ℚ) → is-reduced-fraction-ℤ (fraction-ℚ x) -is-reduced-fraction-ℚ x = pr2 x + fraction-ℚ : fraction-ℤ + fraction-ℚ = pr1 x + + is-reduced-fraction-ℚ : is-reduced-fraction-ℤ fraction-ℚ + is-reduced-fraction-ℚ = pr2 x + + numerator-ℚ : ℤ + numerator-ℚ = numerator-fraction-ℤ fraction-ℚ + + positive-denominator-ℚ : positive-ℤ + positive-denominator-ℚ = positive-denominator-fraction-ℤ fraction-ℚ + + denominator-ℚ : ℤ + denominator-ℚ = denominator-fraction-ℤ fraction-ℚ + + is-positive-denominator-ℚ : is-positive-ℤ denominator-ℚ + is-positive-denominator-ℚ = is-positive-denominator-fraction-ℤ fraction-ℚ ``` ### Inclusion of fractions @@ -86,6 +103,17 @@ is-one-ℚ : ℚ → UU lzero is-one-ℚ x = (x ＝ one-ℚ) ``` +### The mediant of two rationals + +```agda +mediant-ℚ : ℚ → ℚ → ℚ +mediant-ℚ x y = + in-fraction-ℤ + ( mediant-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y)) +``` + ## Properties ### If two fractions are related by `sim-fraction-ℤ`, then their embeddings into `ℚ` are equal diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index 06965bfcf1..ce0ae91405 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -6,4 +6,5 @@ module real-numbers where open import real-numbers.dedekind-real-numbers public +open import real-numbers.rational-real-numbers public ``` diff --git a/src/real-numbers/dedekind-real-numbers.lagda.md b/src/real-numbers/dedekind-real-numbers.lagda.md index 262eaed319..f50b97b7c0 100644 --- a/src/real-numbers/dedekind-real-numbers.lagda.md +++ b/src/real-numbers/dedekind-real-numbers.lagda.md @@ -10,14 +10,27 @@ module real-numbers.dedekind-real-numbers where open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.rational-numbers +open import foundation.binary-transport +open import foundation.cartesian-product-types +open import foundation.complements-subtypes +open import foundation.conjunction +open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.disjunction +open import foundation.embeddings +open import foundation.empty-types open import foundation.existential-quantification +open import foundation.function-types +open import foundation.functoriality-cartesian-product-types +open import foundation.functoriality-dependent-pair-types +open import foundation.identity-types open import foundation.logical-equivalences open import foundation.negation +open import foundation.propositional-truncations open import foundation.propositions open import foundation.sets open import foundation.subtypes +open import foundation.transport-along-identifications open import foundation.truncated-types open import foundation.universe-levels @@ -96,6 +109,65 @@ module _ ```agda ℝ : (l : Level) → UU (lsuc l) ℝ l = Σ (subtype l ℚ) (λ L → Σ (subtype l ℚ) (is-dedekind-cut L)) + +real-dedekind-cut : {l : Level} (L U : subtype l ℚ) → is-dedekind-cut L U → ℝ l +real-dedekind-cut L U H = L , U , H + +module _ + {l : Level} (x : ℝ l) + where + + lower-cut-ℝ : subtype l ℚ + lower-cut-ℝ = pr1 x + + upper-cut-ℝ : subtype l ℚ + upper-cut-ℝ = pr1 (pr2 x) + + is-in-lower-cut-ℝ : ℚ → UU l + is-in-lower-cut-ℝ = is-in-subtype lower-cut-ℝ + + is-in-upper-cut-ℝ : ℚ → UU l + is-in-upper-cut-ℝ = is-in-subtype upper-cut-ℝ + + is-dedekind-cut-cut-ℝ : is-dedekind-cut lower-cut-ℝ upper-cut-ℝ + is-dedekind-cut-cut-ℝ = pr2 (pr2 x) + + is-inhabited-lower-cut-ℝ : exists ℚ lower-cut-ℝ + is-inhabited-lower-cut-ℝ = pr1 (pr1 is-dedekind-cut-cut-ℝ) + + is-inhabited-upper-cut-ℝ : exists ℚ upper-cut-ℝ + is-inhabited-upper-cut-ℝ = pr2 (pr1 is-dedekind-cut-cut-ℝ) + + is-rounded-lower-cut-ℝ : + (q : ℚ) → + is-in-lower-cut-ℝ q ↔ ∃ ℚ (λ r → (le-ℚ q r) × (is-in-lower-cut-ℝ r)) + is-rounded-lower-cut-ℝ = + pr1 (pr1 (pr2 is-dedekind-cut-cut-ℝ)) + + is-rounded-upper-cut-ℝ : + (r : ℚ) → + is-in-upper-cut-ℝ r ↔ ∃ ℚ (λ q → (le-ℚ q r) × (is-in-upper-cut-ℝ q)) + is-rounded-upper-cut-ℝ = + pr2 (pr1 (pr2 is-dedekind-cut-cut-ℝ)) + + is-disjoint-cut-ℝ : (q : ℚ) → ¬ (is-in-lower-cut-ℝ q × is-in-upper-cut-ℝ q) + is-disjoint-cut-ℝ = + pr1 (pr2 (pr2 is-dedekind-cut-cut-ℝ)) + + is-located-lower-upper-cut-ℝ : + (q r : ℚ) → le-ℚ q r → (lower-cut-ℝ q) ∨ (upper-cut-ℝ r) + is-located-lower-upper-cut-ℝ = + pr2 (pr2 (pr2 is-dedekind-cut-cut-ℝ)) + + cut-ℝ : subtype l ℚ + cut-ℝ q = + coproduct-Prop + ( lower-cut-ℝ q) + ( upper-cut-ℝ q) + ( ev-pair ( is-disjoint-cut-ℝ q)) + + is-in-cut-ℝ : ℚ → UU l + is-in-cut-ℝ = is-in-subtype cut-ℝ ``` ## Properties @@ -121,6 +193,325 @@ pr1 (ℝ-Set l) = ℝ l pr2 (ℝ-Set l) = is-set-ℝ l ``` +## Properties of lower/upper Dedekind cuts + +### Lower and upper Dedekind cuts are closed under the standard ordering on the rationals + +```agda +module _ + {l : Level} (x : ℝ l) (p q : ℚ) + where + + le-lower-cut-ℝ : + le-ℚ p q → + is-in-lower-cut-ℝ x q → + is-in-lower-cut-ℝ x p + le-lower-cut-ℝ H H' = + ind-trunc-Prop + ( λ s → lower-cut-ℝ x p) + ( rec-coproduct + ( id) + ( λ I → ex-falso (is-disjoint-cut-ℝ x q (H' , I)))) + ( is-located-lower-upper-cut-ℝ x p q H) + + leq-lower-cut-ℝ : + leq-ℚ p q → + is-in-lower-cut-ℝ x q → + is-in-lower-cut-ℝ x p + leq-lower-cut-ℝ H H' = + rec-coproduct + ( λ s → le-lower-cut-ℝ s H') + ( λ I → + tr + ( is-in-lower-cut-ℝ x) + ( antisymmetric-leq-ℚ q p I H) + ( H')) + ( decide-le-leq-ℚ p q) + + le-upper-cut-ℝ : + le-ℚ p q → + is-in-upper-cut-ℝ x p → + is-in-upper-cut-ℝ x q + le-upper-cut-ℝ H H' = + ind-trunc-Prop + ( λ s → upper-cut-ℝ x q) + ( rec-coproduct + ( λ I → ex-falso (is-disjoint-cut-ℝ x p ( I , H'))) + ( id)) + ( is-located-lower-upper-cut-ℝ x p q H) + + leq-upper-cut-ℝ : + leq-ℚ p q → + is-in-upper-cut-ℝ x p → + is-in-upper-cut-ℝ x q + leq-upper-cut-ℝ H H' = + rec-coproduct + ( λ s → le-upper-cut-ℝ s H') + ( λ I → + tr + ( is-in-upper-cut-ℝ x) + ( antisymmetric-leq-ℚ p q H I) + ( H')) + ( decide-le-leq-ℚ p q) +``` + +### Elements of the lower cut are lower bounds of the upper cut + +```agda +module _ + {l : Level} (x : ℝ l) (p q : ℚ) + where + + le-lower-upper-cut-ℝ : + is-in-lower-cut-ℝ x p → + is-in-upper-cut-ℝ x q → + le-ℚ p q + le-lower-upper-cut-ℝ H H' = + rec-coproduct + ( id) + ( λ I → + ex-falso + ( is-disjoint-cut-ℝ x p + ( H , leq-upper-cut-ℝ x q p I H'))) + ( decide-le-leq-ℚ p q) +``` + +### Characterisation of each cut by the other + +#### The lower cut is the subtype of rationals bounded above by some element of the complement of the upper cut + +```agda +module _ + {l : Level} (x : ℝ l) + where + + is-lower-complement-upper-cut-ℝ-Prop : (p q : ℚ) → Prop l + is-lower-complement-upper-cut-ℝ-Prop p q = + product-Prop + ( le-ℚ-Prop p q) + ( neg-Prop ( upper-cut-ℝ x q)) + + lower-complement-upper-cut-ℝ : subtype l ℚ + lower-complement-upper-cut-ℝ p = + exists-Prop ℚ (is-lower-complement-upper-cut-ℝ-Prop p) +``` + +```agda +module _ + {l : Level} (x : ℝ l) + where + + subset-lower-cut-lower-complement-upper-cut-ℝ : + lower-complement-upper-cut-ℝ x ⊆ lower-cut-ℝ x + subset-lower-cut-lower-complement-upper-cut-ℝ p = + elim-exists-Prop + ( is-lower-complement-upper-cut-ℝ-Prop x p) + ( lower-cut-ℝ x p) + ( λ q I → + map-right-unit-law-disjunction-is-empty-Prop + ( lower-cut-ℝ x p) + ( upper-cut-ℝ x q) + ( pr2 I) + ( is-located-lower-upper-cut-ℝ x p q ( pr1 I))) + + subset-lower-complement-upper-cut-lower-cut-ℝ : + lower-cut-ℝ x ⊆ lower-complement-upper-cut-ℝ x + subset-lower-complement-upper-cut-lower-cut-ℝ p H = + elim-exists-Prop + ( λ q → product-Prop (le-ℚ-Prop p q) (lower-cut-ℝ x q)) + ( lower-complement-upper-cut-ℝ x p) + ( λ q I → + intro-exists + ( is-lower-complement-upper-cut-ℝ-Prop x p) + ( q) + ( map-product + ( id) + ( λ L U → is-disjoint-cut-ℝ x q (L , U)) + ( I))) + ( pr1 (is-rounded-lower-cut-ℝ x p) H) + + eq-lower-cut-lower-complement-upper-cut-ℝ : + lower-complement-upper-cut-ℝ x ＝ lower-cut-ℝ x + eq-lower-cut-lower-complement-upper-cut-ℝ = + antisymmetric-leq-subtype + ( lower-complement-upper-cut-ℝ x) + ( lower-cut-ℝ x) + ( subset-lower-cut-lower-complement-upper-cut-ℝ) + ( subset-lower-complement-upper-cut-lower-cut-ℝ) +``` + +#### The upper cut is the subtype of rationals bounded below by some element of the complement of the lower cut + +```agda +module _ + {l : Level} (x : ℝ l) + where + + is-upper-complement-lower-cut-ℝ-Prop : (q p : ℚ) → Prop l + is-upper-complement-lower-cut-ℝ-Prop q p = + product-Prop + ( le-ℚ-Prop p q) + ( neg-Prop ( lower-cut-ℝ x p)) + + upper-complement-lower-cut-ℝ : subtype l ℚ + upper-complement-lower-cut-ℝ q = + exists-Prop ℚ (is-upper-complement-lower-cut-ℝ-Prop q) +``` + +```agda +module _ + {l : Level} (x : ℝ l) + where + + subset-upper-cut-upper-complement-lower-cut-ℝ : + upper-complement-lower-cut-ℝ x ⊆ upper-cut-ℝ x + subset-upper-cut-upper-complement-lower-cut-ℝ q = + elim-exists-Prop + ( is-upper-complement-lower-cut-ℝ-Prop x q) + ( upper-cut-ℝ x q) + ( λ p I → + map-left-unit-law-disjunction-is-empty-Prop + ( lower-cut-ℝ x p) + ( upper-cut-ℝ x q) + ( pr2 I) + ( is-located-lower-upper-cut-ℝ x p q ( pr1 I))) + + subset-upper-complement-lower-cut-upper-cut-ℝ : + upper-cut-ℝ x ⊆ upper-complement-lower-cut-ℝ x + subset-upper-complement-lower-cut-upper-cut-ℝ q H = + elim-exists-Prop + ( λ p → product-Prop (le-ℚ-Prop p q) (upper-cut-ℝ x p)) + ( upper-complement-lower-cut-ℝ x q) + ( λ p I → + intro-exists + ( is-upper-complement-lower-cut-ℝ-Prop x q) + ( p) + ( map-product + ( id) + ( λ U L → is-disjoint-cut-ℝ x p (L , U)) + ( I))) + ( pr1 (is-rounded-upper-cut-ℝ x q) H) + + eq-upper-cut-upper-complement-lower-cut-ℝ : + upper-complement-lower-cut-ℝ x ＝ upper-cut-ℝ x + eq-upper-cut-upper-complement-lower-cut-ℝ = + antisymmetric-leq-subtype + ( upper-complement-lower-cut-ℝ x) + ( upper-cut-ℝ x) + ( subset-upper-cut-upper-complement-lower-cut-ℝ) + ( subset-upper-complement-lower-cut-upper-cut-ℝ) +``` + +### The lower/upper cut of a real determines the other + +```agda +module _ + {l : Level} (x y : ℝ l) + where + + subset-lower-cut-upper-cut-ℝ : + upper-cut-ℝ y ⊆ upper-cut-ℝ x → lower-cut-ℝ x ⊆ lower-cut-ℝ y + subset-lower-cut-upper-cut-ℝ H = + binary-tr + ( _⊆_) + ( eq-lower-cut-lower-complement-upper-cut-ℝ x) + ( eq-lower-cut-lower-complement-upper-cut-ℝ y) + ( λ p → + elim-exists-Prop + ( is-lower-complement-upper-cut-ℝ-Prop x p) + ( lower-complement-upper-cut-ℝ y p) + ( λ q → intro-∃ q ∘ tot (λ _ K → K ∘ H q))) + + subset-upper-cut-lower-cut-ℝ : + lower-cut-ℝ x ⊆ lower-cut-ℝ y → upper-cut-ℝ y ⊆ upper-cut-ℝ x + subset-upper-cut-lower-cut-ℝ H = + binary-tr + ( _⊆_) + ( eq-upper-cut-upper-complement-lower-cut-ℝ y) + ( eq-upper-cut-upper-complement-lower-cut-ℝ x) + ( λ q → + elim-exists-Prop + ( is-upper-complement-lower-cut-ℝ-Prop y q) + ( upper-complement-lower-cut-ℝ x q) + ( λ p → intro-∃ p ∘ tot (λ _ K → K ∘ H p))) + +module _ + {l : Level} (x y : ℝ l) + where + + eq-lower-cut-eq-upper-cut-ℝ : + upper-cut-ℝ x ＝ upper-cut-ℝ y → lower-cut-ℝ x ＝ lower-cut-ℝ y + eq-lower-cut-eq-upper-cut-ℝ H = + antisymmetric-leq-subtype + ( lower-cut-ℝ x) + ( lower-cut-ℝ y) + ( subset-lower-cut-upper-cut-ℝ x y + ( pr2 ∘ has-same-elements-eq-subtype + ( upper-cut-ℝ x) + ( upper-cut-ℝ y) + ( H))) + ( subset-lower-cut-upper-cut-ℝ y x + ( pr1 ∘ has-same-elements-eq-subtype + ( upper-cut-ℝ x) + ( upper-cut-ℝ y) + ( H))) + + eq-upper-cut-eq-lower-cut-ℝ : + lower-cut-ℝ x ＝ lower-cut-ℝ y → upper-cut-ℝ x ＝ upper-cut-ℝ y + eq-upper-cut-eq-lower-cut-ℝ H = + antisymmetric-leq-subtype + ( upper-cut-ℝ x) + ( upper-cut-ℝ y) + ( subset-upper-cut-lower-cut-ℝ y x + ( pr2 ∘ has-same-elements-eq-subtype + ( lower-cut-ℝ x) + ( lower-cut-ℝ y) + ( H))) + ( subset-upper-cut-lower-cut-ℝ x y + ( pr1 ∘ has-same-elements-eq-subtype + ( lower-cut-ℝ x) + ( lower-cut-ℝ y) + ( H))) +``` + +### The map from a real number to its lower cut is an embedding + +```agda +module _ + {l : Level} (L : subtype l ℚ) + where + + has-upper-cut-Prop : Prop (lsuc l) + has-upper-cut-Prop = + pair + ( Σ (subtype l ℚ) (is-dedekind-cut L)) + ( is-prop-all-elements-equal + ( λ U U' → + eq-type-subtype + ( is-dedekind-cut-Prop L) + ( eq-upper-cut-eq-lower-cut-ℝ + ( pair L U) + ( pair L U') + ( refl)))) + +is-emb-lower-cut : {l : Level} → is-emb (lower-cut-ℝ {l}) +is-emb-lower-cut = is-emb-inclusion-subtype has-upper-cut-Prop +``` + +### Two real numbers with the same lower/upper cut are equal + +```agda +module _ + {l : Level} (x y : ℝ l) + where + + eq-eq-lower-cut-ℝ : lower-cut-ℝ x ＝ lower-cut-ℝ y → x ＝ y + eq-eq-lower-cut-ℝ = eq-type-subtype has-upper-cut-Prop + + eq-eq-upper-cut-ℝ : upper-cut-ℝ x ＝ upper-cut-ℝ y → x ＝ y + eq-eq-upper-cut-ℝ = eq-eq-lower-cut-ℝ ∘ (eq-lower-cut-eq-upper-cut-ℝ x y) +``` + ## References 1. Section 11.2 of Univalent Foundations Project, _Homotopy Type Theory – diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md new file mode 100644 index 0000000000..878b9e33fc --- /dev/null +++ b/src/real-numbers/rational-real-numbers.lagda.md @@ -0,0 +1,256 @@ +# Rational real numbers + +```agda +module real-numbers.rational-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.rational-numbers + +open import foundation.action-on-identifications-functions +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.disjunction +open import foundation.embeddings +open import foundation.empty-types +open import foundation.equivalences +open import foundation.existential-quantification +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.negation +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.retractions +open import foundation.sections +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import real-numbers.dedekind-real-numbers +``` + +
+ +## Idea + +The type of [rationals](elementary-number-theory.rational-numbers.md) `ℚ` +[embeds](foundation-core.embeddings.md) into the type of +[Dedekind reals](real-numbers.dedekind-real-numbers.md) `ℝ`. We call numbers in +the [image](foundation.images.md) of this embedding +{{#concept "rational real numbers" Agda=Rational-ℝ}}. + +## Definitions + +### Strict inequality on rationals gives Dedekind cuts + +```agda +is-dedekind-cut-le-ℚ : + (x : ℚ) → + is-dedekind-cut + (λ (q : ℚ) → le-ℚ-Prop q x) + (λ (r : ℚ) → le-ℚ-Prop x r) +is-dedekind-cut-le-ℚ x = + ( left-∃-le-ℚ x , right-∃-le-ℚ x) , + ( ( λ (q : ℚ) → + dense-le-ℚ q x , + elim-exists-Prop + ( λ r → product-Prop ( le-ℚ-Prop q r) ( le-ℚ-Prop r x)) + ( le-ℚ-Prop q x) + ( λ r (H , H') → transitive-le-ℚ q r x H H')) , + ( λ (r : ℚ) → + α x r ∘ dense-le-ℚ x r , + elim-exists-Prop + ( λ q → product-Prop ( le-ℚ-Prop q r) ( le-ℚ-Prop x q)) + ( le-ℚ-Prop x r) + ( λ q (H , H') → transitive-le-ℚ x q r H' H))) , + ( λ (q : ℚ) (H , H') → asymmetric-le-ℚ q x H H') , + ( located-le-ℚ x) + where + α : + (a b : ℚ) → + ∃ ℚ (λ r → le-ℚ a r × le-ℚ r b) → + ∃ ℚ (λ r → le-ℚ r b × le-ℚ a r) + α a b = + elim-exists-Prop + ( ( λ r → + product-Prop + ( le-ℚ-Prop a r) + ( le-ℚ-Prop r b))) + ( exists-Prop ℚ + ( λ r → + product-Prop + ( le-ℚ-Prop r b) + ( le-ℚ-Prop a r))) + ( λ r ( p , q) → intro-∃ r ( q , p)) +``` + +### The canonical map from `ℚ` to `ℝ` + +```agda +real-rational : ℚ → ℝ lzero +real-rational x = + real-dedekind-cut + ( λ (q : ℚ) → le-ℚ-Prop q x) + ( λ (r : ℚ) → le-ℚ-Prop x r) + ( is-dedekind-cut-le-ℚ x) +``` + +### The property of being a rational real number + +```agda +module _ + {l : Level} (x : ℝ l) (p : ℚ) + where + + is-rational-ℝ-Prop : Prop l + is-rational-ℝ-Prop = + product-Prop + ( neg-Prop (lower-cut-ℝ x p)) + ( neg-Prop (upper-cut-ℝ x p)) + + is-rational-ℝ : UU l + is-rational-ℝ = type-Prop is-rational-ℝ-Prop +``` + +```agda +all-eq-is-rational-ℝ : + {l : Level} (x : ℝ l) (p q : ℚ) → + is-rational-ℝ x p → + is-rational-ℝ x q → + p ＝ q +all-eq-is-rational-ℝ x p q H H' = + trichotomy-le-ℚ p q left-case id right-case + where + left-case : le-ℚ p q → p ＝ q + left-case I = + ex-falso + ( elim-disjunction-Prop + ( lower-cut-ℝ x p) + ( upper-cut-ℝ x q) + ( empty-Prop) + ( pr1 H , pr2 H') + ( is-located-lower-upper-cut-ℝ x p q I)) + + right-case : le-ℚ q p → p ＝ q + right-case I = + ex-falso + ( elim-disjunction-Prop + ( lower-cut-ℝ x q) + ( upper-cut-ℝ x p) + ( empty-Prop) + ( pr1 H' , pr2 H) + ( is-located-lower-upper-cut-ℝ x q p I)) + +is-prop-rational-real : {l : Level} (x : ℝ l) → is-prop (Σ ℚ (is-rational-ℝ x)) +is-prop-rational-real x = + is-prop-all-elements-equal + ( λ p q → + eq-type-subtype + ( is-rational-ℝ-Prop x) + ( all-eq-is-rational-ℝ x (pr1 p) (pr1 q) (pr2 p) (pr2 q))) +``` + +### The subtype of rational reals + +```agda +subtype-rational-real : {l : Level} → ℝ l → Prop l +subtype-rational-real x = + Σ ℚ (is-rational-ℝ x) , is-prop-rational-real x + +Rational-ℝ : (l : Level) → UU (lsuc l) +Rational-ℝ l = + type-subtype subtype-rational-real + +module _ + {l : Level} (x : Rational-ℝ l) + where + + real-rational-ℝ : ℝ l + real-rational-ℝ = pr1 x + + rational-rational-ℝ : ℚ + rational-rational-ℝ = pr1 (pr2 x) + + is-rational-rational-ℝ : is-rational-ℝ real-rational-ℝ rational-rational-ℝ + is-rational-rational-ℝ = pr2 (pr2 x) +``` + +## Properties + +### The real embedding of a rational number is rational + +```agda +is-rational-real-rational : (p : ℚ) → is-rational-ℝ (real-rational p) p +is-rational-real-rational p = irreflexive-le-ℚ p , irreflexive-le-ℚ p +``` + +### Rational real numbers are embedded rationals + +```agda +eq-real-rational-is-rational-ℝ : + (x : ℝ lzero) (q : ℚ) (H : is-rational-ℝ x q) → real-rational q ＝ x +eq-real-rational-is-rational-ℝ x q H = + eq-eq-lower-cut-ℝ + ( real-rational q) + ( x) + ( eq-has-same-elements-subtype + ( λ p → le-ℚ-Prop p q) + ( lower-cut-ℝ x) + ( λ r → + pair + ( λ I → elim-disjunction-Prop + ( lower-cut-ℝ x r) + ( upper-cut-ℝ x q) + ( lower-cut-ℝ x r) + ( id , λ H' → ex-falso (pr2 H H')) + ( is-located-lower-upper-cut-ℝ x r q I)) + ( trichotomy-le-ℚ r q + ( λ I _ → I) + ( λ E H' → ex-falso (pr1 (tr (is-rational-ℝ x) (inv E) H) H')) + ( λ I H' → ex-falso (pr1 H (le-lower-cut-ℝ x q r I H')))))) +``` + +### The cannonical map from rationals to rational reals + +```agda +rational-ℝ-rational : ℚ → Rational-ℝ lzero +rational-ℝ-rational q = real-rational q , q , is-rational-real-rational q +``` + +### The rationals and rational reals are equivalent + +```agda +is-section-rational-ℝ-rational : + (q : ℚ) → + rational-rational-ℝ (rational-ℝ-rational q) ＝ q +is-section-rational-ℝ-rational q = refl + +is-retraction-rational-ℝ-rational : + (x : Rational-ℝ lzero) → + rational-ℝ-rational (rational-rational-ℝ x) ＝ x +is-retraction-rational-ℝ-rational (x , q , H) = + eq-type-subtype + subtype-rational-real + ( ap real-rational α ∙ eq-real-rational-is-rational-ℝ x q H) + where + α : rational-rational-ℝ (x , q , H) ＝ q + α = refl + +equiv-rational-real : Rational-ℝ lzero ≃ ℚ +pr1 equiv-rational-real = rational-rational-ℝ +pr2 equiv-rational-real = + section-rational-rational-ℝ , retraction-rational-rational-ℝ + where + section-rational-rational-ℝ : section rational-rational-ℝ + section-rational-rational-ℝ = + rational-ℝ-rational , is-section-rational-ℝ-rational + + retraction-rational-rational-ℝ : retraction rational-rational-ℝ + retraction-rational-rational-ℝ = + rational-ℝ-rational , is-retraction-rational-ℝ-rational +```