Standard uniform partitions of closed intervals of real numbers

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

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

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))

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
+```

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 :

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)) →

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

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)

src/foundation/null-homotopic-maps.lagda.md

@@ -7,13 +7,15 @@ 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
 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

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)

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

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) ,

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) →

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)
+```

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))
 ```

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

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