diff --git a/src/commutative-algebra/geometric-sequences-commutative-semirings.lagda.md b/src/commutative-algebra/geometric-sequences-commutative-semirings.lagda.md
index 1e4b7ed9f9..71fcbc05c1 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 0abb907785..7e3142369f 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 57acf9d9c0..2d96a63866 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/inequality-standard-finite-types.lagda.md b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md
index 86135f39fc..a3514373d2 100644
--- a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md
+++ b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md
@@ -24,6 +24,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
 
@@ -146,6 +147,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
+  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)
+  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
 
 ```agda
@@ -169,3 +182,26 @@ 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
 ```
+
+### `inr-Fin` preserves inequality
+
+```agda
+abstract
+  preserves-order-inr-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
+  preserves-order-inr-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 n (inr star) = star
+  leq-zero-Fin (succ-ℕ n) (inl i) = leq-zero-Fin n i
+```
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 302d0c9537..06bfd5591f 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 b63e1fc243..3921c89047 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 81bfd369b5..d5b08eebd8 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 23130c0507..79a689660a 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 23da431fc0..b2fb80e9b6 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
 <details><summary>Imports</summary>
 
 ```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/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 e0436da863..e21cf5f9ab 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
@@ -21,6 +21,7 @@ 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
@@ -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.lagda.md b/src/lists.lagda.md
index b8fb537ab6..4ec538b113 100644
--- a/src/lists.lagda.md
+++ b/src/lists.lagda.md
@@ -23,6 +23,7 @@ open import lists.functoriality-tuples-finite-sequences public
 open import lists.insert-at-index-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
diff --git a/src/lists/arrays.lagda.md b/src/lists/arrays.lagda.md
index 08bc9b865b..91dd108515 100644
--- a/src/lists/arrays.lagda.md
+++ b/src/lists/arrays.lagda.md
@@ -71,19 +71,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 c481b3bba9..27f4e84e9d 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/lists/nonempty-arrays.lagda.md b/src/lists/nonempty-arrays.lagda.md
new file mode 100644
index 0000000000..c9410440e9
--- /dev/null
+++ b/src/lists/nonempty-arrays.lagda.md
@@ -0,0 +1,83 @@
+# Nonempty arrays
+
+```agda
+module lists.nonempty-arrays where
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## 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/lists/pairs-of-successive-elements-finite-sequences.lagda.md b/src/lists/pairs-of-successive-elements-finite-sequences.lagda.md
index 56e8e4845c..d14baa06a9 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/literature/introduction-to-homotopy-type-theory.lagda.md b/src/literature/introduction-to-homotopy-type-theory.lagda.md
index 61eb61ff0d..c03837a988 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.lagda.md b/src/order-theory.lagda.md
index 85707fe438..06c4b28dac 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
@@ -83,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 fdde553f93..753fdd7b28 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-arrays-posets.lagda.md b/src/order-theory/increasing-arrays-posets.lagda.md
new file mode 100644
index 0000000000..c96578ae8c
--- /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
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## 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 0000000000..f388fd30bb
--- /dev/null
+++ b/src/order-theory/increasing-finite-sequences-posets.lagda.md
@@ -0,0 +1,176 @@
+# Increasing finite sequences in posets
+
+```agda
+module order-theory.increasing-finite-sequences-posets where
+```
+
+<details><summary>Imports</summary>
+
+```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.homotopies
+open import foundation.identity-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
+
+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
+
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## 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-type-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 n =
+    preserves-order-prop-Poset (Fin-Poset n) P
+
+  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 `a₁, ..., aₙ` is increasing if and only if `a₁ ≤ a₂ ∧ a₂ ≤ a₃ ∧ ... ∧ aₙ₋₁ ≤ aₙ`
+
+```agda
+module _
+  {l1 l2 : Level}
+  (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
+    is-increasing-is-increasing-leq-next-fin-sequence-type-Poset :
+      (n : ℕ) (u : fin-sequence (type-Poset P) n) →
+      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))
+    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 (inl i))
+        ( u (inl (inr star)))
+        ( 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)
+          ( star))
+    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)
+        ( i≤j)
+
+    is-increasing-leq-next-is-increasing-fin-sequence-type-Poset :
+      (n : ℕ) (u : fin-sequence (type-Poset P) 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)
+```
+
+### 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 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/increasing-nonempty-arrays-posets.lagda.md b/src/order-theory/increasing-nonempty-arrays-posets.lagda.md
new file mode 100644
index 0000000000..8893aa2cef
--- /dev/null
+++ b/src/order-theory/increasing-nonempty-arrays-posets.lagda.md
@@ -0,0 +1,210 @@
+# Increasing nonempty arrays in posets
+
+```agda
+module order-theory.increasing-nonempty-arrays-posets where
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## 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-nonempty-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
+      (((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
+  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) =
+      preserves-order-comp-Poset
+        ( Fin-Poset n)
+        ( Fin-Poset (succ-ℕ n))
+        ( P)
+        ( 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
+  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 greatest element
+
+```agda
+module _
+  {l1 l2 : Level}
+  (P : Poset l1 l2)
+  where
+
+  abstract
+    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
+        ( fin-sequence-increasing-nonempty-array-type-Poset P u i)
+        ( head-increasing-nonempty-array-type-Poset P u)
+    is-greatest-element-head-increasing-nonempty-array-type-Poset
+      (((succ-ℕ n , u) , _) , H) i =
+      H i (neg-one-Fin n) star
+```
+
+### The last element of a nonempty array is its least element
+
+```agda
+module _
+  {l1 l2 : Level}
+  (P : Poset l1 l2)
+  where
+
+  abstract
+    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
+        ( last-increasing-nonempty-array-type-Poset P u)
+        ( fin-sequence-increasing-nonempty-array-type-Poset P u i)
+    is-least-element-last-increasing-nonempty-array-type-Poset
+      (((succ-ℕ n , u) , _) , H) i =
+      H (zero-Fin n) i (leq-zero-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 0000000000..db38dc8151
--- /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
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## Idea
+
+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`.
+
+## 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/order-theory/least-upper-bounds-large-posets.lagda.md b/src/order-theory/least-upper-bounds-large-posets.lagda.md
index dfa918f385..3532cb35f1 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 074bfbfe97..c1b50147fd 100644
--- a/src/real-numbers.lagda.md
+++ b/src/real-numbers.lagda.md
@@ -66,6 +66,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
@@ -108,6 +109,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
@@ -136,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
@@ -150,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/closed-intervals-real-numbers.lagda.md b/src/real-numbers/closed-intervals-real-numbers.lagda.md
index 42b0ceb4c6..1df36ede01 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/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 0000000000..e0bab853e4
--- /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
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## 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/maximum-finite-families-nonnegative-real-numbers.lagda.md b/src/real-numbers/maximum-finite-families-nonnegative-real-numbers.lagda.md
index a922197ecc..980580b1c5 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
 ```
 
 </details>
@@ -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
new file mode 100644
index 0000000000..8ff4b4dd6a
--- /dev/null
+++ b/src/real-numbers/partitions-closed-intervals-real-numbers.lagda.md
@@ -0,0 +1,293 @@
+# Partitions of closed intervals of real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.partitions-closed-intervals-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```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.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.raising-universe-levels-unit-type
+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-finite-sequences-posets
+open import order-theory.increasing-nonempty-arrays-posets
+open import order-theory.lower-bounds-large-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.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.nonnegative-real-numbers
+
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## 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 →
+        ( 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-ℝ → ℕ
+  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)
+
+  eq-lower-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) ＝
+    a
+  eq-lower-bound-last-real-fin-sequence-partition-closed-interval-ℝ
+    ((((succ-ℕ n , u) , _) , _) , u₀=a , _) =
+    u₀=a
+
+  eq-upper-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) ＝
+    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-ℝ :
+      (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@((((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-ℝ) →
+      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@((((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-ℝ) →
+    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
+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
+
+```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] : 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 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]) →
+      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 (b ∷ a ∷ empty-tuple)) ,
+          star) ,
+        is-increasing-is-increasing-leq-next-fin-sequence-type-Poset
+          ( ℝ-Poset l)
+          ( 2)
+          ( _)
+          ( raise-star , a≤b)) ,
+      refl ,
+      refl)
+```
+
+## External links
+
+- [Partition of an interval](https://en.wikipedia.org/wiki/Partition_of_an_interval)
+  on Wikipedia
diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md
index 744a7c5885..e9509f45c8 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 0000000000..6a31ce75f5
--- /dev/null
+++ b/src/real-numbers/standard-uniform-partitions-closed-intervals-real-numbers.lagda.md
@@ -0,0 +1,271 @@
+# 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
+```
+
+<details><summary>Imports</summary>
+
+```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.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.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
+```
+
+</details>
+
+## 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-ℝ)
+
+  mesh-standard-uniform-partition-closed-interval-ℝ : ℝ⁰⁺ l
+  mesh-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-ℝ =
+    ( mesh-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-ℝ)
+
+  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
+
+### 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 0000000000..7ae48bde79
--- /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
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## 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
+
+  mesh-uniform-partition-closed-interval-ℝ : ℝ⁰⁺ l
+  mesh-uniform-partition-closed-interval-ℝ =
+    mesh-partition-closed-interval-ℝ [a,b] p
+
+  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
+      ( 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-ℝ =
+    mesh-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 0000000000..10591f3285
--- /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
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## 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 ad5ee69398..d4bfaadb86 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 76c5a3b31f..b86e62890e 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))))
 ```
 
@@ -539,6 +540,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)
+```
+
 ### The complement of `-1` in `Fin (n + 1)` is equivalent to `Fin n`
 
 ```agda