The decidable total order on a standard finite type (#844)

Defines the decidable total order on a standard finite type. Also does a littlebit of refactoring of infix binary comparison operators. --------- Co-authored-by: Egbert Rijke <[email protected]>
UniMath · Oct 16, 2023 · c674508 · c674508
1 parent 245488e
commit c674508
Show file tree

Hide file tree

Showing 15 changed files with 134 additions and 62 deletions.
diff --git a/MIXFIX-OPERATORS.md b/MIXFIX-OPERATORS.md
@@ -170,7 +170,7 @@ Below, we outline a list of general rules when assigning associativities.
 | 40               | Multiplicative arithmetic operators                                                                                                                                                                                                        |
 | 36               | Subtractive arithmetic operators                                                                                                                                                                                                           |
 | 35               | Additive arithmetic operators                                                                                                                                                                                                              |
-| 30               | Relational arithmetic operators, `_≤-ℕ_` and `_<-ℕ_`                                                                                                                                                                                       |
+| 30               | Relational arithmetic operators like`_≤-ℕ_` and `_<-ℕ_`                                                                                                                                                                                    |
 | 25               | Parametric unary operators. This class is currently empty                                                                                                                                                                                  |
 | 20               | Parametric exponentiative operators. This class is currently empty                                                                                                                                                                         |
 | 15               | Parametric multiplicative operators like `_×_`,`_×∗_`, `_∧_`, `_∧∗_`, function composition operators like `_∘_`,`_∘∗_`, `_∘e_`, and `_∘iff_`, identification concatenation and whiskering operators like `_∙_`, `_∙h_`, `_·l_`, and `_·r_` |

diff --git a/src/category-theory/faithful-functors-precategories.lagda.md b/src/category-theory/faithful-functors-precategories.lagda.md
@@ -28,8 +28,8 @@ A [functor](category-theory.functors-precategories.md) between
 its an [embedding](foundation-core.embeddings.md) on hom-sets.
 
 Note that embeddings on [sets](foundation-core.sets.md) happen to coincide with
-[injections](foundation.injective-maps.md), but we define it in terms of the
-stronger notion, as this is the notion that generalizes.
+[injections](foundation.injective-maps.md). However, we define faithful functors
+in terms of embeddings because this is the notion that generalizes.
 
 ## Definition
 
@@ -109,7 +109,7 @@ module _
     is-prop-is-injective-hom-map-Precategory
 ```
 
-### The predicate of being faithful on functors between precategories
+### The predicate of being injective on hom-sets on functors between precategories
 
 ```agda
 module _

diff --git a/src/category-theory/presheaf-categories.lagda.md b/src/category-theory/presheaf-categories.lagda.md
@@ -40,7 +40,7 @@ functor category
   C → Set.
 ```
 
-## Definition
+## Definitions
 
 ### The copresheaf category of a precategory
 

diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md
@@ -29,6 +29,7 @@ open import elementary-number-theory.congruence-integers public
 open import elementary-number-theory.congruence-natural-numbers public
 open import elementary-number-theory.decidable-dependent-function-types public
 open import elementary-number-theory.decidable-total-order-natural-numbers public
+open import elementary-number-theory.decidable-total-order-standard-finite-types public
 open import elementary-number-theory.decidable-types public
 open import elementary-number-theory.difference-integers public
 open import elementary-number-theory.dirichlet-convolution public

diff --git a/src/elementary-number-theory/decidable-total-order-natural-numbers.lagda.md b/src/elementary-number-theory/decidable-total-order-natural-numbers.lagda.md
@@ -1,4 +1,4 @@
-# Natural numbers are a total decidable poset
+# The decidable total order of natural numbers
 
 ```agda
 module elementary-number-theory.decidable-total-order-natural-numbers where
@@ -14,21 +14,30 @@ open import foundation.propositional-truncations
 open import foundation.universe-levels
 
 open import order-theory.decidable-total-orders
+open import order-theory.total-orders
 ```
 
 </details>
 
 ## Idea
 
-The type of natural numbers equipped with its standard ordering relation forms a
-total order.
+The type of [natural numbers](elementary-number-theory.natural-numbers.md)
+[equipped](foundation.structure.md) with its
+[standard ordering relation](elementary-number-theory.inequality-natural-numbers.md)
+forms a [decidable total order](order-theory.decidable-total-orders.md).
 
 ## Definition
 
 ```agda
-ℕ-Decidable-Total-Order :
-  Decidable-Total-Order lzero lzero
+is-total-leq-ℕ : is-total-Poset ℕ-Poset
+is-total-leq-ℕ n m = unit-trunc-Prop (linear-leq-ℕ n m)
+
+ℕ-Total-Order : Total-Order lzero lzero
+pr1 ℕ-Total-Order = ℕ-Poset
+pr2 ℕ-Total-Order = is-total-leq-ℕ
+
+ℕ-Decidable-Total-Order : Decidable-Total-Order lzero lzero
 pr1 ℕ-Decidable-Total-Order = ℕ-Poset
-pr1 (pr2 ℕ-Decidable-Total-Order) n m = unit-trunc-Prop (linear-leq-ℕ n m)
+pr1 (pr2 ℕ-Decidable-Total-Order) = is-total-leq-ℕ
 pr2 (pr2 ℕ-Decidable-Total-Order) = is-decidable-leq-ℕ
 ```
diff --git a/src/elementary-number-theory/decidable-total-order-standard-finite-types.lagda.md b/src/elementary-number-theory/decidable-total-order-standard-finite-types.lagda.md
@@ -0,0 +1,47 @@
+# The decidable total order of a standard finite type
+
+```agda
+module elementary-number-theory.decidable-total-order-standard-finite-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.inequality-natural-numbers
+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.propositional-truncations
+open import foundation.universe-levels
+
+open import order-theory.decidable-total-orders
+open import order-theory.total-orders
+
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Idea
+
+The [standard finite type](univalent-combinatorics.standard-finite-types.md) of
+order `k` [equipped](foundation.structure.md) with its
+[standard ordering relation](elementary-number-theory.inequality-standard-finite-types.md)
+forms a [decidable total order](order-theory.decidable-total-orders.md).
+
+## Definition
+
+```agda
+is-total-leq-Fin : (k : ℕ) → is-total-Poset (Fin-Poset k)
+is-total-leq-Fin k n m = unit-trunc-Prop (linear-leq-Fin k n m)
+
+Fin-Total-Order : ℕ → Total-Order lzero lzero
+pr1 (Fin-Total-Order k) = Fin-Poset k
+pr2 (Fin-Total-Order k) = is-total-leq-Fin k
+
+Fin-Decidable-Total-Order : ℕ → Decidable-Total-Order lzero lzero
+pr1 (Fin-Decidable-Total-Order k) = Fin-Poset k
+pr1 (pr2 (Fin-Decidable-Total-Order k)) = is-total-leq-Fin k
+pr2 (pr2 (Fin-Decidable-Total-Order k)) = is-decidable-leq-Fin k
+```
diff --git a/src/elementary-number-theory/inequality-integers.lagda.md b/src/elementary-number-theory/inequality-integers.lagda.md
@@ -37,6 +37,9 @@ leq-ℤ x y = type-Prop (leq-ℤ-Prop x y)
 
 is-prop-leq-ℤ : (x y : ℤ) → is-prop (leq-ℤ x y)
 is-prop-leq-ℤ x y = is-prop-type-Prop (leq-ℤ-Prop x y)
+
+infix 30 _≤-ℤ_
+_≤-ℤ_ = leq-ℤ
 ```
 
 ## Properties

diff --git a/src/elementary-number-theory/inequality-rational-numbers.lagda.md b/src/elementary-number-theory/inequality-rational-numbers.lagda.md
@@ -36,6 +36,9 @@ leq-ℚ x y = type-Prop (leq-ℚ-Prop x y)
 
 is-prop-leq-ℚ : (x y : ℚ) → is-prop (leq-ℚ x y)
 is-prop-leq-ℚ x y = is-prop-type-Prop (leq-ℚ-Prop x y)
+
+infix 30 _≤-ℚ_
+_≤-ℚ_ = leq-ℚ
 ```
 
 ### Strict inequality on the rational numbers

diff --git a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md
@@ -25,6 +25,7 @@ open import foundation.universe-levels
 
 open import order-theory.posets
 open import order-theory.preorders
+open import order-theory.total-orders
 
 open import univalent-combinatorics.standard-finite-types
 ```
@@ -104,9 +105,7 @@ reflects-leq-nat-Fin (succ-ℕ k) {inl x} {inr star} H = star
 reflects-leq-nat-Fin (succ-ℕ k) {inr star} {inr star} H = star
 ```
 
-## Properties
-
-### The preordering on the standard finite types
+### The partial order on the standard finite types
 
 ```agda
 Fin-Preorder : ℕ → Preorder lzero lzero
@@ -120,6 +119,8 @@ pr1 (Fin-Poset k) = Fin-Preorder k
 pr2 (Fin-Poset k) = antisymmetric-leq-Fin k
 ```
 
+## Properties
+
 ### Ordering on the standard finite types is decidable
 
 ```agda
@@ -134,3 +135,12 @@ pr1 (leq-Fin-Decidable-Prop k x y) = leq-Fin k x y
 pr1 (pr2 (leq-Fin-Decidable-Prop k x y)) = is-prop-leq-Fin k x y
 pr2 (pr2 (leq-Fin-Decidable-Prop k x y)) = is-decidable-leq-Fin k x y
 ```
+
+### Ordering on the standard finite types is linear
+
+```agda
+linear-leq-Fin : (k : ℕ) (x y : Fin k) → leq-Fin k x y + leq-Fin k y x
+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
+```
diff --git a/src/elementary-number-theory/ordinal-induction-natural-numbers.lagda.md b/src/elementary-number-theory/ordinal-induction-natural-numbers.lagda.md
@@ -18,7 +18,7 @@ open import foundation.universe-levels
 
 ## Idea
 
-The ordinal induction principle of the natural numbers is the well-founded
+The **ordinal induction principle of the natural numbers** is the well-founded
 induction principle of ℕ.
 
 ## To Do

diff --git a/src/order-theory/decidable-total-orders.lagda.md b/src/order-theory/decidable-total-orders.lagda.md
@@ -28,8 +28,9 @@ open import order-theory.total-orders
 
 ## Idea
 
-A **decidable total order** is a total order of which the inequality relation is
-decidable.
+A **decidable total order** is a [total order](order-theory.total-orders.md) of
+which the inequality [relation](foundation.binary-relations.md) is
+[decidable](foundation.decidable-relations.md).
 
 ## Definitions
 

diff --git a/src/order-theory/total-orders.lagda.md b/src/order-theory/total-orders.lagda.md
@@ -23,9 +23,10 @@ open import order-theory.total-preorders
 
 ## Idea
 
-A **total order**, or a \*\*linear order, is a poset `P` such that for every two
-elements `x` and `y` in `P` the disjunction `(x ≤ y) ∨ (y ≤ x)` holds. In other
-words, total orders are totally ordered in the sense tat any two elements are
+A **total order**, or a **linear order**, is a [poset](order-theory.posets.md)
+`P` such that for every two elements `x` and `y` in `P` the
+[disjunction](foundation.disjunction.md) `(x ≤ y) ∨ (y ≤ x)` holds. In other
+words, total orders are totally ordered in the sense that any two elements are
 comparable.
 
 ## Definitions
@@ -57,7 +58,7 @@ module _
   is-prop-is-total-Poset = is-prop-is-total-Preorder (preorder-Poset X)
 ```
 
-### Type of total posets
+### The type of total orders
 
 ```agda
 Total-Order : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)

diff --git a/src/set-theory/cardinalities.lagda.md b/src/set-theory/cardinalities.lagda.md
@@ -78,19 +78,15 @@ leq-cardinality-Prop {l1} {l2} =
 leq-cardinality : {l1 l2 : Level} → cardinal l1 → cardinal l2 → UU (l1 ⊔ l2)
 leq-cardinality X Y = type-Prop (leq-cardinality-Prop X Y)
 
-infix 6 _≤-cardinality_
-_≤-cardinality_ : {l1 l2 : Level} → cardinal l1 → cardinal l2 → UU (l1 ⊔ l2)
-_≤-cardinality_ = leq-cardinality
-
 is-prop-leq-cardinality :
   {l1 l2 : Level} {X : cardinal l1} {Y : cardinal l2} →
-  is-prop (X ≤-cardinality Y)
+  is-prop (leq-cardinality X Y)
 is-prop-leq-cardinality {X = X} {Y = Y} =
   is-prop-type-Prop (leq-cardinality-Prop X Y)
 
 compute-leq-cardinality :
   {l1 l2 : Level} (X : Set l1) (Y : Set l2) →
-  ( cardinality X ≤-cardinality cardinality Y) ≃
+  ( leq-cardinality (cardinality X) (cardinality Y)) ≃
   ( mere-emb (type-Set X) (type-Set Y))
 compute-leq-cardinality {l1} {l2} X Y =
   equiv-eq-Prop
@@ -102,12 +98,14 @@ compute-leq-cardinality {l1} {l2} X Y =
 
 unit-leq-cardinality :
   {l1 l2 : Level} (X : Set l1) (Y : Set l2) →
-  mere-emb (type-Set X) (type-Set Y) → cardinality X ≤-cardinality cardinality Y
+  mere-emb (type-Set X) (type-Set Y) →
+  leq-cardinality (cardinality X) (cardinality Y)
 unit-leq-cardinality X Y = map-inv-equiv (compute-leq-cardinality X Y)
 
 inv-unit-leq-cardinality :
   {l1 l2 : Level} (X : Set l1) (Y : Set l2) →
-  cardinality X ≤-cardinality cardinality Y → mere-emb (type-Set X) (type-Set Y)
+  leq-cardinality (cardinality X) (cardinality Y) →
+  mere-emb (type-Set X) (type-Set Y)
 inv-unit-leq-cardinality X Y = pr1 (compute-leq-cardinality X Y)
 
 refl-leq-cardinality : {l : Level} → is-reflexive (leq-cardinality {l})
@@ -121,32 +119,32 @@ transitive-leq-cardinality :
   (X : cardinal l1)
   (Y : cardinal l2)
   (Z : cardinal l3) →
-  X ≤-cardinality Y →
-  Y ≤-cardinality Z →
-  X ≤-cardinality Z
+  leq-cardinality X Y →
+  leq-cardinality Y Z →
+  leq-cardinality X Z
 transitive-leq-cardinality X Y Z =
   apply-dependent-universal-property-trunc-Set'
   (λ u →
     set-Prop
       (function-Prop
-        (u ≤-cardinality Y)
-        (function-Prop (Y ≤-cardinality Z)
+        (leq-cardinality u Y)
+        (function-Prop (leq-cardinality Y Z)
           (leq-cardinality-Prop u Z))))
   (λ a →
     apply-dependent-universal-property-trunc-Set'
     (λ v →
       set-Prop
         (function-Prop
-          ((cardinality a) ≤-cardinality v)
-          (function-Prop (v ≤-cardinality Z)
+          (leq-cardinality (cardinality a) v)
+          (function-Prop (leq-cardinality v Z)
             (leq-cardinality-Prop (cardinality a) Z))))
     (λ b →
       apply-dependent-universal-property-trunc-Set'
       (λ w →
         set-Prop
           (function-Prop
-            ((cardinality a) ≤-cardinality (cardinality b))
-            (function-Prop ((cardinality b) ≤-cardinality w)
+            (leq-cardinality (cardinality a) (cardinality b))
+            (function-Prop (leq-cardinality (cardinality b) w)
               (leq-cardinality-Prop (cardinality a) w))))
       (λ c a<b b<c →
         unit-leq-cardinality
@@ -175,36 +173,36 @@ is-effective-cardinality X Y =
 
 ### Assuming excluded middle we can show that `leq-cardinality` is a partial order
 
-Using the previous result and assuming excluded middle, we can show
+Using the previous result and assuming excluded middle, we can conclude
 `leq-cardinality` is a partial order by showing that it is antisymmetric.
 
 ```agda
 antisymmetric-leq-cardinality :
   {l1 : Level} (X Y : cardinal l1) → (LEM l1) →
-  X ≤-cardinality Y → Y ≤-cardinality X → X ＝ Y
+  leq-cardinality X Y → leq-cardinality Y X → X ＝ Y
 antisymmetric-leq-cardinality {l1} X Y lem =
   apply-dependent-universal-property-trunc-Set'
   (λ u →
     set-Prop
-      (function-Prop
-        (u ≤-cardinality Y)
-        (function-Prop
-          (Y ≤-cardinality u)
-          (Id-Prop (cardinal-Set l1) u Y))))
-  (λ a →
+      ( function-Prop
+        ( leq-cardinality u Y)
+        ( function-Prop
+          ( leq-cardinality Y u)
+          ( Id-Prop (cardinal-Set l1) u Y))))
+  ( λ a →
     apply-dependent-universal-property-trunc-Set'
-    (λ v →
+    ( λ v →
       set-Prop
-        (function-Prop
-          ((cardinality a) ≤-cardinality v)
-          (function-Prop
-            (v ≤-cardinality (cardinality a))
-            (Id-Prop (cardinal-Set l1) (cardinality a) v))))
-    (λ b a<b b<a →
+        ( function-Prop
+          ( leq-cardinality (cardinality a) v)
+          ( function-Prop
+            ( leq-cardinality v (cardinality a))
+            ( Id-Prop (cardinal-Set l1) (cardinality a) v))))
+    ( λ b a<b b<a →
       map-inv-equiv (is-effective-cardinality a b)
         (antisymmetric-mere-emb lem
         (inv-unit-leq-cardinality _ _ a<b)
         (inv-unit-leq-cardinality _ _ b<a)))
-    Y)
-  X
+    ( Y))
+  ( X)
 ```
diff --git a/src/univalent-combinatorics/inequality-types-with-counting.lagda.md b/src/univalent-combinatorics/inequality-types-with-counting.lagda.md
@@ -29,8 +29,7 @@ inequality relations from the standard finite types.
 ## Definition
 
 ```agda
-leq-count :
-  {l : Level} {X : UU l} → count X → X → X → UU lzero
+leq-count : {l : Level} {X : UU l} → count X → X → X → UU lzero
 leq-count e x y =
   leq-Fin
     ( number-of-elements-count e)