From d40c12ed87e57554ec7f29464c9ee274a4d8664a Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Tue, 21 Apr 2026 18:27:13 -0700 Subject: [PATCH 01/14] Progress --- .../inequality-standard-finite-types.lagda.md | 37 +++ src/lists.lagda.md | 1 + src/lists/arrays.lagda.md | 13 - src/lists/finite-sequences.lagda.md | 9 +- src/lists/nonempty-arrays.lagda.md | 83 +++++++ src/order-theory.lagda.md | 3 + .../increasing-arrays-posets.lagda.md | 49 ++++ ...ncreasing-finite-sequences-posets.lagda.md | 173 +++++++++++++ ...increasing-nonempty-arrays-posets.lagda.md | 235 ++++++++++++++++++ .../standard-finite-types.lagda.md | 10 + 10 files changed, 599 insertions(+), 14 deletions(-) create mode 100644 src/lists/nonempty-arrays.lagda.md create mode 100644 src/order-theory/increasing-arrays-posets.lagda.md create mode 100644 src/order-theory/increasing-finite-sequences-posets.lagda.md create mode 100644 src/order-theory/increasing-nonempty-arrays-posets.lagda.md diff --git a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md index da2ee242dff..efc5ec52d5c 100644 --- a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md +++ b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md @@ -23,6 +23,7 @@ open import foundation.propositions open import foundation.unit-type open import foundation.universe-levels +open import order-theory.order-preserving-maps-posets open import order-theory.posets open import order-theory.preorders @@ -145,6 +146,18 @@ abstract reflects-leq-nat-Fin (succ-ℕ k) {inr star} {inr star} H = star ``` +### The reverse embedding of the standard finite types in the natural numbers reverses inequality + +```agda +abstract + reverses-leq-nat-Fin-reverse : + (k : ℕ) (x y : Fin k) → leq-Fin k x y → + leq-ℕ (nat-Fin-reverse k y) (nat-Fin-reverse k x) + reverses-leq-nat-Fin-reverse (succ-ℕ k) x (inr star) x≤y = star + reverses-leq-nat-Fin-reverse (succ-ℕ k) (inl x) (inl y) x≤y = + reverses-leq-nat-Fin-reverse k x y x≤y +``` + ### Ordering on the standard finite types is decidable ```agda @@ -168,3 +181,27 @@ linear-leq-Fin (succ-ℕ k) (inl x) (inl y) = linear-leq-Fin k x y linear-leq-Fin (succ-ℕ k) (inl x) (inr y) = inl star linear-leq-Fin (succ-ℕ k) (inr x) y = inr star ``` + +### `skip-zero-Fin` preserves inequality + +```agda +abstract + preserves-order-skip-zero-Fin : + (n : ℕ) → + preserves-order-Poset (Fin-Poset n) (Fin-Poset (succ-ℕ n)) (skip-zero-Fin n) + preserves-order-skip-zero-Fin (succ-ℕ n) (inl x) (inl y) x≤y = + preserves-order-skip-zero-Fin n x y x≤y + preserves-order-skip-zero-Fin (succ-ℕ n) (inl x) (inr star) _ = star + preserves-order-skip-zero-Fin (succ-ℕ n) (inr x) (inr star) _ = star +``` + +### `zero-Fin n` is the least element of `Fin (succ-ℕ n)` + +```agda +abstract + leq-zero-Fin : + (n : ℕ) (i : Fin (succ-ℕ n)) → leq-Fin (succ-ℕ n) (zero-Fin n) i + leq-zero-Fin 0 (inr star) = star + leq-zero-Fin (succ-ℕ n) (inl i) = leq-zero-Fin n i + leq-zero-Fin (succ-ℕ n) (inr star) = star +``` diff --git a/src/lists.lagda.md b/src/lists.lagda.md index 35af1bbf5ec..94c6cd5f2c6 100644 --- a/src/lists.lagda.md +++ b/src/lists.lagda.md @@ -19,6 +19,7 @@ open import lists.functoriality-tuples public open import lists.functoriality-tuples-finite-sequences public open import lists.lists public open import lists.lists-discrete-types public +open import lists.nonempty-arrays public open import lists.partial-sequences public open import lists.permutation-lists public open import lists.permutation-tuples public diff --git a/src/lists/arrays.lagda.md b/src/lists/arrays.lagda.md index 7b14ee7ed91..367ba86da66 100644 --- a/src/lists/arrays.lagda.md +++ b/src/lists/arrays.lagda.md @@ -70,19 +70,6 @@ module _ is-empty-array : array A → UU lzero is-empty-array = type-Prop ∘ is-empty-array-Prop - is-nonempty-array-Prop : array A → Prop lzero - is-nonempty-array-Prop (zero-ℕ , t) = empty-Prop - is-nonempty-array-Prop (succ-ℕ n , t) = unit-Prop - - is-nonempty-array : array A → UU lzero - is-nonempty-array = type-Prop ∘ is-nonempty-array-Prop - - head-array : (t : array A) → is-nonempty-array t → A - head-array (succ-ℕ n , f) _ = f (inr star) - - tail-array : (t : array A) → is-nonempty-array t → array A - tail-array (succ-ℕ n , f) _ = n , f ∘ inl - cons-array : A → array A → array A cons-array a t = ( succ-ℕ (length-array t) , diff --git a/src/lists/finite-sequences.lagda.md b/src/lists/finite-sequences.lagda.md index da8d60f6daf..d1c2f56684e 100644 --- a/src/lists/finite-sequences.lagda.md +++ b/src/lists/finite-sequences.lagda.md @@ -54,12 +54,19 @@ module _ empty-fin-sequence () head-fin-sequence : (n : ℕ) → fin-sequence A (succ-ℕ n) → A - head-fin-sequence n v = v (inr star) + head-fin-sequence n v = v (neg-one-Fin n) + + last-fin-sequence : (n : ℕ) → fin-sequence A (succ-ℕ n) → A + last-fin-sequence n v = v (zero-Fin n) tail-fin-sequence : (n : ℕ) → fin-sequence A (succ-ℕ n) → fin-sequence A n tail-fin-sequence n v = v ∘ (inl-Fin n) + init-fin-sequence : + (n : ℕ) → fin-sequence A (succ-ℕ n) → fin-sequence A n + init-fin-sequence n v = v ∘ skip-zero-Fin n + cons-fin-sequence : (n : ℕ) → A → fin-sequence A n → fin-sequence A (succ-ℕ n) cons-fin-sequence n a v (inl x) = v x diff --git a/src/lists/nonempty-arrays.lagda.md b/src/lists/nonempty-arrays.lagda.md new file mode 100644 index 00000000000..c9410440e93 --- /dev/null +++ b/src/lists/nonempty-arrays.lagda.md @@ -0,0 +1,83 @@ +# Nonempty arrays + +```agda +module lists.nonempty-arrays where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-natural-numbers + +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.function-types +open import foundation.propositions +open import foundation.subtypes +open import foundation.unit-type +open import foundation.universe-levels + +open import lists.arrays +open import lists.finite-sequences + +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +An [array](lists.arrays.md) is +{{#concept "nonempty" Disambiguation="arrays" Agda=is-nonempty-array}} if it has +at least one element. + +## Definition + +```agda +module _ + {l : Level} {A : UU l} + where + + is-nonempty-array-Prop : array A → Prop lzero + is-nonempty-array-Prop (zero-ℕ , t) = empty-Prop + is-nonempty-array-Prop (succ-ℕ n , t) = unit-Prop + + is-nonempty-array : array A → UU lzero + is-nonempty-array = type-Prop ∘ is-nonempty-array-Prop + +nonempty-array : {l : Level} → UU l → UU l +nonempty-array A = type-subtype (is-nonempty-array-Prop {A = A}) + +module _ + {l : Level} {A : UU l} + where + + length-nonempty-array : nonempty-array A → ℕ + length-nonempty-array ((n , _) , _) = n + + is-nonzero-length-nonempty-array : + (a : nonempty-array A) → is-nonzero-ℕ (length-nonempty-array a) + is-nonzero-length-nonempty-array ((succ-ℕ n , _) , _) () + + nonzero-length-nonempty-array : nonempty-array A → ℕ⁺ + nonzero-length-nonempty-array a = + ( length-nonempty-array a , + is-nonzero-length-nonempty-array a) + + fin-sequence-nonempty-array : + (a : nonempty-array A) → fin-sequence A (length-nonempty-array a) + fin-sequence-nonempty-array ((_ , u) , _) = u + + head-nonempty-array : nonempty-array A → A + head-nonempty-array ((succ-ℕ n , u) , _) = u (neg-one-Fin n) + + tail-nonempty-array : nonempty-array A → array A + tail-nonempty-array ((succ-ℕ n , u) , _) = (n , u ∘ inl-Fin n) + + last-nonempty-array : nonempty-array A → A + last-nonempty-array ((succ-ℕ n , u) , _) = u (zero-Fin n) + + init-nonempty-array : nonempty-array A → array A + init-nonempty-array ((succ-ℕ n , u) , _) = (n , u ∘ skip-zero-Fin n) +``` diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md index 85707fe438d..be413808c90 100644 --- a/src/order-theory.lagda.md +++ b/src/order-theory.lagda.md @@ -62,6 +62,9 @@ open import order-theory.homomorphisms-meet-suplattices public open import order-theory.homomorphisms-suplattices public open import order-theory.ideals-preorders public open import order-theory.incidence-algebras public +open import order-theory.increasing-arrays-posets public +open import order-theory.increasing-finite-sequences-posets public +open import order-theory.increasing-nonempty-arrays-posets public open import order-theory.increasing-sequences-posets public open import order-theory.inflationary-maps-posets public open import order-theory.inflationary-maps-preorders public diff --git a/src/order-theory/increasing-arrays-posets.lagda.md b/src/order-theory/increasing-arrays-posets.lagda.md new file mode 100644 index 00000000000..c96578ae8ca --- /dev/null +++ b/src/order-theory/increasing-arrays-posets.lagda.md @@ -0,0 +1,49 @@ +# Increasing arrays in posets + +```agda +module order-theory.increasing-arrays-posets where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.subtypes +open import foundation.universe-levels + +open import lists.arrays +open import lists.nonempty-arrays + +open import order-theory.increasing-finite-sequences-posets +open import order-theory.posets +``` + +
+ +## Idea + +An [array](lists.arrays.md) in a [poset](order-theory.posets.md) is +{{#concept "increasing" Disambiguation="array in a poset" Agda=is-increasing-array-type-Poset}} +if its associated [finite sequence](lists.finite-sequences.md) is +[increasing](order-theory.increasing-finite-sequences-posets.md). + +## Definition + +```agda +module _ + {l1 l2 : Level} + (P : Poset l1 l2) + where + + is-increasing-prop-array-type-Poset : subtype l2 (array (type-Poset P)) + is-increasing-prop-array-type-Poset (n , u) = + is-increasing-prop-fin-sequence-type-Poset P n u + + is-increasing-array-type-Poset : array (type-Poset P) → UU l2 + is-increasing-array-type-Poset = + is-in-subtype is-increasing-prop-array-type-Poset + + increasing-array-type-Poset : UU (l1 ⊔ l2) + increasing-array-type-Poset = + type-subtype is-increasing-prop-array-type-Poset +``` diff --git a/src/order-theory/increasing-finite-sequences-posets.lagda.md b/src/order-theory/increasing-finite-sequences-posets.lagda.md new file mode 100644 index 00000000000..453288fbd86 --- /dev/null +++ b/src/order-theory/increasing-finite-sequences-posets.lagda.md @@ -0,0 +1,173 @@ +# Increasing finite sequences in posets + +```agda +module order-theory.increasing-finite-sequences-posets where +``` + +
Imports + +```agda +open import elementary-number-theory.inequality-standard-finite-types +open import elementary-number-theory.natural-numbers + +open import foundation.conjunction +open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.logical-equivalences +open import foundation.propositions +open import foundation.subtypes +open import foundation.unit-type +open import foundation.universe-levels + +open import lists.finite-sequences + +open import order-theory.opposite-posets +open import order-theory.order-preserving-maps-posets +open import order-theory.posets + +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +A [finite sequence](lists.finite-sequences.md) of elements of a +[poset](order-theory.posets.md) is +{{#concept "increasing" Disambiguation="finite sequence in a poset" Agda=is-increasing-fin-sequence-Poset}} +if each element is less than or equal to the next. + +## Definition + +```agda +module _ + {l1 l2 : Level} + (P : Poset l1 l2) + where + + is-increasing-prop-fin-sequence-type-Poset : + (n : ℕ) → subtype l2 (fin-sequence (type-Poset P) n) + is-increasing-prop-fin-sequence-type-Poset 0 _ = raise-unit-Prop l2 + is-increasing-prop-fin-sequence-type-Poset 1 _ = raise-unit-Prop l2 + is-increasing-prop-fin-sequence-type-Poset (succ-ℕ (succ-ℕ n)) u = + ( leq-prop-Poset + ( P) + ( u (neg-one-Fin (succ-ℕ n))) + ( u (neg-two-Fin (succ-ℕ n)))) ∧ + ( is-increasing-prop-fin-sequence-type-Poset + ( succ-ℕ n) + ( tail-fin-sequence (succ-ℕ n) u)) + + is-increasing-fin-sequence-type-Poset : + (n : ℕ) → fin-sequence (type-Poset P) n → UU l2 + is-increasing-fin-sequence-type-Poset n = + is-in-subtype (is-increasing-prop-fin-sequence-type-Poset n) + + increasing-fin-sequence-type-Poset : ℕ → UU (l1 ⊔ l2) + increasing-fin-sequence-type-Poset n = + type-subtype (is-increasing-prop-fin-sequence-type-Poset n) + +module _ + {l1 l2 : Level} + (P : Poset l1 l2) + (n : ℕ) + ((u , H) : increasing-fin-sequence-type-Poset P n) + where + + fin-sequence-increasing-fin-sequence-type-Poset : + fin-sequence (type-Poset P) n + fin-sequence-increasing-fin-sequence-type-Poset = u + + is-increasing-fin-sequence-increasing-fin-sequence-type-Poset : + is-increasing-fin-sequence-type-Poset + ( P) + ( n) + ( fin-sequence-increasing-fin-sequence-type-Poset) + is-increasing-fin-sequence-increasing-fin-sequence-type-Poset = H +``` + +## Properties + +### A finite sequence in a poset `P` is increasing if and only if it is an order-reversing map from `Fin n` to `P` + +The +[standard ordering](elementary-number-theory.inequality-standard-finite-types.md) +on the [standard finite types](univalent-combinatorics.standard-finite-types.md) +defines `neg-one-Fin n` as the greatest element of `Fin (succ-ℕ n)`, but finite +sequences use `neg-one-Fin n` as the head, which is conventionally the first +element of the sequence. + +We choose to adopt the convention that the head of an increasing sequence is its +least element, requiring us to reverse the order of `Fin n`. + +```agda +module _ + {l1 l2 : Level} + (P : Poset l1 l2) + where + + abstract + reverses-order-is-increasing-fin-sequence-type-Poset : + (n : ℕ) (u : fin-sequence (type-Poset P) n) → + is-increasing-fin-sequence-type-Poset P n u → + preserves-order-Poset (opposite-Poset (Fin-Poset n)) P u + reverses-order-is-increasing-fin-sequence-type-Poset + (succ-ℕ n) u _ (inr star) (inr star) _ = + refl-leq-Poset P (u (inr star)) + reverses-order-is-increasing-fin-sequence-type-Poset + (succ-ℕ (succ-ℕ n)) u (u₁≤u₂ , increasing-tail-u) (inr star) (inl j) _ = + transitive-leq-Poset + ( P) + ( u (inr star)) + ( u (inl (inr star))) + ( u (inl j)) + ( reverses-order-is-increasing-fin-sequence-type-Poset + ( succ-ℕ n) + ( tail-fin-sequence (succ-ℕ n) u) + ( increasing-tail-u) + ( inr star) + ( j) + ( star)) + ( u₁≤u₂) + reverses-order-is-increasing-fin-sequence-type-Poset + (succ-ℕ (succ-ℕ n)) u (u₁≤u₂ , increasing-tail-u) (inl i) (inl j) j≤i = + reverses-order-is-increasing-fin-sequence-type-Poset + ( succ-ℕ n) + ( tail-fin-sequence (succ-ℕ n) u) + ( increasing-tail-u) + ( i) + ( j) + ( j≤i) + + is-increasing-reverses-order-fin-sequence-type-Poset : + (n : ℕ) (u : fin-sequence (type-Poset P) n) → + preserves-order-Poset (opposite-Poset (Fin-Poset n)) P u → + is-increasing-fin-sequence-type-Poset P n u + is-increasing-reverses-order-fin-sequence-type-Poset 0 u H = raise-star + is-increasing-reverses-order-fin-sequence-type-Poset 1 u H = raise-star + is-increasing-reverses-order-fin-sequence-type-Poset + (succ-ℕ (succ-ℕ n)) u H = + ( H (inr star) (neg-two-Fin (succ-ℕ n)) star , + is-increasing-reverses-order-fin-sequence-type-Poset + ( succ-ℕ n) + ( tail-fin-sequence (succ-ℕ n) u) + ( λ i j → H (inl i) (inl j))) + + reverses-order-iff-is-increasing-fin-sequence-type-Poset : + (n : ℕ) (u : fin-sequence (type-Poset P) n) → + is-increasing-fin-sequence-type-Poset P n u ↔ + preserves-order-Poset (opposite-Poset (Fin-Poset n)) P u + reverses-order-iff-is-increasing-fin-sequence-type-Poset n u = + ( reverses-order-is-increasing-fin-sequence-type-Poset n u , + is-increasing-reverses-order-fin-sequence-type-Poset n u) + + reverses-order-increasing-fin-sequence-type-Poset : + (n : ℕ) (u : increasing-fin-sequence-type-Poset P n) → + preserves-order-Poset + ( opposite-Poset (Fin-Poset n)) + ( P) + ( fin-sequence-increasing-fin-sequence-type-Poset P n u) + reverses-order-increasing-fin-sequence-type-Poset n = + ind-Σ (reverses-order-is-increasing-fin-sequence-type-Poset n) +``` diff --git a/src/order-theory/increasing-nonempty-arrays-posets.lagda.md b/src/order-theory/increasing-nonempty-arrays-posets.lagda.md new file mode 100644 index 00000000000..cdedaf52be3 --- /dev/null +++ b/src/order-theory/increasing-nonempty-arrays-posets.lagda.md @@ -0,0 +1,235 @@ +# Increasing nonempty arrays in posets + +```agda +module order-theory.increasing-nonempty-arrays-posets where +``` + +
Imports + +```agda +open import elementary-number-theory.inequality-standard-finite-types +open import elementary-number-theory.natural-numbers + +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.subtypes +open import foundation.unit-type +open import foundation.universe-levels + +open import lists.arrays +open import lists.finite-sequences +open import lists.nonempty-arrays + +open import order-theory.increasing-arrays-posets +open import order-theory.increasing-finite-sequences-posets +open import order-theory.opposite-posets +open import order-theory.order-preserving-maps-posets +open import order-theory.posets + +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +A [nonempty array](lists.nonempty-arrays.md) in a +[poset](order-theory.posets.md) is +{{#concept "increasing" Disambiguation="nonempty array in a poset" Agda=is-increasing-nonempty-array-type-Poset}} +if its associated [finite sequence](lists.finite-sequences.md) is +[increasing](order-theory.increasing-finite-sequences-posets.md). + +## Definition + +```agda +module _ + {l1 l2 : Level} + (P : Poset l1 l2) + where + + is-increasing-prop-nonempty-array-type-Poset : + subtype l2 (nonempty-array (type-Poset P)) + is-increasing-prop-nonempty-array-type-Poset (u , _) = + is-increasing-prop-array-type-Poset P u + + is-increasing-nonempty-array-type-Poset : + nonempty-array (type-Poset P) → UU l2 + is-increasing-nonempty-array-type-Poset = + is-in-subtype is-increasing-prop-nonempty-array-type-Poset + + increasing-nonempty-array-type-Poset : UU (l1 ⊔ l2) + increasing-nonempty-array-type-Poset = + type-subtype is-increasing-prop-nonempty-array-type-Poset + +module _ + {l1 l2 : Level} + (P : Poset l1 l2) + where + + nonempty-array-increasing-nonempty-array-type-Poset : + increasing-nonempty-array-type-Poset P → nonempty-array (type-Poset P) + nonempty-array-increasing-nonempty-array-type-Poset = pr1 + + is-increasing-nonempty-array-increasing-nonempty-array-type-Poset : + (u : increasing-nonempty-array-type-Poset P) → + is-increasing-nonempty-array-type-Poset + ( P) + ( nonempty-array-increasing-nonempty-array-type-Poset u) + is-increasing-nonempty-array-increasing-nonempty-array-type-Poset = pr2 + + array-increasing-nonempty-array-type-Poset : + increasing-nonempty-array-type-Poset P → array (type-Poset P) + array-increasing-nonempty-array-type-Poset ((u , _) , _) = u + + length-increasing-nonempty-array-type-Poset : + increasing-nonempty-array-type-Poset P → ℕ + length-increasing-nonempty-array-type-Poset (((n , _) , _) , _) = n + + head-increasing-nonempty-array-type-Poset : + increasing-nonempty-array-type-Poset P → type-Poset P + head-increasing-nonempty-array-type-Poset = + head-nonempty-array ∘ nonempty-array-increasing-nonempty-array-type-Poset + + last-increasing-nonempty-array-type-Poset : + increasing-nonempty-array-type-Poset P → type-Poset P + last-increasing-nonempty-array-type-Poset = + last-nonempty-array ∘ nonempty-array-increasing-nonempty-array-type-Poset + + fin-sequence-increasing-nonempty-array-type-Poset : + (u : increasing-nonempty-array-type-Poset P) → + fin-sequence (type-Poset P) (length-increasing-nonempty-array-type-Poset u) + fin-sequence-increasing-nonempty-array-type-Poset (((_ , u) , _) , _) = u +``` + +## Properties + +### The tail of an increasing nonempty array is increasing + +```agda +module _ + {l1 l2 : Level} + (P : Poset l1 l2) + where + + array-tail-increasing-nonempty-array-type-Poset : + increasing-nonempty-array-type-Poset P → array (type-Poset P) + array-tail-increasing-nonempty-array-type-Poset (u , _) = + tail-nonempty-array u + + abstract + is-increasing-array-tail-increasing-nonempty-array-type-Poset : + (u : increasing-nonempty-array-type-Poset P) → + is-increasing-array-type-Poset + ( P) + ( array-tail-increasing-nonempty-array-type-Poset u) + is-increasing-array-tail-increasing-nonempty-array-type-Poset + (((1 , _) , _) , _) = + raise-star + is-increasing-array-tail-increasing-nonempty-array-type-Poset + (((succ-ℕ (succ-ℕ n) , _) , _) , _ , is-increasing-u-tail) = + is-increasing-u-tail + + tail-increasing-nonempty-array-type-Poset : + increasing-nonempty-array-type-Poset P → increasing-array-type-Poset P + tail-increasing-nonempty-array-type-Poset + uu@(((succ-ℕ n , u) , _) , is-increasing-u) = + ( (n , tail-fin-sequence n u) , + is-increasing-array-tail-increasing-nonempty-array-type-Poset uu) +``` + +### The initial segment of an increasing nonempty array is increasing + +```agda +module _ + {l1 l2 : Level} + (P : Poset l1 l2) + where + + array-init-increasing-nonempty-array-type-Poset : + increasing-nonempty-array-type-Poset P → array (type-Poset P) + array-init-increasing-nonempty-array-type-Poset (u , _) = + init-nonempty-array u + + abstract + is-increasing-array-init-increasing-nonempty-array-type-Poset : + (u : increasing-nonempty-array-type-Poset P) → + is-increasing-array-type-Poset + ( P) + ( array-init-increasing-nonempty-array-type-Poset u) + is-increasing-array-init-increasing-nonempty-array-type-Poset + (((succ-ℕ n , u) , _) , H) = + is-increasing-reverses-order-fin-sequence-type-Poset + ( P) + ( n) + ( u ∘ skip-zero-Fin n) + ( preserves-order-comp-Poset + ( opposite-Poset (Fin-Poset n)) + ( opposite-Poset (Fin-Poset (succ-ℕ n))) + ( P) + ( u , + reverses-order-is-increasing-fin-sequence-type-Poset + ( P) + ( succ-ℕ n) + ( u) + ( H)) + ( skip-zero-Fin n , + λ i j → preserves-order-skip-zero-Fin n j i)) + + init-increasing-nonempty-array-type-Poset : + increasing-nonempty-array-type-Poset P → increasing-array-type-Poset P + init-increasing-nonempty-array-type-Poset u = + ( array-init-increasing-nonempty-array-type-Poset u , + is-increasing-array-init-increasing-nonempty-array-type-Poset u) +``` + +### The head of a nonempty array is its least element + +```agda +module _ + {l1 l2 : Level} + (P : Poset l1 l2) + where + + abstract + is-least-element-head-increasing-nonempty-array-type-Poset : + (u : increasing-nonempty-array-type-Poset P) + (i : Fin (length-increasing-nonempty-array-type-Poset P u)) → + leq-Poset P + ( head-increasing-nonempty-array-type-Poset P u) + ( fin-sequence-increasing-nonempty-array-type-Poset P u i) + is-least-element-head-increasing-nonempty-array-type-Poset + (((succ-ℕ n , u) , _) , H) i = + reverses-order-increasing-fin-sequence-type-Poset + ( P) + ( succ-ℕ n) + ( u , H) + ( neg-one-Fin n) + ( i) + ( star) +``` + +### The last element of a nonempty array is its greatest element + +```agda +module _ + {l1 l2 : Level} + (P : Poset l1 l2) + where + + abstract + is-greatest-element-last-increasing-nonempty-array-type-Poset : + (u : increasing-nonempty-array-type-Poset P) + (i : Fin (length-increasing-nonempty-array-type-Poset P u)) → + leq-Poset P + ( fin-sequence-increasing-nonempty-array-type-Poset P u i) + ( last-increasing-nonempty-array-type-Poset P u) + is-greatest-element-last-increasing-nonempty-array-type-Poset + (((succ-ℕ n , u) , _) , H) i = + reverses-order-increasing-fin-sequence-type-Poset + ( P) + ( succ-ℕ n) + ( u , H) + ( i) + ( zero-Fin n) + ( leq-zero-Fin n i) +``` diff --git a/src/univalent-combinatorics/standard-finite-types.lagda.md b/src/univalent-combinatorics/standard-finite-types.lagda.md index 95b5d6686ca..c683359f921 100644 --- a/src/univalent-combinatorics/standard-finite-types.lagda.md +++ b/src/univalent-combinatorics/standard-finite-types.lagda.md @@ -535,6 +535,16 @@ is-inhabited-or-empty-Fin n = is-inhabited-or-empty-is-decidable (is-decidable-Fin n) ``` +### `nat-Fin-reverse (succ-ℕ n)` maps `zero-Fin n` to `n` + +```agda +abstract + nat-reverse-zero-Fin : + (n : ℕ) → nat-Fin-reverse (succ-ℕ n) (zero-Fin n) ＝ n + nat-reverse-zero-Fin zero-ℕ = refl + nat-reverse-zero-Fin (succ-ℕ n) = ap succ-ℕ (nat-reverse-zero-Fin n) +``` + ## See also - [Classical finite types](univalent-combinatorics.classical-finite-types.md), From 55b7bd49a0eea1579a33a769717a57737b0fd06e Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Tue, 21 Apr 2026 18:30:38 -0700 Subject: [PATCH 02/14] simplify --- .../inequality-standard-finite-types.lagda.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md index efc5ec52d5c..55bbfd34e6f 100644 --- a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md +++ b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md @@ -201,7 +201,6 @@ abstract abstract leq-zero-Fin : (n : ℕ) (i : Fin (succ-ℕ n)) → leq-Fin (succ-ℕ n) (zero-Fin n) i - leq-zero-Fin 0 (inr star) = star + leq-zero-Fin n (inr star) = star leq-zero-Fin (succ-ℕ n) (inl i) = leq-zero-Fin n i - leq-zero-Fin (succ-ℕ n) (inr star) = star ``` From 8831c60596b5aa184b07a3926719307549ea35d8 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 23 Apr 2026 16:56:46 -0700 Subject: [PATCH 03/14] Fix link --- src/order-theory/increasing-finite-sequences-posets.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/order-theory/increasing-finite-sequences-posets.lagda.md b/src/order-theory/increasing-finite-sequences-posets.lagda.md index 453288fbd86..c23c58800aa 100644 --- a/src/order-theory/increasing-finite-sequences-posets.lagda.md +++ b/src/order-theory/increasing-finite-sequences-posets.lagda.md @@ -35,7 +35,7 @@ open import univalent-combinatorics.standard-finite-types A [finite sequence](lists.finite-sequences.md) of elements of a [poset](order-theory.posets.md) is -{{#concept "increasing" Disambiguation="finite sequence in a poset" Agda=is-increasing-fin-sequence-Poset}} +{{#concept "increasing" Disambiguation="finite sequence in a poset" Agda=is-increasing-fin-sequence-type-Poset}} if each element is less than or equal to the next. ## Definition From 60f06c811d641a3e674b8e02629bfce8b224d8e8 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 23 Apr 2026 17:03:13 -0700 Subject: [PATCH 04/14] Progress --- src/lists.lagda.md | 1 + ...cessive-elements-finite-sequences.lagda.md | 80 +++++ ...ncreasing-finite-sequences-posets.lagda.md | 58 ++++ src/real-numbers.lagda.md | 1 + .../closed-intervals-real-numbers.lagda.md | 14 + ...ons-closed-intervals-real-numbers.lagda.md | 327 ++++++++++++++++++ 6 files changed, 481 insertions(+) create mode 100644 src/lists/pairs-of-successive-elements-finite-sequences.lagda.md create mode 100644 src/real-numbers/partitions-closed-intervals-real-numbers.lagda.md diff --git a/src/lists.lagda.md b/src/lists.lagda.md index 94c6cd5f2c6..2da735a87bc 100644 --- a/src/lists.lagda.md +++ b/src/lists.lagda.md @@ -20,6 +20,7 @@ open import lists.functoriality-tuples-finite-sequences public open import lists.lists public open import lists.lists-discrete-types public open import lists.nonempty-arrays public +open import lists.pairs-of-successive-elements-finite-sequences public open import lists.partial-sequences public open import lists.permutation-lists public open import lists.permutation-tuples public diff --git a/src/lists/pairs-of-successive-elements-finite-sequences.lagda.md b/src/lists/pairs-of-successive-elements-finite-sequences.lagda.md new file mode 100644 index 00000000000..f6a1caa0e8c --- /dev/null +++ b/src/lists/pairs-of-successive-elements-finite-sequences.lagda.md @@ -0,0 +1,80 @@ +# Pairs of successive elements in a finite sequence + +```agda +module lists.pairs-of-successive-elements-finite-sequences where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.cartesian-product-types +open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.function-extensionality +open import foundation.homotopies +open import foundation.identity-types +open import foundation.unit-type +open import foundation.universe-levels + +open import lists.finite-sequences + +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +Given a nonempty [finite sequence](lists.finite-sequences.md) `a` with elements +`a₀, a₁, ..., aₙ`, the +{{#concept "sequence of pairs of successive elements" Agda=pair-succ-fin-sequence}} +of `a` is the the sequence `(a₀, a₁), (a₁, a₂), ..., (aₙ₋₁, aₙ)`. + +## Definition + +```agda +pair-succ-fin-sequence : + {l : Level} {A : UU l} (n : ℕ) → + fin-sequence A (succ-ℕ n) → fin-sequence (A × A) n +pair-succ-fin-sequence (succ-ℕ n) a = + cons-fin-sequence + ( n) + ( head-fin-sequence (succ-ℕ n) a , + head-fin-sequence n (tail-fin-sequence (succ-ℕ n) a)) + ( pair-succ-fin-sequence n (tail-fin-sequence (succ-ℕ n) a)) + +pair-succ-fin-sequence' : + {l : Level} {A : UU l} (n : ℕ) → + fin-sequence A (succ-ℕ n) → fin-sequence (A × A) n +pair-succ-fin-sequence' n a i = + ( a (skip-zero-Fin n i) , + a (inl-Fin n i)) +``` + +## Properties + +### The two definitions of the sequence of pairs of successive elements are homotopic + +```agda +abstract + htpy-pair-succ-fin-sequence' : + {l : Level} {A : UU l} (n : ℕ) (a : fin-sequence A (succ-ℕ n)) → + pair-succ-fin-sequence n a ~ pair-succ-fin-sequence' n a + htpy-pair-succ-fin-sequence' (succ-ℕ n) a (inl i) = + htpy-pair-succ-fin-sequence' n (tail-fin-sequence (succ-ℕ n) a) i + htpy-pair-succ-fin-sequence' (succ-ℕ n) a (inr star) = + refl +``` + +### The two definitions of the sequence of pairs of successive elements are equal + +```agda +abstract + eq-pair-succ-fin-sequence' : + {l : Level} {A : UU l} (n : ℕ) (a : fin-sequence A (succ-ℕ n)) → + pair-succ-fin-sequence n a ＝ pair-succ-fin-sequence' n a + eq-pair-succ-fin-sequence' n a = + eq-htpy (htpy-pair-succ-fin-sequence' n a) +``` diff --git a/src/order-theory/increasing-finite-sequences-posets.lagda.md b/src/order-theory/increasing-finite-sequences-posets.lagda.md index c23c58800aa..6e3aa7ebca1 100644 --- a/src/order-theory/increasing-finite-sequences-posets.lagda.md +++ b/src/order-theory/increasing-finite-sequences-posets.lagda.md @@ -14,6 +14,8 @@ open import foundation.conjunction open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types open import foundation.logical-equivalences open import foundation.propositions open import foundation.subtypes @@ -21,7 +23,9 @@ open import foundation.unit-type open import foundation.universe-levels open import lists.finite-sequences +open import lists.pairs-of-successive-elements-finite-sequences +open import order-theory.closed-intervals-posets open import order-theory.opposite-posets open import order-theory.order-preserving-maps-posets open import order-theory.posets @@ -171,3 +175,57 @@ module _ reverses-order-increasing-fin-sequence-type-Poset n = ind-Σ (reverses-order-is-increasing-fin-sequence-type-Poset n) ``` + +### Given an increasing sequence `a₁ ≤ a₂ ≤ ... ≤ aₙ`, the sequence of intervals `[a₁, a₂], [a₂, a₃], ..., [aₙ₋₁, aₙ]` + +```agda +module _ + {l1 l2 : Level} + (P : Poset l1 l2) + where + + closed-intervals-increasing-fin-sequence-type-Poset : + (n : ℕ) → increasing-fin-sequence-type-Poset P (succ-ℕ n) → + fin-sequence (closed-interval-Poset P) n + closed-intervals-increasing-fin-sequence-type-Poset + ( succ-ℕ n) + ( u , u₁≤u₂ , is-increasing-tail-u) = + cons-fin-sequence + ( n) + ( ( head-fin-sequence (succ-ℕ n) u , + head-fin-sequence n (tail-fin-sequence (succ-ℕ n) u)) , + u₁≤u₂) + ( closed-intervals-increasing-fin-sequence-type-Poset + ( n) + ( tail-fin-sequence (succ-ℕ n) u , is-increasing-tail-u)) + + closed-intervals-increasing-fin-sequence-type-Poset' : + (n : ℕ) → increasing-fin-sequence-type-Poset P (succ-ℕ n) → + fin-sequence (closed-interval-Poset P) n + closed-intervals-increasing-fin-sequence-type-Poset' n (u , H) i = + ( pair-succ-fin-sequence' n u i , + reverses-order-is-increasing-fin-sequence-type-Poset P + ( succ-ℕ n) + ( u) + ( H) + ( skip-zero-Fin n i) + ( inl-Fin n i) + ( leq-succ-Fin n i)) + + abstract + htpy-closed-intervals-increasing-fin-sequence-type-Poset' : + (n : ℕ) (u : increasing-fin-sequence-type-Poset P (succ-ℕ n)) → + closed-intervals-increasing-fin-sequence-type-Poset n u ~ + closed-intervals-increasing-fin-sequence-type-Poset' n u + htpy-closed-intervals-increasing-fin-sequence-type-Poset' + (succ-ℕ n) (u , _ , H) (inl i) = + htpy-closed-intervals-increasing-fin-sequence-type-Poset' + ( n) + ( tail-fin-sequence (succ-ℕ n) u , H) + ( i) + htpy-closed-intervals-increasing-fin-sequence-type-Poset' + (succ-ℕ n) (u , _ , _) (inr star) = + eq-type-subtype + ( ind-Σ (leq-prop-Poset P)) + ( refl) +``` diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index 94ce16971ee..c6767f75a7a 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -106,6 +106,7 @@ open import real-numbers.nonpositive-real-numbers public open import real-numbers.nonzero-real-numbers public open import real-numbers.nonzero-roots-nonnegative-real-numbers public open import real-numbers.odd-roots-real-numbers public +open import real-numbers.partitions-closed-intervals-real-numbers public open import real-numbers.pointwise-continuous-endomaps-real-numbers public open import real-numbers.pointwise-epsilon-delta-continuous-endomaps-real-numbers public open import real-numbers.positive-and-negative-real-numbers public diff --git a/src/real-numbers/closed-intervals-real-numbers.lagda.md b/src/real-numbers/closed-intervals-real-numbers.lagda.md index 4e2bf491329..8edf2071209 100644 --- a/src/real-numbers/closed-intervals-real-numbers.lagda.md +++ b/src/real-numbers/closed-intervals-real-numbers.lagda.md @@ -14,6 +14,7 @@ open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.positive-rational-numbers open import foundation.dependent-pair-types +open import foundation.function-types open import foundation.logical-equivalences open import foundation.propositional-truncations open import foundation.propositions @@ -38,6 +39,7 @@ open import real-numbers.dedekind-real-numbers open import real-numbers.inequalities-addition-and-subtraction-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.metric-space-of-real-numbers +open import real-numbers.nonnegative-real-numbers open import real-numbers.rational-real-numbers open import real-numbers.short-map-binary-maximum-real-numbers open import real-numbers.short-map-binary-minimum-real-numbers @@ -91,6 +93,18 @@ upper-bound-closed-interval-ℝ = ## Properties +### The width of a closed interval + +```agda +nonnegative-width-closed-interval-ℝ : + {l1 l2 : Level} → closed-interval-ℝ l1 l2 → ℝ⁰⁺ (l1 ⊔ l2) +nonnegative-width-closed-interval-ℝ (_ , a≤b) = nonnegative-diff-leq-ℝ a≤b + +width-closed-interval-ℝ : + {l1 l2 : Level} → closed-interval-ℝ l1 l2 → ℝ (l1 ⊔ l2) +width-closed-interval-ℝ = real-ℝ⁰⁺ ∘ nonnegative-width-closed-interval-ℝ +``` + ### Closed intervals in the real numbers are closed in the metric space of real numbers ```agda diff --git a/src/real-numbers/partitions-closed-intervals-real-numbers.lagda.md b/src/real-numbers/partitions-closed-intervals-real-numbers.lagda.md new file mode 100644 index 00000000000..252f62f8610 --- /dev/null +++ b/src/real-numbers/partitions-closed-intervals-real-numbers.lagda.md @@ -0,0 +1,327 @@ +# Partitions of closed intervals of real numbers + +```agda +module real-numbers.partitions-closed-intervals-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.inequality-standard-finite-types +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-functions +open import foundation.binary-transport +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.unit-type +open import foundation.universe-levels + +open import lists.finite-sequences +open import lists.tuples + +open import order-theory.increasing-arrays-posets +open import order-theory.increasing-finite-sequences-posets +open import order-theory.increasing-nonempty-arrays-posets +open import order-theory.large-posets +open import order-theory.least-upper-bounds-large-posets +open import order-theory.lower-bounds-large-posets +open import order-theory.opposite-posets +open import order-theory.order-preserving-maps-posets +open import order-theory.upper-bounds-large-posets + +open import real-numbers.addition-real-numbers +open import real-numbers.closed-intervals-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.difference-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers +open import real-numbers.inequality-nonnegative-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.maximum-finite-families-nonnegative-real-numbers +open import real-numbers.multiplication-nonnegative-real-numbers +open import real-numbers.multiplication-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.similarity-real-numbers + +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +A +{{#concept "partition" Disambiguation="of a closed interval in ℝ" Agda=partition-closed-interval-ℝ}} +of a [closed interval](real-numbers.closed-intervals-real-numbers.md) `[a, b]` +in the [real numbers](real-numbers.dedekind-real-numbers.md) is an +[increasing nonempty array](order-theory.increasing-nonempty-arrays-posets.md) +in `ℝ` whose first element is `a` and whose last element is `b`. + +## Definition + +```agda +module _ + {l : Level} + ([a,b]@((a , b) , a≤b) : closed-interval-ℝ l l) + where + + partition-closed-interval-ℝ : UU (lsuc l) + partition-closed-interval-ℝ = + Σ ( increasing-nonempty-array-type-Poset (ℝ-Poset l)) + ( λ u → + ( head-increasing-nonempty-array-type-Poset (ℝ-Poset l) u ＝ a) × + ( last-increasing-nonempty-array-type-Poset (ℝ-Poset l) u ＝ b)) + + pred-length-partition-closed-interval-ℝ : + partition-closed-interval-ℝ → ℕ + pred-length-partition-closed-interval-ℝ ((((succ-ℕ n , _) , _) , _) , _) = + n + + length-partition-closed-interval-ℝ : + partition-closed-interval-ℝ → ℕ + length-partition-closed-interval-ℝ = + succ-ℕ ∘ pred-length-partition-closed-interval-ℝ + + real-fin-sequence-partition-closed-interval-ℝ : + (p : partition-closed-interval-ℝ) → + fin-sequence (ℝ l) (length-partition-closed-interval-ℝ p) + real-fin-sequence-partition-closed-interval-ℝ + ((((succ-ℕ n , u) , _) , _) , _) = u + + is-increasing-real-fin-sequence-partition-closed-interval-ℝ : + (p : partition-closed-interval-ℝ) → + is-increasing-fin-sequence-type-Poset + ( ℝ-Poset l) + ( length-partition-closed-interval-ℝ p) + ( real-fin-sequence-partition-closed-interval-ℝ p) + is-increasing-real-fin-sequence-partition-closed-interval-ℝ + ((((succ-ℕ n , u) , _) , H) , _) = + H + + increasing-real-fin-sequence-partition-closed-interval-ℝ : + (p : partition-closed-interval-ℝ) → + increasing-fin-sequence-type-Poset + ( ℝ-Poset l) + ( length-partition-closed-interval-ℝ p) + increasing-real-fin-sequence-partition-closed-interval-ℝ + ((((succ-ℕ n , u) , _) , H) , _) = + ( u , H) + + abstract + reverses-order-fin-sequence-partition-closed-interval-ℝ : + (p : partition-closed-interval-ℝ) → + preserves-order-Poset + ( opposite-Poset (Fin-Poset (length-partition-closed-interval-ℝ p))) + ( ℝ-Poset l) + ( real-fin-sequence-partition-closed-interval-ℝ p) + reverses-order-fin-sequence-partition-closed-interval-ℝ + ((((succ-ℕ n , u) , _) , H) , _) = + reverses-order-is-increasing-fin-sequence-type-Poset + ( ℝ-Poset l) + ( succ-ℕ n) + ( u) + ( H) + + eq-lower-bound-head-real-fin-sequence-partition-closed-interval-ℝ : + (p : partition-closed-interval-ℝ) → + head-fin-sequence + ( pred-length-partition-closed-interval-ℝ p) + ( real-fin-sequence-partition-closed-interval-ℝ p) ＝ + a + eq-lower-bound-head-real-fin-sequence-partition-closed-interval-ℝ + ((((succ-ℕ n , u) , _) , _) , u₋₁=a , _) = + u₋₁=a + + eq-upper-bound-last-real-fin-sequence-partition-closed-interval-ℝ : + (p : partition-closed-interval-ℝ) → + last-fin-sequence + ( pred-length-partition-closed-interval-ℝ p) + ( real-fin-sequence-partition-closed-interval-ℝ p) ＝ + b + eq-upper-bound-last-real-fin-sequence-partition-closed-interval-ℝ + ((((succ-ℕ n , u) , _) , _) , _ , u₀=b) = + u₀=b + + abstract + lower-bound-real-fin-sequence-partition-closed-interval-ℝ : + (p : partition-closed-interval-ℝ) → + is-lower-bound-family-of-elements-Large-Poset + ( ℝ-Large-Poset) + ( real-fin-sequence-partition-closed-interval-ℝ p) + ( a) + lower-bound-real-fin-sequence-partition-closed-interval-ℝ p i = + binary-tr + ( leq-ℝ) + ( eq-lower-bound-head-real-fin-sequence-partition-closed-interval-ℝ p) + ( refl) + ( reverses-order-fin-sequence-partition-closed-interval-ℝ + ( p) + ( neg-one-Fin (pred-length-partition-closed-interval-ℝ p)) + ( i) + ( leq-neg-one-Fin (pred-length-partition-closed-interval-ℝ p) i)) + + upper-bound-real-fin-sequence-partition-closed-interval-ℝ : + (p : partition-closed-interval-ℝ) → + is-upper-bound-family-of-elements-Large-Poset + ( ℝ-Large-Poset) + ( real-fin-sequence-partition-closed-interval-ℝ p) + ( b) + upper-bound-real-fin-sequence-partition-closed-interval-ℝ p i = + binary-tr + ( leq-ℝ) + ( refl) + ( eq-upper-bound-last-real-fin-sequence-partition-closed-interval-ℝ p) + ( reverses-order-fin-sequence-partition-closed-interval-ℝ + ( p) + ( i) + ( zero-Fin (pred-length-partition-closed-interval-ℝ p)) + ( leq-zero-Fin (pred-length-partition-closed-interval-ℝ p) i)) + + fin-sequence-partition-closed-interval-ℝ : + (p : partition-closed-interval-ℝ) → + fin-sequence + ( type-closed-interval-ℝ l [a,b]) + ( length-partition-closed-interval-ℝ p) + fin-sequence-partition-closed-interval-ℝ p i = + ( real-fin-sequence-partition-closed-interval-ℝ p i , + lower-bound-real-fin-sequence-partition-closed-interval-ℝ p i , + upper-bound-real-fin-sequence-partition-closed-interval-ℝ p i) +``` + +## Properties + +### The sequence of closed intervals of a partition + +```agda +fin-sequence-closed-interval-partition-closed-interval-ℝ : + {l : Level} ([a,b] : closed-interval-ℝ l l) + (p : partition-closed-interval-ℝ [a,b]) → + fin-sequence + ( closed-interval-ℝ l l) + ( pred-length-partition-closed-interval-ℝ [a,b] p) +fin-sequence-closed-interval-partition-closed-interval-ℝ {l} [a,b] p = + closed-intervals-increasing-fin-sequence-type-Poset + ( ℝ-Poset l) + ( pred-length-partition-closed-interval-ℝ [a,b] p) + ( increasing-real-fin-sequence-partition-closed-interval-ℝ [a,b] p) +``` + +### The mesh of a partition + +```agda +module _ + {l : Level} + ([a,b] : closed-interval-ℝ l l) + where + + diffs-partition-closed-interval-ℝ : + (p : partition-closed-interval-ℝ [a,b]) → + fin-sequence + ( ℝ⁰⁺ l) + ( pred-length-partition-closed-interval-ℝ [a,b] p) + diffs-partition-closed-interval-ℝ p = + ( nonnegative-width-closed-interval-ℝ) ∘ + ( fin-sequence-closed-interval-partition-closed-interval-ℝ [a,b] p) + + mesh-partition-closed-interval-ℝ : + partition-closed-interval-ℝ [a,b] → ℝ⁰⁺ l + mesh-partition-closed-interval-ℝ p = + max-fin-sequence-ℝ⁰⁺ + ( pred-length-partition-closed-interval-ℝ [a,b] p) + ( diffs-partition-closed-interval-ℝ p) + + real-mesh-partition-closed-interval-ℝ : + partition-closed-interval-ℝ [a,b] → ℝ l + real-mesh-partition-closed-interval-ℝ = + real-ℝ⁰⁺ ∘ mesh-partition-closed-interval-ℝ +``` + +### The mesh of a partition of a closed interval is at most the width of the interval + +```agda +module _ + {l : Level} + ([a,b]@((a , b) , a≤b) : closed-interval-ℝ l l) + where + + abstract + bound-diffs-partition-closed-interval-ℝ : + (p : partition-closed-interval-ℝ [a,b]) → + is-upper-bound-family-of-elements-Large-Poset + ( large-poset-ℝ⁰⁺) + ( diffs-partition-closed-interval-ℝ [a,b] p) + ( nonnegative-width-closed-interval-ℝ [a,b]) + bound-diffs-partition-closed-interval-ℝ + p@((((succ-ℕ n , u) , _) , _) , _) i = + let + open inequality-reasoning-Large-Poset ℝ-Large-Poset + in + chain-of-inequalities + real-ℝ⁰⁺ (diffs-partition-closed-interval-ℝ [a,b] p i) + ≤ u (inl-Fin n i) -ℝ u (skip-zero-Fin n i) + by + leq-eq-ℝ + ( ap + ( width-closed-interval-ℝ) + ( htpy-closed-intervals-increasing-fin-sequence-type-Poset' + ( ℝ-Poset l) + ( pred-length-partition-closed-interval-ℝ [a,b] p) + ( increasing-real-fin-sequence-partition-closed-interval-ℝ + ( [a,b]) + ( p)) + ( i))) + ≤ b -ℝ u (skip-zero-Fin n i) + by + preserves-leq-right-add-ℝ _ _ _ + ( upper-bound-real-fin-sequence-partition-closed-interval-ℝ + ( [a,b]) + ( p) + ( inl-Fin n i)) + ≤ b -ℝ a + by + reverses-leq-left-diff-ℝ _ + ( lower-bound-real-fin-sequence-partition-closed-interval-ℝ + ( [a,b]) + ( p) + ( skip-zero-Fin n i)) + + bound-mesh-partition-closed-interval-ℝ : + (p : partition-closed-interval-ℝ [a,b]) → + leq-ℝ⁰⁺ + ( mesh-partition-closed-interval-ℝ [a,b] p) + ( nonnegative-width-closed-interval-ℝ [a,b]) + bound-mesh-partition-closed-interval-ℝ p = + forward-implication + ( is-least-upper-bound-max-fin-sequence-ℝ⁰⁺ + ( pred-length-partition-closed-interval-ℝ [a,b] p) + ( diffs-partition-closed-interval-ℝ [a,b] p) + ( nonnegative-width-closed-interval-ℝ [a,b])) + ( bound-diffs-partition-closed-interval-ℝ p) +``` + +### The trivial partition of a closed interval + +```agda +module _ + {l : Level} + ([a,b]@((a , b) , a≤b) : closed-interval-ℝ l l) + where + + trivial-partition-closed-interval-ℝ : + partition-closed-interval-ℝ [a,b] + trivial-partition-closed-interval-ℝ = + ( ( ((2 , component-tuple 2 (a ∷ b ∷ empty-tuple)) , star) , + a≤b , + raise-star) , + refl , + refl) +``` + +## External links + +- [Partition of an interval](https://en.wikipedia.org/wiki/Partition_of_an_interval) + on Wikipedia From 09b44f5becab9f4aca4d54b05481c614cab6915d Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 30 Apr 2026 17:00:45 -0700 Subject: [PATCH 05/14] Progress --- .../inequality-standard-finite-types.lagda.md | 10 +- ...ncreasing-finite-sequences-posets.lagda.md | 126 ++++++++---------- ...increasing-nonempty-arrays-posets.lagda.md | 59 +++----- .../standard-finite-types.lagda.md | 3 +- 4 files changed, 77 insertions(+), 121 deletions(-) diff --git a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md index 55bbfd34e6f..4f14975dd91 100644 --- a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md +++ b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md @@ -186,13 +186,13 @@ linear-leq-Fin (succ-ℕ k) (inr x) y = inr star ```agda abstract - preserves-order-skip-zero-Fin : + preserves-order-inr-Fin : (n : ℕ) → preserves-order-Poset (Fin-Poset n) (Fin-Poset (succ-ℕ n)) (skip-zero-Fin n) - preserves-order-skip-zero-Fin (succ-ℕ n) (inl x) (inl y) x≤y = - preserves-order-skip-zero-Fin n x y x≤y - preserves-order-skip-zero-Fin (succ-ℕ n) (inl x) (inr star) _ = star - preserves-order-skip-zero-Fin (succ-ℕ n) (inr x) (inr star) _ = star + preserves-order-inr-Fin (succ-ℕ n) (inl x) (inl y) x≤y = + preserves-order-inr-Fin n x y x≤y + preserves-order-inr-Fin (succ-ℕ n) (inl x) (inr star) _ = star + preserves-order-inr-Fin (succ-ℕ n) (inr x) (inr star) _ = star ``` ### `zero-Fin n` is the least element of `Fin (succ-ℕ n)` diff --git a/src/order-theory/increasing-finite-sequences-posets.lagda.md b/src/order-theory/increasing-finite-sequences-posets.lagda.md index c23c58800aa..848b95695f3 100644 --- a/src/order-theory/increasing-finite-sequences-posets.lagda.md +++ b/src/order-theory/increasing-finite-sequences-posets.lagda.md @@ -48,16 +48,8 @@ module _ is-increasing-prop-fin-sequence-type-Poset : (n : ℕ) → subtype l2 (fin-sequence (type-Poset P) n) - is-increasing-prop-fin-sequence-type-Poset 0 _ = raise-unit-Prop l2 - is-increasing-prop-fin-sequence-type-Poset 1 _ = raise-unit-Prop l2 - is-increasing-prop-fin-sequence-type-Poset (succ-ℕ (succ-ℕ n)) u = - ( leq-prop-Poset - ( P) - ( u (neg-one-Fin (succ-ℕ n))) - ( u (neg-two-Fin (succ-ℕ n)))) ∧ - ( is-increasing-prop-fin-sequence-type-Poset - ( succ-ℕ n) - ( tail-fin-sequence (succ-ℕ n) u)) + is-increasing-prop-fin-sequence-type-Poset n = + preserves-order-prop-Poset (Fin-Poset n) P is-increasing-fin-sequence-type-Poset : (n : ℕ) → fin-sequence (type-Poset P) n → UU l2 @@ -89,17 +81,7 @@ module _ ## Properties -### A finite sequence in a poset `P` is increasing if and only if it is an order-reversing map from `Fin n` to `P` - -The -[standard ordering](elementary-number-theory.inequality-standard-finite-types.md) -on the [standard finite types](univalent-combinatorics.standard-finite-types.md) -defines `neg-one-Fin n` as the greatest element of `Fin (succ-ℕ n)`, but finite -sequences use `neg-one-Fin n` as the head, which is conventionally the first -element of the sequence. - -We choose to adopt the convention that the head of an increasing sequence is its -least element, requiring us to reverse the order of `Fin n`. +### A finite sequence `a₁, ..., aₙ` is increasing if and only if `a₁ ≤ a₂ ∧ a₂ ≤ a₃ ∧ ... ∧ aₙ₋₁ ≤ aₙ` ```agda module _ @@ -107,67 +89,67 @@ module _ (P : Poset l1 l2) where + is-increasing-leq-next-prop-fin-sequence-type-Poset : + (n : ℕ) → subtype l2 (fin-sequence (type-Poset P) n) + is-increasing-leq-next-prop-fin-sequence-type-Poset 0 _ = raise-unit-Prop l2 + is-increasing-leq-next-prop-fin-sequence-type-Poset 1 _ = raise-unit-Prop l2 + is-increasing-leq-next-prop-fin-sequence-type-Poset (succ-ℕ n@(succ-ℕ _)) u = + ( is-increasing-leq-next-prop-fin-sequence-type-Poset + ( n) + ( tail-fin-sequence n u)) ∧ + ( leq-prop-Poset P (u (inl (inr star))) (u (inr star))) + + is-increasing-leq-next-fin-sequence-type-Poset : + (n : ℕ) → fin-sequence (type-Poset P) n → UU l2 + is-increasing-leq-next-fin-sequence-type-Poset n = + is-in-subtype (is-increasing-leq-next-prop-fin-sequence-type-Poset n) + abstract - reverses-order-is-increasing-fin-sequence-type-Poset : + is-increasing-is-increasing-leq-next-fin-sequence-type-Poset : (n : ℕ) (u : fin-sequence (type-Poset P) n) → - is-increasing-fin-sequence-type-Poset P n u → - preserves-order-Poset (opposite-Poset (Fin-Poset n)) P u - reverses-order-is-increasing-fin-sequence-type-Poset - (succ-ℕ n) u _ (inr star) (inr star) _ = + is-increasing-leq-next-fin-sequence-type-Poset n u → + is-increasing-fin-sequence-type-Poset P n u + is-increasing-is-increasing-leq-next-fin-sequence-type-Poset + (succ-ℕ _) u H (inr star) (inr star) _ = refl-leq-Poset P (u (inr star)) - reverses-order-is-increasing-fin-sequence-type-Poset - (succ-ℕ (succ-ℕ n)) u (u₁≤u₂ , increasing-tail-u) (inr star) (inl j) _ = + is-increasing-is-increasing-leq-next-fin-sequence-type-Poset + (succ-ℕ n@(succ-ℕ _)) u (incr-tail-u , u₋₂≤u₋₁) (inl i) (inr star) _ = transitive-leq-Poset ( P) - ( u (inr star)) + ( u (inl i)) ( u (inl (inr star))) - ( u (inl j)) - ( reverses-order-is-increasing-fin-sequence-type-Poset - ( succ-ℕ n) - ( tail-fin-sequence (succ-ℕ n) u) - ( increasing-tail-u) + ( u (inr star)) + ( u₋₂≤u₋₁) + ( is-increasing-is-increasing-leq-next-fin-sequence-type-Poset + ( n) + ( tail-fin-sequence n u) + ( incr-tail-u) + ( i) ( inr star) - ( j) ( star)) - ( u₁≤u₂) - reverses-order-is-increasing-fin-sequence-type-Poset - (succ-ℕ (succ-ℕ n)) u (u₁≤u₂ , increasing-tail-u) (inl i) (inl j) j≤i = - reverses-order-is-increasing-fin-sequence-type-Poset - ( succ-ℕ n) - ( tail-fin-sequence (succ-ℕ n) u) - ( increasing-tail-u) + is-increasing-is-increasing-leq-next-fin-sequence-type-Poset + ( succ-ℕ n@(succ-ℕ _)) u (incr-tail-u , _) (inl i) (inl j) i≤j = + is-increasing-is-increasing-leq-next-fin-sequence-type-Poset + ( n) + ( tail-fin-sequence n u) + ( incr-tail-u) ( i) ( j) - ( j≤i) + ( i≤j) - is-increasing-reverses-order-fin-sequence-type-Poset : + is-increasing-leq-next-is-increasing-fin-sequence-type-Poset : (n : ℕ) (u : fin-sequence (type-Poset P) n) → - preserves-order-Poset (opposite-Poset (Fin-Poset n)) P u → - is-increasing-fin-sequence-type-Poset P n u - is-increasing-reverses-order-fin-sequence-type-Poset 0 u H = raise-star - is-increasing-reverses-order-fin-sequence-type-Poset 1 u H = raise-star - is-increasing-reverses-order-fin-sequence-type-Poset - (succ-ℕ (succ-ℕ n)) u H = - ( H (inr star) (neg-two-Fin (succ-ℕ n)) star , - is-increasing-reverses-order-fin-sequence-type-Poset - ( succ-ℕ n) - ( tail-fin-sequence (succ-ℕ n) u) - ( λ i j → H (inl i) (inl j))) - - reverses-order-iff-is-increasing-fin-sequence-type-Poset : - (n : ℕ) (u : fin-sequence (type-Poset P) n) → - is-increasing-fin-sequence-type-Poset P n u ↔ - preserves-order-Poset (opposite-Poset (Fin-Poset n)) P u - reverses-order-iff-is-increasing-fin-sequence-type-Poset n u = - ( reverses-order-is-increasing-fin-sequence-type-Poset n u , - is-increasing-reverses-order-fin-sequence-type-Poset n u) - - reverses-order-increasing-fin-sequence-type-Poset : - (n : ℕ) (u : increasing-fin-sequence-type-Poset P n) → - preserves-order-Poset - ( opposite-Poset (Fin-Poset n)) - ( P) - ( fin-sequence-increasing-fin-sequence-type-Poset P n u) - reverses-order-increasing-fin-sequence-type-Poset n = - ind-Σ (reverses-order-is-increasing-fin-sequence-type-Poset n) + is-increasing-fin-sequence-type-Poset P n u → + is-increasing-leq-next-fin-sequence-type-Poset n u + is-increasing-leq-next-is-increasing-fin-sequence-type-Poset 0 u H = + raise-star + is-increasing-leq-next-is-increasing-fin-sequence-type-Poset 1 u H = + raise-star + is-increasing-leq-next-is-increasing-fin-sequence-type-Poset + (succ-ℕ n@(succ-ℕ _)) u H = + ( is-increasing-leq-next-is-increasing-fin-sequence-type-Poset + ( n) + ( tail-fin-sequence n u) + ( λ i j → H (inl i) (inl j)) , + H (inl (inr star)) (inr star) star) ``` diff --git a/src/order-theory/increasing-nonempty-arrays-posets.lagda.md b/src/order-theory/increasing-nonempty-arrays-posets.lagda.md index cdedaf52be3..9534440869a 100644 --- a/src/order-theory/increasing-nonempty-arrays-posets.lagda.md +++ b/src/order-theory/increasing-nonempty-arrays-posets.lagda.md @@ -123,11 +123,8 @@ module _ ( P) ( array-tail-increasing-nonempty-array-type-Poset u) is-increasing-array-tail-increasing-nonempty-array-type-Poset - (((1 , _) , _) , _) = - raise-star - is-increasing-array-tail-increasing-nonempty-array-type-Poset - (((succ-ℕ (succ-ℕ n) , _) , _) , _ , is-increasing-u-tail) = - is-increasing-u-tail + (((succ-ℕ n , u) , _) , H) i j = + H (inl-Fin n i) (inl-Fin n j) tail-increasing-nonempty-array-type-Poset : increasing-nonempty-array-type-Poset P → increasing-array-type-Poset P @@ -158,22 +155,12 @@ module _ ( array-init-increasing-nonempty-array-type-Poset u) is-increasing-array-init-increasing-nonempty-array-type-Poset (((succ-ℕ n , u) , _) , H) = - is-increasing-reverses-order-fin-sequence-type-Poset + preserves-order-comp-Poset + ( Fin-Poset n) + ( Fin-Poset (succ-ℕ n)) ( P) - ( n) - ( u ∘ skip-zero-Fin n) - ( preserves-order-comp-Poset - ( opposite-Poset (Fin-Poset n)) - ( opposite-Poset (Fin-Poset (succ-ℕ n))) - ( P) - ( u , - reverses-order-is-increasing-fin-sequence-type-Poset - ( P) - ( succ-ℕ n) - ( u) - ( H)) - ( skip-zero-Fin n , - λ i j → preserves-order-skip-zero-Fin n j i)) + ( u , H) + ( inr-Fin n , preserves-order-inr-Fin n) init-increasing-nonempty-array-type-Poset : increasing-nonempty-array-type-Poset P → increasing-array-type-Poset P @@ -182,7 +169,7 @@ module _ is-increasing-array-init-increasing-nonempty-array-type-Poset u) ``` -### The head of a nonempty array is its least element +### The head of a nonempty array is its greatest element ```agda module _ @@ -191,24 +178,18 @@ module _ where abstract - is-least-element-head-increasing-nonempty-array-type-Poset : + is-greatest-element-head-increasing-nonempty-array-type-Poset : (u : increasing-nonempty-array-type-Poset P) (i : Fin (length-increasing-nonempty-array-type-Poset P u)) → leq-Poset P - ( head-increasing-nonempty-array-type-Poset P u) ( fin-sequence-increasing-nonempty-array-type-Poset P u i) - is-least-element-head-increasing-nonempty-array-type-Poset + ( head-increasing-nonempty-array-type-Poset P u) + is-greatest-element-head-increasing-nonempty-array-type-Poset (((succ-ℕ n , u) , _) , H) i = - reverses-order-increasing-fin-sequence-type-Poset - ( P) - ( succ-ℕ n) - ( u , H) - ( neg-one-Fin n) - ( i) - ( star) + H i (neg-one-Fin n) star ``` -### The last element of a nonempty array is its greatest element +### The last element of a nonempty array is its least element ```agda module _ @@ -217,19 +198,13 @@ module _ where abstract - is-greatest-element-last-increasing-nonempty-array-type-Poset : + is-least-element-last-increasing-nonempty-array-type-Poset : (u : increasing-nonempty-array-type-Poset P) (i : Fin (length-increasing-nonempty-array-type-Poset P u)) → leq-Poset P - ( fin-sequence-increasing-nonempty-array-type-Poset P u i) ( last-increasing-nonempty-array-type-Poset P u) - is-greatest-element-last-increasing-nonempty-array-type-Poset + ( fin-sequence-increasing-nonempty-array-type-Poset P u i) + is-least-element-last-increasing-nonempty-array-type-Poset (((succ-ℕ n , u) , _) , H) i = - reverses-order-increasing-fin-sequence-type-Poset - ( P) - ( succ-ℕ n) - ( u , H) - ( i) - ( zero-Fin n) - ( leq-zero-Fin n i) + H (zero-Fin n) i (leq-zero-Fin n i) ``` diff --git a/src/univalent-combinatorics/standard-finite-types.lagda.md b/src/univalent-combinatorics/standard-finite-types.lagda.md index c683359f921..5e507b64bfe 100644 --- a/src/univalent-combinatorics/standard-finite-types.lagda.md +++ b/src/univalent-combinatorics/standard-finite-types.lagda.md @@ -214,8 +214,7 @@ is-nonzero-Fin (succ-ℕ k) x = ¬ (is-zero-Fin (succ-ℕ k) x) ```agda skip-zero-Fin : (k : ℕ) → Fin k → Fin (succ-ℕ k) -skip-zero-Fin (succ-ℕ k) (inl x) = inl (skip-zero-Fin k x) -skip-zero-Fin (succ-ℕ k) (inr star) = inr star +skip-zero-Fin = inr-Fin succ-Fin : (k : ℕ) → Fin k → Fin k succ-Fin (succ-ℕ k) (inl x) = skip-zero-Fin k x From 831415ce219bca2b421841d21beaeba7a97030fc Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 1 May 2026 10:52:04 -0700 Subject: [PATCH 06/14] Update --- ...uences-of-elements-abelian-groups.lagda.md | 12 +- ...cessive-elements-finite-sequences.lagda.md | 4 +- src/order-theory.lagda.md | 1 + .../closed-intervals-large-posets.lagda.md | 11 ++ ...ncreasing-finite-sequences-posets.lagda.md | 44 +---- ...set-closed-intervals-large-posets.lagda.md | 169 +++++++++++++++++ src/real-numbers.lagda.md | 1 + ...set-closed-intervals-real-numbers.lagda.md | 140 ++++++++++++++ ...ons-closed-intervals-real-numbers.lagda.md | 177 +++++++----------- 9 files changed, 405 insertions(+), 154 deletions(-) create mode 100644 src/order-theory/large-poset-closed-intervals-large-posets.lagda.md create mode 100644 src/real-numbers/large-poset-closed-intervals-real-numbers.lagda.md diff --git a/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md b/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md index e0436da8639..18336af4749 100644 --- a/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md +++ b/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md @@ -16,6 +16,7 @@ open import finite-group-theory.permutations-standard-finite-types open import foundation.action-on-identifications-functions open import foundation.coproduct-types +open import foundation.unit-type open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-types @@ -321,20 +322,21 @@ module _ sum-telescope-fin-sequence-type-Ab : (n : ℕ) (u : fin-sequence-type-Ab G (succ-ℕ n)) → sum-fin-sequence-type-Ab G n (telescope-fin-sequence-type-Ab n u) ＝ - right-subtraction-Ab G (head-fin-sequence n u) (last-fin-sequence n u) + right-subtraction-Ab G (last-fin-sequence n u) (head-fin-sequence n u) sum-telescope-fin-sequence-type-Ab 0 u = - inv (right-inverse-law-add-Ab G (head-fin-sequence 0 u)) + inv (right-inverse-law-add-Ab G (u (inr star))) sum-telescope-fin-sequence-type-Ab (succ-ℕ n) u = ( ap-add-Ab G - ( sum-telescope-fin-sequence-type-Ab n (tail-fin-sequence (succ-ℕ n) u)) + ( sum-telescope-fin-sequence-type-Ab + ( n) + ( tail-fin-sequence (succ-ℕ n) u)) ( refl)) ∙ - ( commutative-add-Ab G _ _) ∙ ( add-right-subtraction-Ab G _ _ _) sum-telescope-fin-sequence-type-Ab' : (n : ℕ) (u : fin-sequence-type-Ab G (succ-ℕ n)) → sum-fin-sequence-type-Ab G n (telescope-fin-sequence-type-Ab' n u) ＝ - right-subtraction-Ab G (last-fin-sequence n u) (head-fin-sequence n u) + right-subtraction-Ab G (head-fin-sequence n u) (last-fin-sequence n u) sum-telescope-fin-sequence-type-Ab' n u = ( htpy-sum-fin-sequence-type-Ab G ( n) diff --git a/src/lists/pairs-of-successive-elements-finite-sequences.lagda.md b/src/lists/pairs-of-successive-elements-finite-sequences.lagda.md index 56e8e4845cf..d14baa06a97 100644 --- a/src/lists/pairs-of-successive-elements-finite-sequences.lagda.md +++ b/src/lists/pairs-of-successive-elements-finite-sequences.lagda.md @@ -39,6 +39,6 @@ pair-succ-fin-sequence : {l : Level} {A : UU l} (n : ℕ) → fin-sequence A (succ-ℕ n) → fin-sequence (A × A) n pair-succ-fin-sequence n a i = - ( a (skip-zero-Fin n i) , - a (inl-Fin n i)) + ( a (inl-Fin n i) , + a (inr-Fin n i)) ``` diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md index be413808c90..06c4b28dac0 100644 --- a/src/order-theory.lagda.md +++ b/src/order-theory.lagda.md @@ -86,6 +86,7 @@ open import order-theory.large-join-semilattices public open import order-theory.large-locales public open import order-theory.large-meet-semilattices public open import order-theory.large-meet-subsemilattices public +open import order-theory.large-poset-closed-intervals-large-posets public open import order-theory.large-posets public open import order-theory.large-preorders public open import order-theory.large-quotient-locales public diff --git a/src/order-theory/closed-intervals-large-posets.lagda.md b/src/order-theory/closed-intervals-large-posets.lagda.md index fdde553f930..753fdd7b28c 100644 --- a/src/order-theory/closed-intervals-large-posets.lagda.md +++ b/src/order-theory/closed-intervals-large-posets.lagda.md @@ -59,6 +59,12 @@ module _ subtype-closed-interval-Large-Poset _ [a,b] = is-in-closed-interval-prop-Large-Poset [a,b] + type-closed-interval-Large-Poset : + {l1 l2 : Level} (l3 : Level) → + closed-interval-Large-Poset l1 l2 → UU (α l3 ⊔ β l1 l3 ⊔ β l3 l2) + type-closed-interval-Large-Poset l3 [a,b] = + type-subtype (subtype-closed-interval-Large-Poset l3 [a,b]) + lower-bound-closed-interval-Large-Poset : {l1 l2 : Level} → closed-interval-Large-Poset l1 l2 → type-Large-Poset P l1 lower-bound-closed-interval-Large-Poset ((a , b) , _) = a @@ -66,4 +72,9 @@ module _ upper-bound-closed-interval-Large-Poset : {l1 l2 : Level} → closed-interval-Large-Poset l1 l2 → type-Large-Poset P l2 upper-bound-closed-interval-Large-Poset ((a , b) , _) = b + + singleton-closed-interval-Large-Poset : + {l : Level} → type-Large-Poset P l → closed-interval-Large-Poset l l + singleton-closed-interval-Large-Poset x = + ( (x , x) , refl-leq-Large-Poset P x) ``` diff --git a/src/order-theory/increasing-finite-sequences-posets.lagda.md b/src/order-theory/increasing-finite-sequences-posets.lagda.md index 3c325c6d95c..ae1246896b5 100644 --- a/src/order-theory/increasing-finite-sequences-posets.lagda.md +++ b/src/order-theory/increasing-finite-sequences-posets.lagda.md @@ -169,45 +169,7 @@ module _ closed-intervals-increasing-fin-sequence-type-Poset : (n : ℕ) → increasing-fin-sequence-type-Poset P (succ-ℕ n) → fin-sequence (closed-interval-Poset P) n - closed-intervals-increasing-fin-sequence-type-Poset - ( succ-ℕ n) - ( u , u₁≤u₂ , is-increasing-tail-u) = - cons-fin-sequence - ( n) - ( ( head-fin-sequence (succ-ℕ n) u , - head-fin-sequence n (tail-fin-sequence (succ-ℕ n) u)) , - u₁≤u₂) - ( closed-intervals-increasing-fin-sequence-type-Poset - ( n) - ( tail-fin-sequence (succ-ℕ n) u , is-increasing-tail-u)) - - closed-intervals-increasing-fin-sequence-type-Poset' : - (n : ℕ) → increasing-fin-sequence-type-Poset P (succ-ℕ n) → - fin-sequence (closed-interval-Poset P) n - closed-intervals-increasing-fin-sequence-type-Poset' n (u , H) i = - ( pair-succ-fin-sequence' n u i , - reverses-order-is-increasing-fin-sequence-type-Poset P - ( succ-ℕ n) - ( u) - ( H) - ( skip-zero-Fin n i) - ( inl-Fin n i) - ( leq-succ-Fin n i)) - - abstract - htpy-closed-intervals-increasing-fin-sequence-type-Poset' : - (n : ℕ) (u : increasing-fin-sequence-type-Poset P (succ-ℕ n)) → - closed-intervals-increasing-fin-sequence-type-Poset n u ~ - closed-intervals-increasing-fin-sequence-type-Poset' n u - htpy-closed-intervals-increasing-fin-sequence-type-Poset' - (succ-ℕ n) (u , _ , H) (inl i) = - htpy-closed-intervals-increasing-fin-sequence-type-Poset' - ( n) - ( tail-fin-sequence (succ-ℕ n) u , H) - ( i) - htpy-closed-intervals-increasing-fin-sequence-type-Poset' - (succ-ℕ n) (u , _ , _) (inr star) = - eq-type-subtype - ( ind-Σ (leq-prop-Poset P)) - ( refl) + closed-intervals-increasing-fin-sequence-type-Poset n (u , H) i = + ( pair-succ-fin-sequence n u i , + H (inl-Fin n i) (inr-Fin n i) (leq-succ-Fin n i)) ``` diff --git a/src/order-theory/large-poset-closed-intervals-large-posets.lagda.md b/src/order-theory/large-poset-closed-intervals-large-posets.lagda.md new file mode 100644 index 00000000000..d675bfdb533 --- /dev/null +++ b/src/order-theory/large-poset-closed-intervals-large-posets.lagda.md @@ -0,0 +1,169 @@ +# The large poset of closed intervals in large posets + +```agda +module order-theory.large-poset-closed-intervals-large-posets where +``` + +
Imports + +```agda +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.equality-cartesian-product-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.subtypes +open import foundation.universe-levels + +open import order-theory.closed-intervals-large-posets +open import order-theory.large-posets +open import order-theory.large-preorders +``` + +
+ +## Idea + +In a [large poset](order-theory.large-posets.lagda.md) `P`, the type of +[closed intervals](order-theory.closed-intervals-large-posets.md) itself forms a +large poset under the containment relation, in which `[a, b]` is contained in +`[c, d]` if `c ≤ a` and `b ≤ d`. + +## Definition + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} (P : Large-Poset α β) + where + + leq-prop-closed-interval-Large-Poset : + {l1 l2 l3 l4 : Level} → + closed-interval-Large-Poset P l1 l2 → + closed-interval-Large-Poset P l3 l4 → + Prop (β l2 l4 ⊔ β l3 l1) + leq-prop-closed-interval-Large-Poset ((a , b) , _) ((c , d) , _) = + leq-prop-Large-Poset P c a ∧ leq-prop-Large-Poset P b d + + leq-closed-interval-Large-Poset : + {l1 l2 l3 l4 : Level} → + closed-interval-Large-Poset P l1 l2 → + closed-interval-Large-Poset P l3 l4 → + UU (β l2 l4 ⊔ β l3 l1) + leq-closed-interval-Large-Poset [a,b] [c,d] = + type-Prop (leq-prop-closed-interval-Large-Poset [a,b] [c,d]) +``` + +## Properties + +### Containment of closed intervals is reflexive + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} (P : Large-Poset α β) + where + + abstract + refl-leq-closed-interval-Large-Poset : + {l1 l2 : Level} ([a,b] : closed-interval-Large-Poset P l1 l2) → + leq-closed-interval-Large-Poset P [a,b] [a,b] + refl-leq-closed-interval-Large-Poset ((a , b) , _) = + ( refl-leq-Large-Poset P a , + refl-leq-Large-Poset P b) +``` + +### Containment of closed intervals is transitive + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} (P : Large-Poset α β) + where + + abstract + transitive-leq-closed-interval-Large-Poset : + {l1 l2 l3 l4 l5 l6 : Level} + ([a,b] : closed-interval-Large-Poset P l1 l2) + ([c,d] : closed-interval-Large-Poset P l3 l4) + ([e,f] : closed-interval-Large-Poset P l5 l6) → + leq-closed-interval-Large-Poset P [c,d] [e,f] → + leq-closed-interval-Large-Poset P [a,b] [c,d] → + leq-closed-interval-Large-Poset P [a,b] [e,f] + transitive-leq-closed-interval-Large-Poset + ((a , b) , _) ((c , d) , _) ((e , f) , _) (e≤c , d≤f) (c≤a , b≤d) = + ( transitive-leq-Large-Poset P e c a c≤a e≤c , + transitive-leq-Large-Poset P b d f d≤f b≤d) +``` + +### Containment of closed intervals is antisymmetric + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} (P : Large-Poset α β) + where + + abstract + antisymmetric-leq-closed-interval-Large-Poset : + {l1 l2 : Level} + ([a,b] [c,d] : closed-interval-Large-Poset P l1 l2) → + leq-closed-interval-Large-Poset P [a,b] [c,d] → + leq-closed-interval-Large-Poset P [c,d] [a,b] → + [a,b] ＝ [c,d] + antisymmetric-leq-closed-interval-Large-Poset + ((a , b) , _) ((c , d) , _) (c≤a , b≤d) (a≤c , d≤b) = + eq-type-subtype + ( ind-Σ (leq-prop-Large-Poset P)) + ( eq-pair + ( antisymmetric-leq-Large-Poset P a c a≤c c≤a) + ( antisymmetric-leq-Large-Poset P b d b≤d d≤b)) +``` + +### The large poset of closed intervals + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} (P : Large-Poset α β) + where + + large-preorder-closed-interval-Large-Poset : + Large-Preorder (λ l → α l ⊔ β l l) (λ l1 l2 → β l1 l2 ⊔ β l2 l1) + large-preorder-closed-interval-Large-Poset = + make-Large-Preorder + ( λ l → closed-interval-Large-Poset P l l) + ( leq-prop-closed-interval-Large-Poset P) + ( refl-leq-closed-interval-Large-Poset P) + ( transitive-leq-closed-interval-Large-Poset P) + + large-poset-closed-interval-Large-Poset : + Large-Poset (λ l → α l ⊔ β l l) (λ l1 l2 → β l1 l2 ⊔ β l2 l1) + large-poset-closed-interval-Large-Poset = + make-Large-Poset + ( large-preorder-closed-interval-Large-Poset) + ( antisymmetric-leq-closed-interval-Large-Poset P) +``` + +### If `[a, b]` is contained in `[c, d]`, then the subtype of `[a, b]` is contained in the subtype of `[c, d]` + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} (P : Large-Poset α β) + where + + abstract + leq-subtype-leq-closed-interval-Large-Poset : + {l1 l2 l3 l4 l5 : Level} + ([a,b] : closed-interval-Large-Poset P l1 l2) + ([c,d] : closed-interval-Large-Poset P l3 l4) → + leq-closed-interval-Large-Poset P [a,b] [c,d] → + subtype-closed-interval-Large-Poset P l5 [a,b] ⊆ + subtype-closed-interval-Large-Poset P l5 [c,d] + leq-subtype-leq-closed-interval-Large-Poset [a,b] [c,d] [a,b]⊆[c,d] x = + transitive-leq-closed-interval-Large-Poset + ( P) + ( singleton-closed-interval-Large-Poset P x) + ( [a,b]) + ( [c,d]) + ( [a,b]⊆[c,d]) +``` + +## See also + +- [The (small) poset of closed intervals in (small) posets](order-theory.poset-closed-intervals-posets.md) diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index c6767f75a7a..08d5ab650a0 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -65,6 +65,7 @@ open import real-numbers.iterated-halving-difference-real-numbers public open import real-numbers.large-additive-group-of-real-numbers public open import real-numbers.large-multiplicative-group-of-positive-real-numbers public open import real-numbers.large-multiplicative-monoid-of-real-numbers public +open import real-numbers.large-poset-closed-intervals-real-numbers public open import real-numbers.large-ring-of-real-numbers public open import real-numbers.limits-of-endomaps-real-numbers public open import real-numbers.limits-of-sequences-real-numbers public diff --git a/src/real-numbers/large-poset-closed-intervals-real-numbers.lagda.md b/src/real-numbers/large-poset-closed-intervals-real-numbers.lagda.md new file mode 100644 index 00000000000..e0bab853e40 --- /dev/null +++ b/src/real-numbers/large-poset-closed-intervals-real-numbers.lagda.md @@ -0,0 +1,140 @@ +# The large poset of closed intervals of real numbers + +```agda +module real-numbers.large-poset-closed-intervals-real-numbers where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.subtypes +open import foundation.universe-levels + +open import order-theory.large-poset-closed-intervals-large-posets +open import order-theory.large-posets + +open import real-numbers.closed-intervals-real-numbers +open import real-numbers.difference-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.raising-universe-levels-real-numbers +``` + +
+ +## Idea + +The type of [closed intervals](real-numbers.closed-intervals-real-numbers.md) in +the [real numbers](real-numbers.dedekind-real-numbers.md) forms a +[large poset](order-theory.large-posets.md) under the containment relation, +where `[a, b]` is contained in `[c, d]` if `c ≤ a` and `b ≤ d`. + +## Definition + +```agda +leq-prop-closed-interval-ℝ : + {l1 l2 l3 l4 : Level} → + closed-interval-ℝ l1 l2 → closed-interval-ℝ l3 l4 → Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4) +leq-prop-closed-interval-ℝ = + leq-prop-closed-interval-Large-Poset ℝ-Large-Poset + +leq-closed-interval-ℝ : + {l1 l2 l3 l4 : Level} → + closed-interval-ℝ l1 l2 → closed-interval-ℝ l3 l4 → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) +leq-closed-interval-ℝ = leq-closed-interval-Large-Poset ℝ-Large-Poset +``` + +## Properties + +### Containment of intervals forms a poset + +```agda +refl-leq-closed-interval-ℝ : + {l1 l2 : Level} ([a,b] : closed-interval-ℝ l1 l2) → + leq-closed-interval-ℝ [a,b] [a,b] +refl-leq-closed-interval-ℝ = + refl-leq-closed-interval-Large-Poset ℝ-Large-Poset + +transitive-leq-closed-interval-ℝ : + {l1 l2 l3 l4 l5 l6 : Level} + ([a,b] : closed-interval-ℝ l1 l2) + ([c,d] : closed-interval-ℝ l3 l4) + ([e,f] : closed-interval-ℝ l5 l6) → + leq-closed-interval-ℝ [c,d] [e,f] → + leq-closed-interval-ℝ [a,b] [c,d] → + leq-closed-interval-ℝ [a,b] [e,f] +transitive-leq-closed-interval-ℝ = + transitive-leq-closed-interval-Large-Poset ℝ-Large-Poset + +antisymmetric-leq-closed-interval-ℝ : + {l1 l2 : Level} ([a,b] [c,d] : closed-interval-ℝ l1 l2) → + leq-closed-interval-ℝ [a,b] [c,d] → + leq-closed-interval-ℝ [c,d] [a,b] → + [a,b] ＝ [c,d] +antisymmetric-leq-closed-interval-ℝ = + antisymmetric-leq-closed-interval-Large-Poset ℝ-Large-Poset + +large-poset-closed-interval-ℝ : Large-Poset lsuc (_⊔_) +large-poset-closed-interval-ℝ = + large-poset-closed-interval-Large-Poset ℝ-Large-Poset +``` + +### If `[a, b]` is contained in `[c, d]`, then their subtypes are contained + +```agda +abstract + leq-subtype-leq-closed-interval-ℝ : + {l1 l2 l3 l4 l5 : Level} + ([a,b] : closed-interval-ℝ l1 l2) + ([c,d] : closed-interval-ℝ l3 l4) → + leq-closed-interval-ℝ [a,b] [c,d] → + subtype-closed-interval-ℝ l5 [a,b] ⊆ subtype-closed-interval-ℝ l5 [c,d] + leq-subtype-leq-closed-interval-ℝ = + leq-subtype-leq-closed-interval-Large-Poset ℝ-Large-Poset +``` + +### If the subtype associated with `[a, b]` is contained in the subtype associated with `[c, d]`, then `[a, b]` is contained in `[c, d]` + +```agda +abstract + leq-leq-subtype-closed-interval-ℝ : + {l1 l2 l3 l4 : Level} + ([a,b] : closed-interval-ℝ l1 l2) + ([c,d] : closed-interval-ℝ l3 l4) → + ( subtype-closed-interval-ℝ (l1 ⊔ l2) [a,b] ⊆ + subtype-closed-interval-ℝ (l1 ⊔ l2) [c,d]) → + leq-closed-interval-ℝ [a,b] [c,d] + leq-leq-subtype-closed-interval-ℝ + {l1} {l2} ((a , b) , a≤b) ((c , d) , c≤d) S[a,b]⊆S[c,d] = + ( reflects-leq-right-raise-ℝ + ( l2) + ( pr1 + ( S[a,b]⊆S[c,d] + ( raise-ℝ l2 a) + ( leq-sim-ℝ (sim-raise-ℝ l2 a) , + preserves-leq-left-raise-ℝ l2 a≤b))) , + reflects-leq-left-raise-ℝ + ( l1) + ( pr2 + ( S[a,b]⊆S[c,d] + ( raise-ℝ l1 b) + ( preserves-leq-right-raise-ℝ l1 a≤b , + leq-sim-ℝ' (sim-raise-ℝ l1 b))))) +``` + +### If `[a, b]` is contained in `[c, d]`, the width of `[a, b]` is less than or equal to the width of `[c, d]` + +```agda +abstract + leq-width-leq-closed-interval-ℝ : + {l1 l2 l3 l4 : Level} + ([a,b] : closed-interval-ℝ l1 l2) + ([c,d] : closed-interval-ℝ l3 l4) → + leq-closed-interval-ℝ [a,b] [c,d] → + leq-ℝ (width-closed-interval-ℝ [a,b]) (width-closed-interval-ℝ [c,d]) + leq-width-leq-closed-interval-ℝ ((a , b) , _) ((c , d) , _) (a≤c , b≤d) = + preserves-leq-add-ℝ b≤d (neg-leq-ℝ a≤c) +``` diff --git a/src/real-numbers/partitions-closed-intervals-real-numbers.lagda.md b/src/real-numbers/partitions-closed-intervals-real-numbers.lagda.md index 252f62f8610..899080c34eb 100644 --- a/src/real-numbers/partitions-closed-intervals-real-numbers.lagda.md +++ b/src/real-numbers/partitions-closed-intervals-real-numbers.lagda.md @@ -1,6 +1,8 @@ # Partitions of closed intervals of real numbers ```agda +{-# OPTIONS --lossy-unification #-} + module real-numbers.partitions-closed-intervals-real-numbers where ``` @@ -11,41 +13,32 @@ open import elementary-number-theory.inequality-standard-finite-types open import elementary-number-theory.natural-numbers open import foundation.action-on-identifications-functions -open import foundation.binary-transport open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.function-types open import foundation.identity-types open import foundation.logical-equivalences +open import foundation.transport-along-identifications open import foundation.unit-type open import foundation.universe-levels open import lists.finite-sequences open import lists.tuples -open import order-theory.increasing-arrays-posets open import order-theory.increasing-finite-sequences-posets open import order-theory.increasing-nonempty-arrays-posets -open import order-theory.large-posets -open import order-theory.least-upper-bounds-large-posets open import order-theory.lower-bounds-large-posets -open import order-theory.opposite-posets -open import order-theory.order-preserving-maps-posets open import order-theory.upper-bounds-large-posets open import real-numbers.addition-real-numbers open import real-numbers.closed-intervals-real-numbers open import real-numbers.dedekind-real-numbers -open import real-numbers.difference-real-numbers -open import real-numbers.inequalities-addition-and-subtraction-real-numbers open import real-numbers.inequality-nonnegative-real-numbers open import real-numbers.inequality-real-numbers +open import real-numbers.large-poset-closed-intervals-real-numbers open import real-numbers.maximum-finite-families-nonnegative-real-numbers open import real-numbers.multiplication-nonnegative-real-numbers -open import real-numbers.multiplication-real-numbers open import real-numbers.nonnegative-real-numbers -open import real-numbers.rational-real-numbers -open import real-numbers.similarity-real-numbers open import univalent-combinatorics.standard-finite-types ``` @@ -73,8 +66,8 @@ module _ partition-closed-interval-ℝ = Σ ( increasing-nonempty-array-type-Poset (ℝ-Poset l)) ( λ u → - ( head-increasing-nonempty-array-type-Poset (ℝ-Poset l) u ＝ a) × - ( last-increasing-nonempty-array-type-Poset (ℝ-Poset l) u ＝ b)) + ( last-increasing-nonempty-array-type-Poset (ℝ-Poset l) u ＝ a) × + ( head-increasing-nonempty-array-type-Poset (ℝ-Poset l) u ＝ b)) pred-length-partition-closed-interval-ℝ : partition-closed-interval-ℝ → ℕ @@ -111,40 +104,25 @@ module _ ((((succ-ℕ n , u) , _) , H) , _) = ( u , H) - abstract - reverses-order-fin-sequence-partition-closed-interval-ℝ : - (p : partition-closed-interval-ℝ) → - preserves-order-Poset - ( opposite-Poset (Fin-Poset (length-partition-closed-interval-ℝ p))) - ( ℝ-Poset l) - ( real-fin-sequence-partition-closed-interval-ℝ p) - reverses-order-fin-sequence-partition-closed-interval-ℝ - ((((succ-ℕ n , u) , _) , H) , _) = - reverses-order-is-increasing-fin-sequence-type-Poset - ( ℝ-Poset l) - ( succ-ℕ n) - ( u) - ( H) - - eq-lower-bound-head-real-fin-sequence-partition-closed-interval-ℝ : + eq-lower-bound-last-real-fin-sequence-partition-closed-interval-ℝ : (p : partition-closed-interval-ℝ) → - head-fin-sequence + last-fin-sequence ( pred-length-partition-closed-interval-ℝ p) ( real-fin-sequence-partition-closed-interval-ℝ p) ＝ a - eq-lower-bound-head-real-fin-sequence-partition-closed-interval-ℝ - ((((succ-ℕ n , u) , _) , _) , u₋₁=a , _) = - u₋₁=a + eq-lower-bound-last-real-fin-sequence-partition-closed-interval-ℝ + ((((succ-ℕ n , u) , _) , _) , u₀=a , _) = + u₀=a - eq-upper-bound-last-real-fin-sequence-partition-closed-interval-ℝ : + eq-upper-bound-head-real-fin-sequence-partition-closed-interval-ℝ : (p : partition-closed-interval-ℝ) → - last-fin-sequence + head-fin-sequence ( pred-length-partition-closed-interval-ℝ p) ( real-fin-sequence-partition-closed-interval-ℝ p) ＝ b - eq-upper-bound-last-real-fin-sequence-partition-closed-interval-ℝ - ((((succ-ℕ n , u) , _) , _) , _ , u₀=b) = - u₀=b + eq-upper-bound-head-real-fin-sequence-partition-closed-interval-ℝ + ((((succ-ℕ n , u) , _) , _) , _ , u₋₁=b) = + u₋₁=b abstract lower-bound-real-fin-sequence-partition-closed-interval-ℝ : @@ -153,16 +131,9 @@ module _ ( ℝ-Large-Poset) ( real-fin-sequence-partition-closed-interval-ℝ p) ( a) - lower-bound-real-fin-sequence-partition-closed-interval-ℝ p i = - binary-tr - ( leq-ℝ) - ( eq-lower-bound-head-real-fin-sequence-partition-closed-interval-ℝ p) - ( refl) - ( reverses-order-fin-sequence-partition-closed-interval-ℝ - ( p) - ( neg-one-Fin (pred-length-partition-closed-interval-ℝ p)) - ( i) - ( leq-neg-one-Fin (pred-length-partition-closed-interval-ℝ p) i)) + lower-bound-real-fin-sequence-partition-closed-interval-ℝ + p@((((succ-ℕ n , u) , _) , H) , u₀=a , _) i = + tr (λ x → leq-ℝ x (u i)) u₀=a (H (zero-Fin n) i (leq-zero-Fin n i)) upper-bound-real-fin-sequence-partition-closed-interval-ℝ : (p : partition-closed-interval-ℝ) → @@ -170,16 +141,9 @@ module _ ( ℝ-Large-Poset) ( real-fin-sequence-partition-closed-interval-ℝ p) ( b) - upper-bound-real-fin-sequence-partition-closed-interval-ℝ p i = - binary-tr - ( leq-ℝ) - ( refl) - ( eq-upper-bound-last-real-fin-sequence-partition-closed-interval-ℝ p) - ( reverses-order-fin-sequence-partition-closed-interval-ℝ - ( p) - ( i) - ( zero-Fin (pred-length-partition-closed-interval-ℝ p)) - ( leq-zero-Fin (pred-length-partition-closed-interval-ℝ p) i)) + upper-bound-real-fin-sequence-partition-closed-interval-ℝ + p@((((succ-ℕ n , u) , _) , H) , _ , u₋₁=b) i = + tr (leq-ℝ (u i)) u₋₁=b (H i (neg-one-Fin n) star) fin-sequence-partition-closed-interval-ℝ : (p : partition-closed-interval-ℝ) → @@ -197,17 +161,39 @@ module _ ### The sequence of closed intervals of a partition ```agda -fin-sequence-closed-interval-partition-closed-interval-ℝ : - {l : Level} ([a,b] : closed-interval-ℝ l l) - (p : partition-closed-interval-ℝ [a,b]) → - fin-sequence - ( closed-interval-ℝ l l) - ( pred-length-partition-closed-interval-ℝ [a,b] p) -fin-sequence-closed-interval-partition-closed-interval-ℝ {l} [a,b] p = - closed-intervals-increasing-fin-sequence-type-Poset - ( ℝ-Poset l) - ( pred-length-partition-closed-interval-ℝ [a,b] p) - ( increasing-real-fin-sequence-partition-closed-interval-ℝ [a,b] p) +module _ + {l : Level} + ([a,b]@((a , b) , _) : closed-interval-ℝ l l) + where + + fin-sequence-closed-interval-partition-closed-interval-ℝ : + (p : partition-closed-interval-ℝ [a,b]) → + fin-sequence + ( closed-interval-ℝ l l) + ( pred-length-partition-closed-interval-ℝ [a,b] p) + fin-sequence-closed-interval-partition-closed-interval-ℝ p = + closed-intervals-increasing-fin-sequence-type-Poset + ( ℝ-Poset l) + ( pred-length-partition-closed-interval-ℝ [a,b] p) + ( increasing-real-fin-sequence-partition-closed-interval-ℝ [a,b] p) + + abstract + leq-fin-sequence-closed-interval-partition-closed-interval-ℝ : + (p : partition-closed-interval-ℝ [a,b]) → + is-upper-bound-family-of-elements-Large-Poset + ( large-poset-closed-interval-ℝ) + ( fin-sequence-closed-interval-partition-closed-interval-ℝ p) + ( [a,b]) + leq-fin-sequence-closed-interval-partition-closed-interval-ℝ + p@((((succ-ℕ n , u) , _) , _) , _) i = + ( lower-bound-real-fin-sequence-partition-closed-interval-ℝ + ( [a,b]) + ( p) + ( inl-Fin n i) , + upper-bound-real-fin-sequence-partition-closed-interval-ℝ + ( [a,b]) + ( p) + ( inr-Fin n i)) ``` ### The mesh of a partition @@ -245,7 +231,7 @@ module _ ```agda module _ {l : Level} - ([a,b]@((a , b) , a≤b) : closed-interval-ℝ l l) + ([a,b] : closed-interval-ℝ l l) where abstract @@ -255,39 +241,14 @@ module _ ( large-poset-ℝ⁰⁺) ( diffs-partition-closed-interval-ℝ [a,b] p) ( nonnegative-width-closed-interval-ℝ [a,b]) - bound-diffs-partition-closed-interval-ℝ - p@((((succ-ℕ n , u) , _) , _) , _) i = - let - open inequality-reasoning-Large-Poset ℝ-Large-Poset - in - chain-of-inequalities - real-ℝ⁰⁺ (diffs-partition-closed-interval-ℝ [a,b] p i) - ≤ u (inl-Fin n i) -ℝ u (skip-zero-Fin n i) - by - leq-eq-ℝ - ( ap - ( width-closed-interval-ℝ) - ( htpy-closed-intervals-increasing-fin-sequence-type-Poset' - ( ℝ-Poset l) - ( pred-length-partition-closed-interval-ℝ [a,b] p) - ( increasing-real-fin-sequence-partition-closed-interval-ℝ - ( [a,b]) - ( p)) - ( i))) - ≤ b -ℝ u (skip-zero-Fin n i) - by - preserves-leq-right-add-ℝ _ _ _ - ( upper-bound-real-fin-sequence-partition-closed-interval-ℝ - ( [a,b]) - ( p) - ( inl-Fin n i)) - ≤ b -ℝ a - by - reverses-leq-left-diff-ℝ _ - ( lower-bound-real-fin-sequence-partition-closed-interval-ℝ - ( [a,b]) - ( p) - ( skip-zero-Fin n i)) + bound-diffs-partition-closed-interval-ℝ p i = + leq-width-leq-closed-interval-ℝ + ( fin-sequence-closed-interval-partition-closed-interval-ℝ [a,b] p i) + ( [a,b]) + ( leq-fin-sequence-closed-interval-partition-closed-interval-ℝ + ( [a,b]) + ( p) + ( i)) bound-mesh-partition-closed-interval-ℝ : (p : partition-closed-interval-ℝ [a,b]) → @@ -314,9 +275,13 @@ module _ trivial-partition-closed-interval-ℝ : partition-closed-interval-ℝ [a,b] trivial-partition-closed-interval-ℝ = - ( ( ((2 , component-tuple 2 (a ∷ b ∷ empty-tuple)) , star) , - a≤b , - raise-star) , + ( ( ( (2 , component-tuple 2 (b ∷ a ∷ empty-tuple)) , + star) , + is-increasing-is-increasing-leq-next-fin-sequence-type-Poset + ( ℝ-Poset l) + ( 2) + ( _) + ( raise-star , a≤b)) , refl , refl) ``` From ddf1b7072b65c46bd338945dbd6b849e57769f2d Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 5 Jun 2026 19:25:34 -0700 Subject: [PATCH 07/14] Progress --- .../inequality-standard-finite-types.lagda.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md index ec6de87d0f0..298787b6213 100644 --- a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md +++ b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md @@ -151,12 +151,12 @@ abstract ```agda abstract - reverses-leq-nat-Fin-reverse : + is-decreasing-nat-Fin-reverse : (k : ℕ) (x y : Fin k) → leq-Fin k x y → leq-ℕ (nat-Fin-reverse k y) (nat-Fin-reverse k x) - reverses-leq-nat-Fin-reverse (succ-ℕ k) x (inr star) x≤y = star - reverses-leq-nat-Fin-reverse (succ-ℕ k) (inl x) (inl y) x≤y = - reverses-leq-nat-Fin-reverse k x y x≤y + is-decreasing-nat-Fin-reverse (succ-ℕ k) x (inr star) x≤y = star + is-decreasing-nat-Fin-reverse (succ-ℕ k) (inl x) (inl y) x≤y = + is-decreasing-nat-Fin-reverse k x y x≤y ``` ### Ordering on the standard finite types is decidable From 1d5bcd87ca7d3afd6db9e469ff4beaaa4fcd5fb5 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 5 Jun 2026 19:44:19 -0700 Subject: [PATCH 08/14] Fix docs --- .../inequality-standard-finite-types.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md index 298787b6213..a3514373d26 100644 --- a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md +++ b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md @@ -183,13 +183,13 @@ linear-leq-Fin (succ-ℕ k) (inl x) (inr y) = inl star linear-leq-Fin (succ-ℕ k) (inr x) y = inr star ``` -### `skip-zero-Fin` preserves inequality +### `inr-Fin` preserves inequality ```agda abstract preserves-order-inr-Fin : (n : ℕ) → - preserves-order-Poset (Fin-Poset n) (Fin-Poset (succ-ℕ n)) (skip-zero-Fin n) + preserves-order-Poset (Fin-Poset n) (Fin-Poset (succ-ℕ n)) (inr-Fin n) preserves-order-inr-Fin (succ-ℕ n) (inl x) (inl y) x≤y = preserves-order-inr-Fin n x y x≤y preserves-order-inr-Fin (succ-ℕ n) (inl x) (inr star) _ = star From 531d3205b3c372f482fda2dfc6d5e8f2ea920b7c Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 6 Jun 2026 10:52:11 -0700 Subject: [PATCH 09/14] Fix imports --- src/order-theory/increasing-finite-sequences-posets.lagda.md | 1 + 1 file changed, 1 insertion(+) diff --git a/src/order-theory/increasing-finite-sequences-posets.lagda.md b/src/order-theory/increasing-finite-sequences-posets.lagda.md index 848b95695f3..adf743a6105 100644 --- a/src/order-theory/increasing-finite-sequences-posets.lagda.md +++ b/src/order-theory/increasing-finite-sequences-posets.lagda.md @@ -16,6 +16,7 @@ open import foundation.dependent-pair-types open import foundation.function-types open import foundation.logical-equivalences open import foundation.propositions +open import foundation.raising-universe-levels-unit-type open import foundation.subtypes open import foundation.unit-type open import foundation.universe-levels From 4d615c8adaaba121000ea31427a76f54db20682f Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 6 Jun 2026 12:24:10 -0700 Subject: [PATCH 10/14] Add a variable name --- src/order-theory/increasing-nonempty-arrays-posets.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/order-theory/increasing-nonempty-arrays-posets.lagda.md b/src/order-theory/increasing-nonempty-arrays-posets.lagda.md index 9534440869a..8893aa2cefb 100644 --- a/src/order-theory/increasing-nonempty-arrays-posets.lagda.md +++ b/src/order-theory/increasing-nonempty-arrays-posets.lagda.md @@ -49,7 +49,7 @@ module _ is-increasing-prop-nonempty-array-type-Poset : subtype l2 (nonempty-array (type-Poset P)) - is-increasing-prop-nonempty-array-type-Poset (u , _) = + is-increasing-prop-nonempty-array-type-Poset (u , is-nonempty-u) = is-increasing-prop-array-type-Poset P u is-increasing-nonempty-array-type-Poset : From a1a04b7695d9969cb00d456ad289ce826d20fad3 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 6 Jun 2026 12:32:44 -0700 Subject: [PATCH 11/14] Fix link --- .../large-poset-closed-intervals-large-posets.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/order-theory/large-poset-closed-intervals-large-posets.lagda.md b/src/order-theory/large-poset-closed-intervals-large-posets.lagda.md index d675bfdb533..db38dc81511 100644 --- a/src/order-theory/large-poset-closed-intervals-large-posets.lagda.md +++ b/src/order-theory/large-poset-closed-intervals-large-posets.lagda.md @@ -24,7 +24,7 @@ open import order-theory.large-preorders ## Idea -In a [large poset](order-theory.large-posets.lagda.md) `P`, the type of +In a [large poset](order-theory.large-posets.md) `P`, the type of [closed intervals](order-theory.closed-intervals-large-posets.md) itself forms a large poset under the containment relation, in which `[a, b]` is contained in `[c, d]` if `c ≤ a` and `b ≤ d`. From f9fcc06c45c59ad680e329b670b68b03309b3827 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 6 Jun 2026 12:33:26 -0700 Subject: [PATCH 12/14] make pre-commit --- ...sums-of-finite-sequences-of-elements-abelian-groups.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md b/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md index 18336af4749..e21cf5f9abe 100644 --- a/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md +++ b/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md @@ -16,12 +16,12 @@ open import finite-group-theory.permutations-standard-finite-types open import foundation.action-on-identifications-functions open import foundation.coproduct-types -open import foundation.unit-type open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-types open import foundation.homotopies open import foundation.identity-types +open import foundation.unit-type open import foundation.universe-levels open import group-theory.abelian-groups From b2f6329fe48feff78f74077b2bcbcf4f3cb67d9f Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Wed, 10 Jun 2026 12:56:14 -0700 Subject: [PATCH 13/14] Progress --- ...c-sequences-commutative-semirings.lagda.md | 2 +- .../congruence-natural-numbers.lagda.md | 2 +- .../finitary-natural-numbers.lagda.md | 6 +- ...-arithmetic-standard-finite-types.lagda.md | 8 +- .../modular-arithmetic.lagda.md | 2 +- .../rational-numbers.lagda.md | 4 + ...mpson-delooping-sign-homomorphism.lagda.md | 2 +- src/foundation/null-homotopic-maps.lagda.md | 17 ++ src/lists/finite-sequences.lagda.md | 2 +- ...roduction-to-homotopy-type-theory.lagda.md | 2 +- .../least-upper-bounds-large-posets.lagda.md | 33 +++ src/real-numbers.lagda.md | 3 + ...families-nonnegative-real-numbers.lagda.md | 57 ++++ ...ons-closed-intervals-real-numbers.lagda.md | 1 + .../rational-real-numbers.lagda.md | 4 + ...ons-closed-intervals-real-numbers.lagda.md | 251 ++++++++++++++++++ ...ons-closed-intervals-real-numbers.lagda.md | 161 +++++++++++ .../unit-fractions-real-numbers.lagda.md | 82 ++++++ .../binomial-theorem-semirings.lagda.md | 4 +- .../standard-finite-types.lagda.md | 23 +- 20 files changed, 640 insertions(+), 26 deletions(-) create mode 100644 src/real-numbers/standard-uniform-partitions-closed-intervals-real-numbers.lagda.md create mode 100644 src/real-numbers/uniform-partitions-closed-intervals-real-numbers.lagda.md create mode 100644 src/real-numbers/unit-fractions-real-numbers.lagda.md diff --git a/src/commutative-algebra/geometric-sequences-commutative-semirings.lagda.md b/src/commutative-algebra/geometric-sequences-commutative-semirings.lagda.md index 1e4b7ed9f99..71fcbc05c19 100644 --- a/src/commutative-algebra/geometric-sequences-commutative-semirings.lagda.md +++ b/src/commutative-algebra/geometric-sequences-commutative-semirings.lagda.md @@ -341,7 +341,7 @@ module _ ap-add-Commutative-Semiring R ( ap ( seq-standard-geometric-sequence-Commutative-Semiring R a r) - ( is-zero-nat-zero-Fin {n})) + ( nat-zero-Fin n)) ( htpy-sum-fin-sequence-type-Commutative-Semiring R n ( λ i → ap diff --git a/src/elementary-number-theory/congruence-natural-numbers.lagda.md b/src/elementary-number-theory/congruence-natural-numbers.lagda.md index 0abb9077859..7e3142369f6 100644 --- a/src/elementary-number-theory/congruence-natural-numbers.lagda.md +++ b/src/elementary-number-theory/congruence-natural-numbers.lagda.md @@ -141,7 +141,7 @@ eq-cong-nat-Fin (succ-ℕ k) x y H = cong-is-zero-nat-zero-Fin : {k : ℕ} → cong-ℕ (succ-ℕ k) (nat-Fin (succ-ℕ k) (zero-Fin k)) zero-ℕ cong-is-zero-nat-zero-Fin {k} = - cong-identification-ℕ (succ-ℕ k) (is-zero-nat-zero-Fin {k}) + cong-identification-ℕ (succ-ℕ k) (nat-zero-Fin k) ``` ```agda diff --git a/src/elementary-number-theory/finitary-natural-numbers.lagda.md b/src/elementary-number-theory/finitary-natural-numbers.lagda.md index 57acf9d9c0e..2d96a638666 100644 --- a/src/elementary-number-theory/finitary-natural-numbers.lagda.md +++ b/src/elementary-number-theory/finitary-natural-numbers.lagda.md @@ -193,7 +193,7 @@ convert-based-succ-based-ℕ ( succ-ℕ k) (constant-based-ℕ .(succ-ℕ k) (inr _)) = ( ap ( λ t → ((succ-ℕ k) *ℕ (succ-ℕ t)) +ℕ t) - ( is-zero-nat-zero-Fin {k})) ∙ + ( nat-zero-Fin k)) ∙ ( right-unit-law-mul-ℕ (succ-ℕ k)) convert-based-succ-based-ℕ (succ-ℕ k) (unary-op-based-ℕ .(succ-ℕ k) (inl x) n) = ap @@ -205,7 +205,7 @@ convert-based-succ-based-ℕ ( ( ( succ-ℕ k) *ℕ ( succ-ℕ (convert-based-ℕ (succ-ℕ k) (succ-based-ℕ (succ-ℕ k) n)))) +ℕ_) - ( is-zero-nat-zero-Fin {k})) ∙ + ( nat-zero-Fin k)) ∙ ( ( ap ( ((succ-ℕ k) *ℕ_) ∘ succ-ℕ) ( convert-based-succ-based-ℕ (succ-ℕ k) n)) ∙ @@ -218,7 +218,7 @@ convert-based-succ-based-ℕ is-section-inv-convert-based-ℕ : (k n : ℕ) → convert-based-ℕ (succ-ℕ k) (inv-convert-based-ℕ k n) ＝ n -is-section-inv-convert-based-ℕ k zero-ℕ = is-zero-nat-zero-Fin {k} +is-section-inv-convert-based-ℕ k zero-ℕ = nat-zero-Fin k is-section-inv-convert-based-ℕ k (succ-ℕ n) = ( convert-based-succ-based-ℕ (succ-ℕ k) (inv-convert-based-ℕ k n)) ∙ ( ap succ-ℕ (is-section-inv-convert-based-ℕ k n)) diff --git a/src/elementary-number-theory/modular-arithmetic-standard-finite-types.lagda.md b/src/elementary-number-theory/modular-arithmetic-standard-finite-types.lagda.md index 302d0c9537d..06bfd5591f7 100644 --- a/src/elementary-number-theory/modular-arithmetic-standard-finite-types.lagda.md +++ b/src/elementary-number-theory/modular-arithmetic-standard-finite-types.lagda.md @@ -72,7 +72,7 @@ cong-nat-succ-Fin (succ-ℕ k) (inr _) = { nat-Fin (succ-ℕ k) (zero-Fin k)} { zero-ℕ} { succ-ℕ k} - ( is-zero-nat-zero-Fin {k}) + ( nat-zero-Fin k) ( cong-zero-ℕ' (succ-ℕ k)) cong-nat-mod-succ-ℕ : @@ -181,7 +181,7 @@ is-surjective-mod-succ-ℕ k = leq-nat-mod-succ-ℕ : (k x : ℕ) → leq-ℕ (nat-Fin (succ-ℕ k) (mod-succ-ℕ k x)) x leq-nat-mod-succ-ℕ k zero-ℕ = - concatenate-eq-leq-ℕ zero-ℕ (is-zero-nat-zero-Fin {k}) (refl-leq-ℕ zero-ℕ) + concatenate-eq-leq-ℕ zero-ℕ (nat-zero-Fin k) (refl-leq-ℕ zero-ℕ) leq-nat-mod-succ-ℕ k (succ-ℕ x) = transitive-leq-ℕ ( nat-Fin (succ-ℕ k) (mod-succ-ℕ k (succ-ℕ x))) @@ -611,8 +611,8 @@ left-zero-law-mul-Fin k x = ( succ-ℕ k) { (nat-Fin (succ-ℕ k) (zero-Fin k)) *ℕ (nat-Fin (succ-ℕ k) x)} { nat-Fin (succ-ℕ k) (zero-Fin k)} - ( ( ap (_*ℕ (nat-Fin (succ-ℕ k) x)) (is-zero-nat-zero-Fin {k})) ∙ - ( inv (is-zero-nat-zero-Fin {k}))))) ∙ + ( ( ap (_*ℕ (nat-Fin (succ-ℕ k) x)) (nat-zero-Fin k)) ∙ + ( inv (nat-zero-Fin k))))) ∙ ( is-section-nat-Fin k (zero-Fin k)) right-zero-law-mul-Fin : diff --git a/src/elementary-number-theory/modular-arithmetic.lagda.md b/src/elementary-number-theory/modular-arithmetic.lagda.md index b63e1fc243f..3921c89047b 100644 --- a/src/elementary-number-theory/modular-arithmetic.lagda.md +++ b/src/elementary-number-theory/modular-arithmetic.lagda.md @@ -150,7 +150,7 @@ abstract is-zero-int-zero-ℤ-Mod : (k : ℕ) → is-zero-ℤ (int-ℤ-Mod k (zero-ℤ-Mod k)) is-zero-int-zero-ℤ-Mod (zero-ℕ) = refl - is-zero-int-zero-ℤ-Mod (succ-ℕ k) = ap int-ℕ (is-zero-nat-zero-Fin {k}) + is-zero-int-zero-ℤ-Mod (succ-ℕ k) = ap int-ℕ (nat-zero-Fin k) int-ℤ-Mod-bounded : (k : ℕ) → (x : ℤ-Mod (succ-ℕ k)) → diff --git a/src/elementary-number-theory/rational-numbers.lagda.md b/src/elementary-number-theory/rational-numbers.lagda.md index 81bfd369b53..d5b08eebd84 100644 --- a/src/elementary-number-theory/rational-numbers.lagda.md +++ b/src/elementary-number-theory/rational-numbers.lagda.md @@ -14,6 +14,7 @@ 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.natural-numbers +open import elementary-number-theory.nonzero-natural-numbers open import elementary-number-theory.positive-and-negative-integers open import elementary-number-theory.positive-integers open import elementary-number-theory.reduced-integer-fractions @@ -117,6 +118,9 @@ pr2 (rational-ℤ x) = is-one-gcd-one-ℤ' x ```agda rational-ℕ : ℕ → ℚ rational-ℕ n = rational-ℤ (int-ℕ n) + +rational-ℕ⁺ : ℕ⁺ → ℚ +rational-ℕ⁺ n = rational-ℕ (nat-ℕ⁺ n) ``` ### Negative one, zero and one diff --git a/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md index 23130c05078..79a689660a3 100644 --- a/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md +++ b/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md @@ -135,7 +135,7 @@ module _ ( sign-homomorphism-Fin-2 n ( Fin-Type-With-Cardinality-ℕ n) ( inv-equiv (inv-equiv f ∘e g)))) +ℕ_) - ( is-zero-nat-zero-Fin {k = 1}) ∙ + ( nat-zero-Fin 1) ∙ ( is-section-nat-Fin 1 ( sign-homomorphism-Fin-2 n ( Fin-Type-With-Cardinality-ℕ n) diff --git a/src/foundation/null-homotopic-maps.lagda.md b/src/foundation/null-homotopic-maps.lagda.md index 23da431fc0c..b2fb80e9b62 100644 --- a/src/foundation/null-homotopic-maps.lagda.md +++ b/src/foundation/null-homotopic-maps.lagda.md @@ -7,6 +7,7 @@ module foundation.null-homotopic-maps where
Imports ```agda +open import foundation.action-on-identifications-functions open import foundation.coherently-constant-maps open import foundation.commuting-triangles-of-identifications open import foundation.constant-maps @@ -14,6 +15,7 @@ open import foundation.dependent-pair-types open import foundation.dependent-products-propositions open import foundation.empty-types open import foundation.equivalences-contractible-types +open import foundation.function-types open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopy-induction open import foundation.identity-types @@ -366,6 +368,21 @@ module _ ( is-null-homotopic-null-homotopic-map f) ``` +### Null-homotopic maps are preserved by left composition + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} + (f : B → C) {g : A → B} + (K@(b , fa=b) : is-null-homotopic-map g) + where + + left-comp-is-null-homotopic-map : is-null-homotopic-map (f ∘ g) + left-comp-is-null-homotopic-map = + ( f b , + λ a → ap f (fa=b a)) +``` + ## See also - Null-homotopic maps are diff --git a/src/lists/finite-sequences.lagda.md b/src/lists/finite-sequences.lagda.md index c481b3bba9e..27f4e84e9db 100644 --- a/src/lists/finite-sequences.lagda.md +++ b/src/lists/finite-sequences.lagda.md @@ -181,7 +181,7 @@ module _ eq-zero-fin-sequence-sequence : (n : ℕ) → fin-sequence-sequence (succ-ℕ n) (zero-Fin n) ＝ u 0 - eq-zero-fin-sequence-sequence n = ap u (is-zero-nat-zero-Fin {n}) + eq-zero-fin-sequence-sequence n = ap u (nat-zero-Fin n) eq-skip-zero-fin-sequence-sequence : (n : ℕ) (i : Fin n) → diff --git a/src/literature/introduction-to-homotopy-type-theory.lagda.md b/src/literature/introduction-to-homotopy-type-theory.lagda.md index 61eb61ff0d1..c03837a988f 100644 --- a/src/literature/introduction-to-homotopy-type-theory.lagda.md +++ b/src/literature/introduction-to-homotopy-type-theory.lagda.md @@ -1202,7 +1202,7 @@ open import elementary-number-theory.modular-arithmetic-standard-finite-types us ```agda open import univalent-combinatorics.standard-finite-types using - ( is-zero-nat-zero-Fin -- ι(zero) = 0 + ( nat-zero-Fin -- ι(zero) = 0 ; nat-skip-zero-Fin -- ι(skip-zero x) = ι(x) + 1 ) open import elementary-number-theory.modular-arithmetic-standard-finite-types using diff --git a/src/order-theory/least-upper-bounds-large-posets.lagda.md b/src/order-theory/least-upper-bounds-large-posets.lagda.md index dfa918f385f..3532cb35f1d 100644 --- a/src/order-theory/least-upper-bounds-large-posets.lagda.md +++ b/src/order-theory/least-upper-bounds-large-posets.lagda.md @@ -10,8 +10,10 @@ module order-theory.least-upper-bounds-large-posets where open import foundation.dependent-pair-types open import foundation.function-types open import foundation.logical-equivalences +open import foundation.transport-along-identifications open import foundation.type-arithmetic-cartesian-product-types open import foundation.universe-levels +open import foundation.weakly-constant-maps open import order-theory.dependent-products-large-posets open import order-theory.large-posets @@ -373,3 +375,34 @@ module _ is-binary-least-upper-bound-swap-Large-Poset P y x x ( left-leq-right-least-upper-bound-Large-Poset y x y≤x) ``` + +### If a family of elements is weakly constant, any of its elements is a least upper bound + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} + (P : Large-Poset α β) + {l1 l2 : Level} {I : UU l1} (x : I → type-Large-Poset P l2) + (wc-x : is-weakly-constant-map x) + (i : I) + where abstract + + is-least-upper-bound-element-weakly-constant-family-of-elements-Large-Poset : + is-least-upper-bound-family-of-elements-Large-Poset + ( P) + ( x) + ( x i) + pr1 + ( is-least-upper-bound-element-weakly-constant-family-of-elements-Large-Poset + y) + x≤y = + x≤y i + pr2 + ( is-least-upper-bound-element-weakly-constant-family-of-elements-Large-Poset + y) + xi≤y j = + tr + ( λ z → leq-Large-Poset P z y) + ( wc-x i j) + ( xi≤y) +``` diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index 70392e7ce97..c1b50147fdd 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -138,6 +138,7 @@ open import real-numbers.similarity-positive-real-numbers public open import real-numbers.similarity-real-numbers public open import real-numbers.square-roots-nonnegative-real-numbers public open import real-numbers.squares-real-numbers public +open import real-numbers.standard-uniform-partitions-closed-intervals-real-numbers public open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers public open import real-numbers.strict-inequality-nonnegative-real-numbers public open import real-numbers.strict-inequality-positive-real-numbers public @@ -152,9 +153,11 @@ open import real-numbers.suprema-families-real-numbers public open import real-numbers.totally-bounded-subsets-real-numbers public open import real-numbers.transposition-addition-subtraction-cuts-dedekind-real-numbers public open import real-numbers.uniform-homeomorphism-unit-interval-proper-closed-interval-real-numbers public +open import real-numbers.uniform-partitions-closed-intervals-real-numbers public open import real-numbers.uniformly-continuous-endomaps-real-numbers public open import real-numbers.uniformly-continuous-real-maps-proper-closed-intervals-real-numbers public open import real-numbers.unit-closed-interval-real-numbers public +open import real-numbers.unit-fractions-real-numbers public open import real-numbers.upper-dedekind-real-numbers public open import real-numbers.zero-nonnegative-real-numbers public open import real-numbers.zero-real-numbers public diff --git a/src/real-numbers/maximum-finite-families-nonnegative-real-numbers.lagda.md b/src/real-numbers/maximum-finite-families-nonnegative-real-numbers.lagda.md index a922197ecc1..980580b1c5f 100644 --- a/src/real-numbers/maximum-finite-families-nonnegative-real-numbers.lagda.md +++ b/src/real-numbers/maximum-finite-families-nonnegative-real-numbers.lagda.md @@ -11,19 +11,23 @@ module real-numbers.maximum-finite-families-nonnegative-real-numbers where ```agda open import elementary-number-theory.natural-numbers +open import foundation.identity-types open import foundation.universe-levels +open import foundation.weakly-constant-maps open import lists.finite-sequences open import order-theory.join-semilattices open import order-theory.joins-finite-families-large-join-semilattices open import order-theory.least-upper-bounds-large-posets +open import order-theory.similarity-of-elements-large-posets open import real-numbers.binary-maximum-nonnegative-real-numbers open import real-numbers.inequality-nonnegative-real-numbers open import real-numbers.nonnegative-real-numbers open import univalent-combinatorics.finite-types +open import univalent-combinatorics.standard-finite-types ```
@@ -109,3 +113,56 @@ module _ ( I) ( f) ``` + +### If a finite family of nonnegative real numbers is weakly constant, any of its elements are equal to the maximum + +```agda +module _ + {l1 l2 : Level} (I : Finite-Type l1) + (f : type-Finite-Type I → ℝ⁰⁺ l2) + (wc-f : is-weakly-constant-map f) + (i : type-Finite-Type I) + where abstract + + max-weakly-constant-finite-family-ℝ⁰⁺ : max-finite-family-ℝ⁰⁺ I f ＝ f i + max-weakly-constant-finite-family-ℝ⁰⁺ = + eq-sim-Large-Poset + ( large-poset-ℝ⁰⁺) + ( max-finite-family-ℝ⁰⁺ I f) + ( f i) + ( sim-is-least-upper-bound-family-of-elements-Large-Poset + ( large-poset-ℝ⁰⁺) + ( is-least-upper-bound-max-finite-family-ℝ⁰⁺ I f) + ( is-least-upper-bound-element-weakly-constant-family-of-elements-Large-Poset + ( large-poset-ℝ⁰⁺) + ( f) + ( wc-f) + ( i))) +``` + +### If a finite sequence of nonnegative real numbers is weakly constant, any of its elements are equal to the maximum + +```agda +module _ + {l : Level} + (n : ℕ) + (f : fin-sequence (ℝ⁰⁺ l) n) + (wc-f : is-weakly-constant-map f) + (i : Fin n) + where abstract + + max-weakly-constant-fin-sequence-ℝ⁰⁺ : max-fin-sequence-ℝ⁰⁺ n f ＝ f i + max-weakly-constant-fin-sequence-ℝ⁰⁺ = + eq-sim-Large-Poset + ( large-poset-ℝ⁰⁺) + ( max-fin-sequence-ℝ⁰⁺ n f) + ( f i) + ( sim-is-least-upper-bound-family-of-elements-Large-Poset + ( large-poset-ℝ⁰⁺) + ( is-least-upper-bound-max-fin-sequence-ℝ⁰⁺ n f) + ( is-least-upper-bound-element-weakly-constant-family-of-elements-Large-Poset + ( large-poset-ℝ⁰⁺) + ( f) + ( wc-f) + ( i))) +``` diff --git a/src/real-numbers/partitions-closed-intervals-real-numbers.lagda.md b/src/real-numbers/partitions-closed-intervals-real-numbers.lagda.md index 899080c34eb..8ff4b4dd6a2 100644 --- a/src/real-numbers/partitions-closed-intervals-real-numbers.lagda.md +++ b/src/real-numbers/partitions-closed-intervals-real-numbers.lagda.md @@ -18,6 +18,7 @@ open import foundation.dependent-pair-types open import foundation.function-types open import foundation.identity-types open import foundation.logical-equivalences +open import foundation.raising-universe-levels-unit-type open import foundation.transport-along-identifications open import foundation.unit-type open import foundation.universe-levels diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md index 744a7c58851..e9509f45c82 100644 --- a/src/real-numbers/rational-real-numbers.lagda.md +++ b/src/real-numbers/rational-real-numbers.lagda.md @@ -12,6 +12,7 @@ module real-numbers.rational-real-numbers where open import elementary-number-theory.integers open import elementary-number-theory.natural-numbers open import elementary-number-theory.nonnegative-rational-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 @@ -96,6 +97,9 @@ real-ℤ x = real-ℚ (rational-ℤ x) ```agda real-ℕ : ℕ → ℝ lzero real-ℕ n = real-ℤ (int-ℕ n) + +real-ℕ⁺ : ℕ⁺ → ℝ lzero +real-ℕ⁺ n = real-ℕ (nat-ℕ⁺ n) ``` ### Zero as a real number diff --git a/src/real-numbers/standard-uniform-partitions-closed-intervals-real-numbers.lagda.md b/src/real-numbers/standard-uniform-partitions-closed-intervals-real-numbers.lagda.md new file mode 100644 index 00000000000..dc5cf28c82d --- /dev/null +++ b/src/real-numbers/standard-uniform-partitions-closed-intervals-real-numbers.lagda.md @@ -0,0 +1,251 @@ +# The standard uniform partitions of closed intervals in the real numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.standard-uniform-partitions-closed-intervals-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.inequality-standard-finite-types +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.null-homotopic-maps +open import foundation.unit-type +open import foundation.universe-levels +open import foundation.weakly-constant-maps + +open import group-theory.abelian-groups + +open import lists.arrays +open import lists.finite-sequences +open import lists.nonempty-arrays + +open import order-theory.increasing-finite-sequences-posets +open import order-theory.increasing-nonempty-arrays-posets + +open import real-numbers.addition-real-numbers +open import real-numbers.closed-intervals-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.difference-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.large-additive-group-of-real-numbers +open import real-numbers.multiplication-nonnegative-real-numbers +open import real-numbers.multiplication-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.partitions-closed-intervals-real-numbers +open import real-numbers.positive-and-negative-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.similarity-real-numbers +open import real-numbers.uniform-partitions-closed-intervals-real-numbers +open import real-numbers.unit-fractions-real-numbers + +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +Given a [natural number](elementary-number-theory.natural-numbers.md) `n` and a +[closed interval](real-numbers.closed-intervals-real-numbers.md) `[a, b]` in the +[real numbers](real-numbers.dedekind-real-numbers.md), the +{{#concept "standard uniform partition" Disambiguation="of a given length closed interval in the real numbers" Agda=standard-uniform-partition-closed-interval-ℝ}} +of `[a, b]` contains `n + 1` intervals, each of width `(b - a) / (n + 1)`. + +## Definition + +```agda +module _ + {l : Level} + ([a,b]@((a , b) , a≤b) : closed-interval-ℝ l l) + (n : ℕ) + (let 1/⟨n+1⟩ = reciprocal-real-succ-ℕ n) + where + + fin-sequence-standard-uniform-partition-closed-interval-ℝ : + fin-sequence (ℝ l) (n +ℕ 2) + fin-sequence-standard-uniform-partition-closed-interval-ℝ i = + a +ℝ (b -ℝ a) *ℝ 1/⟨n+1⟩ *ℝ real-ℕ (nat-Fin (n +ℕ 2) i) + + abstract + is-increasing-fin-sequence-standard-uniform-partition-closed-interval-ℝ : + is-increasing-fin-sequence-type-Poset + ( ℝ-Poset l) + ( n +ℕ 2) + ( fin-sequence-standard-uniform-partition-closed-interval-ℝ) + is-increasing-fin-sequence-standard-uniform-partition-closed-interval-ℝ + i j i≤j = + preserves-leq-left-add-ℝ a _ _ + ( preserves-leq-left-mul-ℝ⁰⁺ + ( nonnegative-diff-leq-ℝ a≤b *ℝ⁰⁺ + nonnegative-ℝ⁺ (positive-reciprocal-real-succ-ℕ n)) + ( preserves-leq-real-ℕ (preserves-leq-nat-Fin (n +ℕ 2) {i} {j} i≤j))) + + array-standard-uniform-partition-closed-interval-ℝ : array (ℝ l) + array-standard-uniform-partition-closed-interval-ℝ = + ( n +ℕ 2 , fin-sequence-standard-uniform-partition-closed-interval-ℝ) + + nonempty-array-standard-uniform-partition-closed-interval-ℝ : + nonempty-array (ℝ l) + nonempty-array-standard-uniform-partition-closed-interval-ℝ = + ( array-standard-uniform-partition-closed-interval-ℝ , + star) + + increasing-nonempty-array-standard-uniform-partition-closed-interval-ℝ : + increasing-nonempty-array-type-Poset (ℝ-Poset l) + increasing-nonempty-array-standard-uniform-partition-closed-interval-ℝ = + ( nonempty-array-standard-uniform-partition-closed-interval-ℝ , + is-increasing-fin-sequence-standard-uniform-partition-closed-interval-ℝ) + + abstract + is-lower-bound-last-fin-sequence-standard-uniform-partition-closed-interval-ℝ : + last-fin-sequence + ( succ-ℕ n) + ( fin-sequence-standard-uniform-partition-closed-interval-ℝ) ＝ + lower-bound-closed-interval-ℝ [a,b] + is-lower-bound-last-fin-sequence-standard-uniform-partition-closed-interval-ℝ = + eq-sim-ℝ + ( similarity-reasoning-ℝ + ( a) +ℝ + ( (b -ℝ a) *ℝ + 1/⟨n+1⟩ *ℝ + real-ℕ (nat-Fin (n +ℕ 2) (zero-Fin (succ-ℕ n)))) + ~ℝ a +ℝ (b -ℝ a) *ℝ 1/⟨n+1⟩ *ℝ zero-ℝ + by + sim-eq-ℝ + ( ap-add-ℝ + ( refl) + ( ap-mul-ℝ refl (ap real-ℕ (nat-zero-Fin (n +ℕ 2))))) + ~ℝ a +ℝ zero-ℝ + by preserves-sim-left-add-ℝ a _ _ (right-zero-law-mul-ℝ _) + ~ℝ a + by sim-eq-ℝ (right-unit-law-add-ℝ a)) + + is-upper-bound-head-fin-sequence-standard-uniform-partition-closed-interval-ℝ : + head-fin-sequence + ( succ-ℕ n) + ( fin-sequence-standard-uniform-partition-closed-interval-ℝ) ＝ + b + is-upper-bound-head-fin-sequence-standard-uniform-partition-closed-interval-ℝ = + equational-reasoning + a +ℝ (b -ℝ a) *ℝ 1/⟨n+1⟩ *ℝ real-ℕ (succ-ℕ n) + ＝ a +ℝ (b -ℝ a) *ℝ (1/⟨n+1⟩ *ℝ real-ℕ (succ-ℕ n)) + by ap-add-ℝ refl (associative-mul-ℝ _ _ _) + ＝ a +ℝ (b -ℝ a) *ℝ one-ℝ + by + ap-add-ℝ + ( refl) + ( ap-mul-ℝ refl (left-inverse-law-reciprocal-real-succ-ℕ n)) + ＝ a +ℝ (b -ℝ a) + by ap-add-ℝ refl (right-unit-law-mul-ℝ _) + ＝ b + by eq-sim-ℝ (cancel-right-conjugation-ℝ a b) + + partition-standard-uniform-partition-closed-interval-ℝ : + partition-closed-interval-ℝ [a,b] + partition-standard-uniform-partition-closed-interval-ℝ = + ( increasing-nonempty-array-standard-uniform-partition-closed-interval-ℝ , + is-lower-bound-last-fin-sequence-standard-uniform-partition-closed-interval-ℝ , + is-upper-bound-head-fin-sequence-standard-uniform-partition-closed-interval-ℝ) + + nonnegative-width-standard-uniform-partition-closed-interval-ℝ : ℝ⁰⁺ l + nonnegative-width-standard-uniform-partition-closed-interval-ℝ = + nonnegative-width-closed-interval-ℝ [a,b] *ℝ⁰⁺ + nonnegative-reciprocal-real-succ-ℕ n + + abstract + compute-diffs-partition-standard-uniform-partition-closed-interval-ℝ : + (i : Fin (succ-ℕ n)) → + diffs-partition-closed-interval-ℝ + ( [a,b]) + ( partition-standard-uniform-partition-closed-interval-ℝ) + ( i) ＝ + nonnegative-width-closed-interval-ℝ [a,b] *ℝ⁰⁺ + nonnegative-reciprocal-real-succ-ℕ n + compute-diffs-partition-standard-uniform-partition-closed-interval-ℝ i = + let + iℕ = nat-Fin (n +ℕ 2) (inl-Fin (succ-ℕ n) i) + jℕ = nat-Fin (n +ℕ 2) (inr-Fin (succ-ℕ n) i) + in + eq-ℝ⁰⁺ _ _ + ( equational-reasoning + ( a +ℝ (b -ℝ a) *ℝ 1/⟨n+1⟩ *ℝ real-ℕ jℕ) -ℝ + ( a +ℝ (b -ℝ a) *ℝ 1/⟨n+1⟩ *ℝ real-ℕ iℕ) + ＝ + ((b -ℝ a) *ℝ 1/⟨n+1⟩ *ℝ real-ℕ jℕ) -ℝ + ((b -ℝ a) *ℝ 1/⟨n+1⟩ *ℝ real-ℕ iℕ) + by right-subtraction-left-add-Ab (ab-add-ℝ l) _ _ _ + ＝ + ((b -ℝ a) *ℝ 1/⟨n+1⟩) *ℝ (real-ℕ jℕ -ℝ real-ℕ iℕ) + by + inv + ( left-distributive-mul-diff-ℝ + ( (b -ℝ a) *ℝ 1/⟨n+1⟩) + ( real-ℕ jℕ) + ( real-ℕ iℕ)) + ＝ + ((b -ℝ a) *ℝ 1/⟨n+1⟩) *ℝ (real-ℕ (succ-ℕ iℕ) -ℝ real-ℕ iℕ) + by + ap-mul-ℝ + { l1 = l} + ( refl) + { l2 = lzero} + ( ap-diff-ℝ (ap real-ℕ (nat-inr-Fin (succ-ℕ n) i)) refl) + ＝ + ( (b -ℝ a) *ℝ 1/⟨n+1⟩) *ℝ + ( (real-ℕ iℕ +ℝ one-ℝ) -ℝ real-ℕ iℕ) + by + ap-mul-ℝ + { l1 = l} + ( refl) + { l2 = lzero} + ( ap-diff-ℝ (inv (add-real-ℕ iℕ 1)) refl) + ＝ ((b -ℝ a) *ℝ 1/⟨n+1⟩) *ℝ one-ℝ + by + ap-mul-ℝ + { l1 = l} + ( refl) + { l2 = lzero} + ( eq-sim-ℝ (cancel-left-conjugation-ℝ (real-ℕ iℕ) one-ℝ)) + ＝ (b -ℝ a) *ℝ 1/⟨n+1⟩ + by right-unit-law-mul-ℝ _) + + is-null-homotopic-map-diffs-partition-standard-uniform-partition-closed-interval-ℝ : + is-null-homotopic-map + ( diffs-partition-closed-interval-ℝ + ( [a,b]) + ( partition-standard-uniform-partition-closed-interval-ℝ)) + is-null-homotopic-map-diffs-partition-standard-uniform-partition-closed-interval-ℝ = + ( nonnegative-width-standard-uniform-partition-closed-interval-ℝ , + compute-diffs-partition-standard-uniform-partition-closed-interval-ℝ) + + is-uniform-partition-standard-uniform-partition-closed-interval-ℝ : + is-uniform-partition-closed-interval-ℝ + ( [a,b]) + ( partition-standard-uniform-partition-closed-interval-ℝ) + is-uniform-partition-standard-uniform-partition-closed-interval-ℝ = + is-weakly-constant-map-is-null-homotopic-map + ( left-comp-is-null-homotopic-map + ( real-ℝ⁰⁺) + ( is-null-homotopic-map-diffs-partition-standard-uniform-partition-closed-interval-ℝ)) + + standard-uniform-partition-closed-interval-ℝ : + uniform-partition-closed-interval-ℝ [a,b] + standard-uniform-partition-closed-interval-ℝ = + ( partition-standard-uniform-partition-closed-interval-ℝ , + is-uniform-partition-standard-uniform-partition-closed-interval-ℝ) +``` + +## Properties + +### Every nonempty uniform partition of a closed interval is standard + +This has yet to be proven. diff --git a/src/real-numbers/uniform-partitions-closed-intervals-real-numbers.lagda.md b/src/real-numbers/uniform-partitions-closed-intervals-real-numbers.lagda.md new file mode 100644 index 00000000000..5efb97a88b5 --- /dev/null +++ b/src/real-numbers/uniform-partitions-closed-intervals-real-numbers.lagda.md @@ -0,0 +1,161 @@ +# Uniform partitions of closed intervals in the real numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.uniform-partitions-closed-intervals-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.identity-types +open import foundation.null-homotopic-maps +open import foundation.subtypes +open import foundation.universe-levels +open import foundation.weakly-constant-maps + +open import lists.finite-sequences + +open import order-theory.least-upper-bounds-large-posets +open import order-theory.similarity-of-elements-large-posets + +open import real-numbers.closed-intervals-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.inequality-nonnegative-real-numbers +open import real-numbers.maximum-finite-families-nonnegative-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.partitions-closed-intervals-real-numbers + +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +A {{#concept "uniform partition" Agda=uniform-partition-closed-interval-ℝ}} of a +[closed interval](real-numbers.closed-intervals-real-numbers.md) `[a, b]` in the +[real numbers](real-numbers.dedekind-real-numbers.md) is a +[partition](real-numbers.partitions-closed-intervals-real-numbers.md) in which +the widths of the component intervals are +[weakly constant](foundation.weakly-constant-maps.md). + +## Definition + +```agda +module _ + {l : Level} + ([a,b] : closed-interval-ℝ l l) + where + + is-uniform-prop-partition-closed-interval-ℝ : + subtype (lsuc l) (partition-closed-interval-ℝ [a,b]) + is-uniform-prop-partition-closed-interval-ℝ p = + is-weakly-constant-map-prop-Set + ( ℝ-Set l) + ( width-closed-interval-ℝ ∘ + fin-sequence-closed-interval-partition-closed-interval-ℝ [a,b] p) + + is-uniform-partition-closed-interval-ℝ : + partition-closed-interval-ℝ [a,b] → UU (lsuc l) + is-uniform-partition-closed-interval-ℝ = + is-in-subtype is-uniform-prop-partition-closed-interval-ℝ + + uniform-partition-closed-interval-ℝ : UU (lsuc l) + uniform-partition-closed-interval-ℝ = + type-subtype is-uniform-prop-partition-closed-interval-ℝ +``` + +## Properties + +### Properties inherited from all partitions + +```agda +module _ + {l : Level} + ([a,b] : closed-interval-ℝ l l) + (up@(p , is-uniform-p) : + uniform-partition-closed-interval-ℝ [a,b]) + where + + partition-uniform-partition-closed-interval-ℝ : + partition-closed-interval-ℝ [a,b] + partition-uniform-partition-closed-interval-ℝ = p + + pred-length-uniform-partition-closed-interval-ℝ : ℕ + pred-length-uniform-partition-closed-interval-ℝ = + pred-length-partition-closed-interval-ℝ [a,b] p + + length-uniform-partition-closed-interval-ℝ : ℕ + length-uniform-partition-closed-interval-ℝ = + length-partition-closed-interval-ℝ [a,b] p + + fin-sequence-closed-interval-uniform-partition-closed-interval-ℝ : + fin-sequence + ( closed-interval-ℝ l l) + ( pred-length-uniform-partition-closed-interval-ℝ) + fin-sequence-closed-interval-uniform-partition-closed-interval-ℝ = + fin-sequence-closed-interval-partition-closed-interval-ℝ [a,b] p + + fin-sequence-nonnegative-width-closed-interval-uniform-partition-closed-interval-ℝ : + fin-sequence (ℝ⁰⁺ l) (pred-length-uniform-partition-closed-interval-ℝ) + fin-sequence-nonnegative-width-closed-interval-uniform-partition-closed-interval-ℝ = + nonnegative-width-closed-interval-ℝ ∘ + fin-sequence-closed-interval-uniform-partition-closed-interval-ℝ + + abstract + is-weakly-constant-fin-sequence-nonnegative-width-closed-interval-uniform-partition-closed-interval-ℝ : + is-weakly-constant-map + ( fin-sequence-nonnegative-width-closed-interval-uniform-partition-closed-interval-ℝ) + is-weakly-constant-fin-sequence-nonnegative-width-closed-interval-uniform-partition-closed-interval-ℝ + i j = + eq-ℝ⁰⁺ _ _ (is-uniform-p i j) +``` + +### The width of partitions in a uniform partition + +If the partition is trivial, containing no partitions because it is a partition +of a singleton interval `[a, a]`, we define the width of the partitions to be +zero. + +```agda +module _ + {l : Level} + ([a,b] : closed-interval-ℝ l l) + (up@(p , is-uniform-p) : + uniform-partition-closed-interval-ℝ [a,b]) + where + + nonnegative-width-interval-uniform-partition-closed-interval-ℝ : ℝ⁰⁺ l + nonnegative-width-interval-uniform-partition-closed-interval-ℝ = + mesh-partition-closed-interval-ℝ [a,b] p + + width-interval-uniform-partition-closed-interval-ℝ : ℝ l + width-interval-uniform-partition-closed-interval-ℝ = + real-ℝ⁰⁺ nonnegative-width-interval-uniform-partition-closed-interval-ℝ + + is-null-homotopic-fin-sequence-nonnegative-width-closed-interval-uniform-partition-closed-interval-ℝ : + is-null-homotopic-map + ( fin-sequence-nonnegative-width-closed-interval-uniform-partition-closed-interval-ℝ + ( [a,b]) + ( up)) + pr1 + is-null-homotopic-fin-sequence-nonnegative-width-closed-interval-uniform-partition-closed-interval-ℝ = + nonnegative-width-interval-uniform-partition-closed-interval-ℝ + pr2 + is-null-homotopic-fin-sequence-nonnegative-width-closed-interval-uniform-partition-closed-interval-ℝ + i = + inv + ( max-weakly-constant-fin-sequence-ℝ⁰⁺ + ( pred-length-uniform-partition-closed-interval-ℝ [a,b] up) + ( diffs-partition-closed-interval-ℝ [a,b] p) + ( is-weakly-constant-fin-sequence-nonnegative-width-closed-interval-uniform-partition-closed-interval-ℝ + ( [a,b]) + ( up)) + ( i)) +``` diff --git a/src/real-numbers/unit-fractions-real-numbers.lagda.md b/src/real-numbers/unit-fractions-real-numbers.lagda.md new file mode 100644 index 00000000000..10591f3285f --- /dev/null +++ b/src/real-numbers/unit-fractions-real-numbers.lagda.md @@ -0,0 +1,82 @@ +# Unit fractions in the real numbers + +```agda +module real-numbers.unit-fractions-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.multiplication-rational-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-natural-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.unit-fractions-rational-numbers + +open import foundation.action-on-identifications-functions +open import foundation.identity-types +open import foundation.universe-levels + +open import real-numbers.dedekind-real-numbers +open import real-numbers.multiplication-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.positive-and-negative-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.rational-real-numbers +``` + +
+ +## Idea + +A {{#concept "unit fraction" Disambiguation="in the real numbers"}} in the +[real numbers](real-numbers.dedekind-real-numbers.md) is the +[real embedding](real-numbers.rational-real-numbers.md) of a +[rational unit fraction](elementary-number-theory.unit-fractions-rational-numbers.md). + +## Definition + +```agda +positive-reciprocal-real-ℕ⁺ : ℕ⁺ → ℝ⁺ lzero +positive-reciprocal-real-ℕ⁺ n = + positive-real-ℚ⁺ (positive-reciprocal-rational-ℕ⁺ n) + +reciprocal-real-ℕ⁺ : ℕ⁺ → ℝ lzero +reciprocal-real-ℕ⁺ n = real-ℝ⁺ (positive-reciprocal-real-ℕ⁺ n) + +positive-reciprocal-real-succ-ℕ : ℕ → ℝ⁺ lzero +positive-reciprocal-real-succ-ℕ n = + positive-reciprocal-real-ℕ⁺ (succ-nonzero-ℕ' n) + +nonnegative-reciprocal-real-succ-ℕ : ℕ → ℝ⁰⁺ lzero +nonnegative-reciprocal-real-succ-ℕ n = + nonnegative-ℝ⁺ (positive-reciprocal-real-succ-ℕ n) + +reciprocal-real-succ-ℕ : ℕ → ℝ lzero +reciprocal-real-succ-ℕ n = real-ℝ⁺ (positive-reciprocal-real-succ-ℕ n) +``` + +## Properties + +### Inverse laws + +```agda +module _ + (n : ℕ⁺) + where abstract + + left-inverse-law-reciprocal-real-ℕ⁺ : + reciprocal-real-ℕ⁺ n *ℝ real-ℕ⁺ n ＝ one-ℝ + left-inverse-law-reciprocal-real-ℕ⁺ = + ( mul-real-ℚ _ _) ∙ + ( ap real-ℚ (left-inverse-law-reciprocal-rational-ℕ⁺ n)) + +module _ + (n : ℕ) + where abstract + + left-inverse-law-reciprocal-real-succ-ℕ : + reciprocal-real-succ-ℕ n *ℝ real-ℕ (succ-ℕ n) ＝ one-ℝ + left-inverse-law-reciprocal-real-succ-ℕ = + left-inverse-law-reciprocal-real-ℕ⁺ (succ-nonzero-ℕ' n) +``` diff --git a/src/ring-theory/binomial-theorem-semirings.lagda.md b/src/ring-theory/binomial-theorem-semirings.lagda.md index ad5ee693984..d4bfaadb866 100644 --- a/src/ring-theory/binomial-theorem-semirings.lagda.md +++ b/src/ring-theory/binomial-theorem-semirings.lagda.md @@ -369,7 +369,7 @@ module _ ( power-Semiring R ( dist-ℕ m (succ-ℕ (succ-ℕ n))) ( y)))) - ( is-zero-nat-zero-Fin {n})) ∙ + ( nat-zero-Fin n)) ∙ ( ( left-unit-law-multiple-Semiring R ( mul-Semiring R ( one-Semiring R) @@ -568,7 +568,7 @@ binomial-theorem-Semiring R (succ-ℕ (succ-ℕ n)) x y H = ( power-Semiring R ( dist-ℕ m (succ-ℕ (succ-ℕ n))) ( y)))) - ( is-zero-nat-zero-Fin {n})) ∙ + ( nat-zero-Fin n)) ∙ ( ( left-unit-law-multiple-Semiring R ( mul-Semiring R ( one-Semiring R) diff --git a/src/univalent-combinatorics/standard-finite-types.lagda.md b/src/univalent-combinatorics/standard-finite-types.lagda.md index 5b68a49e080..b86e62890ee 100644 --- a/src/univalent-combinatorics/standard-finite-types.lagda.md +++ b/src/univalent-combinatorics/standard-finite-types.lagda.md @@ -291,25 +291,26 @@ pr2 (emb-nat-Fin k) = is-emb-nat-Fin k ``` ```agda -is-zero-nat-zero-Fin : {k : ℕ} → is-zero-ℕ (nat-Fin (succ-ℕ k) (zero-Fin k)) -is-zero-nat-zero-Fin {zero-ℕ} = refl -is-zero-nat-zero-Fin {succ-ℕ k} = is-zero-nat-zero-Fin {k} +abstract + nat-zero-Fin : (k : ℕ) → is-zero-ℕ (nat-Fin (succ-ℕ k) (zero-Fin k)) + nat-zero-Fin zero-ℕ = refl + nat-zero-Fin (succ-ℕ k) = nat-zero-Fin k + + nat-inr-Fin : + (k : ℕ) (x : Fin k) → + nat-Fin (succ-ℕ k) (inr-Fin k x) ＝ succ-ℕ (nat-Fin k x) + nat-inr-Fin (succ-ℕ k) (inl x) = nat-inr-Fin k x + nat-inr-Fin (succ-ℕ k) (inr star) = refl nat-skip-zero-Fin : (k : ℕ) (x : Fin k) → nat-Fin (succ-ℕ k) (skip-zero-Fin k x) ＝ succ-ℕ (nat-Fin k x) -nat-skip-zero-Fin (succ-ℕ k) (inl x) = nat-skip-zero-Fin k x -nat-skip-zero-Fin (succ-ℕ k) (inr star) = refl +nat-skip-zero-Fin = nat-inr-Fin nat-succ-Fin : (k : ℕ) (x : Fin k) → nat-Fin (succ-ℕ k) (succ-Fin (succ-ℕ k) (inl x)) ＝ succ-ℕ (nat-Fin k x) nat-succ-Fin k x = nat-skip-zero-Fin k x - -nat-inr-Fin : - (k : ℕ) (x : Fin k) → nat-Fin (succ-ℕ k) (inr-Fin k x) ＝ succ-ℕ (nat-Fin k x) -nat-inr-Fin (succ-ℕ k) (inl x) = nat-inr-Fin k x -nat-inr-Fin (succ-ℕ k) (inr star) = refl ``` ```agda @@ -453,7 +454,7 @@ leq-nat-succ-Fin (succ-ℕ k) (inl x) = leq-nat-succ-Fin (succ-ℕ k) (inr star) = concatenate-eq-leq-ℕ ( succ-ℕ (nat-Fin (succ-ℕ k) (inr star))) - ( is-zero-nat-zero-Fin {succ-ℕ k}) + ( nat-zero-Fin (succ-ℕ k)) ( leq-zero-ℕ (succ-ℕ (nat-Fin (succ-ℕ k) (inr star)))) ``` From dd8e7468152f725cddcf352fc735712914535383 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Wed, 10 Jun 2026 17:51:37 -0700 Subject: [PATCH 14/14] Compute the mesh of the standard uniform partition --- ...ons-closed-intervals-real-numbers.lagda.md | 26 ++++++++++++++++--- ...ons-closed-intervals-real-numbers.lagda.md | 12 ++++----- 2 files changed, 29 insertions(+), 9 deletions(-) diff --git a/src/real-numbers/standard-uniform-partitions-closed-intervals-real-numbers.lagda.md b/src/real-numbers/standard-uniform-partitions-closed-intervals-real-numbers.lagda.md index dc5cf28c82d..6a31ce75f5a 100644 --- a/src/real-numbers/standard-uniform-partitions-closed-intervals-real-numbers.lagda.md +++ b/src/real-numbers/standard-uniform-partitions-closed-intervals-real-numbers.lagda.md @@ -37,6 +37,7 @@ open import real-numbers.difference-real-numbers open import real-numbers.inequalities-addition-and-subtraction-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.large-additive-group-of-real-numbers +open import real-numbers.maximum-finite-families-nonnegative-real-numbers open import real-numbers.multiplication-nonnegative-real-numbers open import real-numbers.multiplication-real-numbers open import real-numbers.nonnegative-real-numbers @@ -156,8 +157,8 @@ module _ is-lower-bound-last-fin-sequence-standard-uniform-partition-closed-interval-ℝ , is-upper-bound-head-fin-sequence-standard-uniform-partition-closed-interval-ℝ) - nonnegative-width-standard-uniform-partition-closed-interval-ℝ : ℝ⁰⁺ l - nonnegative-width-standard-uniform-partition-closed-interval-ℝ = + mesh-standard-uniform-partition-closed-interval-ℝ : ℝ⁰⁺ l + mesh-standard-uniform-partition-closed-interval-ℝ = nonnegative-width-closed-interval-ℝ [a,b] *ℝ⁰⁺ nonnegative-reciprocal-real-succ-ℕ n @@ -224,7 +225,7 @@ module _ ( [a,b]) ( partition-standard-uniform-partition-closed-interval-ℝ)) is-null-homotopic-map-diffs-partition-standard-uniform-partition-closed-interval-ℝ = - ( nonnegative-width-standard-uniform-partition-closed-interval-ℝ , + ( mesh-standard-uniform-partition-closed-interval-ℝ , compute-diffs-partition-standard-uniform-partition-closed-interval-ℝ) is-uniform-partition-standard-uniform-partition-closed-interval-ℝ : @@ -242,6 +243,25 @@ module _ standard-uniform-partition-closed-interval-ℝ = ( partition-standard-uniform-partition-closed-interval-ℝ , is-uniform-partition-standard-uniform-partition-closed-interval-ℝ) + + abstract + compute-mesh-standard-uniform-partition-closed-interval-ℝ : + mesh-uniform-partition-closed-interval-ℝ + ( [a,b]) + ( standard-uniform-partition-closed-interval-ℝ) ＝ + mesh-standard-uniform-partition-closed-interval-ℝ + compute-mesh-standard-uniform-partition-closed-interval-ℝ = + max-weakly-constant-fin-sequence-ℝ⁰⁺ + ( succ-ℕ n) + ( diffs-partition-closed-interval-ℝ + ( [a,b]) + ( partition-standard-uniform-partition-closed-interval-ℝ)) + ( is-weakly-constant-fin-sequence-nonnegative-width-closed-interval-uniform-partition-closed-interval-ℝ + ( [a,b]) + ( standard-uniform-partition-closed-interval-ℝ)) + ( neg-one-Fin n) ∙ + compute-diffs-partition-standard-uniform-partition-closed-interval-ℝ + ( neg-one-Fin n) ``` ## Properties diff --git a/src/real-numbers/uniform-partitions-closed-intervals-real-numbers.lagda.md b/src/real-numbers/uniform-partitions-closed-intervals-real-numbers.lagda.md index 5efb97a88b5..7ae48bde791 100644 --- a/src/real-numbers/uniform-partitions-closed-intervals-real-numbers.lagda.md +++ b/src/real-numbers/uniform-partitions-closed-intervals-real-numbers.lagda.md @@ -131,13 +131,13 @@ module _ uniform-partition-closed-interval-ℝ [a,b]) where - nonnegative-width-interval-uniform-partition-closed-interval-ℝ : ℝ⁰⁺ l - nonnegative-width-interval-uniform-partition-closed-interval-ℝ = + mesh-uniform-partition-closed-interval-ℝ : ℝ⁰⁺ l + mesh-uniform-partition-closed-interval-ℝ = mesh-partition-closed-interval-ℝ [a,b] p - width-interval-uniform-partition-closed-interval-ℝ : ℝ l - width-interval-uniform-partition-closed-interval-ℝ = - real-ℝ⁰⁺ nonnegative-width-interval-uniform-partition-closed-interval-ℝ + real-mesh-interval-uniform-partition-closed-interval-ℝ : ℝ l + real-mesh-interval-uniform-partition-closed-interval-ℝ = + real-ℝ⁰⁺ mesh-uniform-partition-closed-interval-ℝ is-null-homotopic-fin-sequence-nonnegative-width-closed-interval-uniform-partition-closed-interval-ℝ : is-null-homotopic-map @@ -146,7 +146,7 @@ module _ ( up)) pr1 is-null-homotopic-fin-sequence-nonnegative-width-closed-interval-uniform-partition-closed-interval-ℝ = - nonnegative-width-interval-uniform-partition-closed-interval-ℝ + mesh-uniform-partition-closed-interval-ℝ pr2 is-null-homotopic-fin-sequence-nonnegative-width-closed-interval-uniform-partition-closed-interval-ℝ i =