From 7945fa5dd215ec683a071ead208bc9a9e060118e Mon Sep 17 00:00:00 2001
From: Louis Wasserman <wasserman.louis@gmail.com>
Date: Fri, 7 Feb 2025 12:39:47 -0800
Subject: [PATCH] Minimum and maximum for decidable total orders (#1291)

---
 .../decidable-total-orders.lagda.md           | 170 ++++++++++++++++++
 1 file changed, 170 insertions(+)

diff --git a/src/order-theory/decidable-total-orders.lagda.md b/src/order-theory/decidable-total-orders.lagda.md
index 2aeb739708..b8541bded7 100644
--- a/src/order-theory/decidable-total-orders.lagda.md
+++ b/src/order-theory/decidable-total-orders.lagda.md
@@ -11,6 +11,7 @@ open import foundation.binary-relations
 open import foundation.coproduct-types
 open import foundation.decidable-propositions
 open import foundation.dependent-pair-types
+open import foundation.empty-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.sets
@@ -18,6 +19,8 @@ open import foundation.universe-levels
 
 open import order-theory.decidable-posets
 open import order-theory.decidable-total-preorders
+open import order-theory.greatest-lower-bounds-posets
+open import order-theory.least-upper-bounds-posets
 open import order-theory.posets
 open import order-theory.preorders
 open import order-theory.total-orders
@@ -181,3 +184,170 @@ module _
   set-Decidable-Total-Order : Set l1
   set-Decidable-Total-Order = set-Poset poset-Decidable-Total-Order
 ```
+
+## Properties
+
+### Any two elements in a decidable total order have a minimum and maximum
+
+```agda
+module _
+  {l1 l2 : Level}
+  (T : Decidable-Total-Order l1 l2)
+  (x y : type-Decidable-Total-Order T)
+  where
+
+  min-Total-Order : type-Decidable-Total-Order T
+  min-Total-Order =
+    rec-coproduct
+      ( λ x≤y → x)
+      ( λ y<x → y)
+      ( is-leq-or-strict-greater-Decidable-Total-Order T x y)
+
+  max-Total-Order : type-Decidable-Total-Order T
+  max-Total-Order =
+    rec-coproduct
+      ( λ x≤y → y)
+      ( λ y<x → x)
+      ( is-leq-or-strict-greater-Decidable-Total-Order T x y)
+```
+
+### `min x y ≤ x`
+
+```agda
+  leq-left-min-Total-Order : leq-Decidable-Total-Order T min-Total-Order x
+  leq-left-min-Total-Order
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = refl-leq-Decidable-Total-Order T x
+  ... | inr y<x = pr2 y<x
+```
+
+### `min x y ≤ y`
+
+```agda
+  leq-right-min-Total-Order : leq-Decidable-Total-Order T min-Total-Order y
+  leq-right-min-Total-Order
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = x≤y
+  ... | inr y<x = refl-leq-Decidable-Total-Order T y
+```
+
+### `x ≤ max x y`
+
+```agda
+  leq-left-max-Total-Order : leq-Decidable-Total-Order T x max-Total-Order
+  leq-left-max-Total-Order
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = x≤y
+  ... | inr y<x = refl-leq-Decidable-Total-Order T x
+```
+
+### `y ≤ max x y`
+
+```agda
+  leq-right-max-Total-Order : leq-Decidable-Total-Order T y max-Total-Order
+  leq-right-max-Total-Order
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = refl-leq-Decidable-Total-Order T y
+  ... | inr y<x = pr2 y<x
+```
+
+### `min` is commutative
+
+```agda
+module _
+  {l1 l2 : Level}
+  (T : Decidable-Total-Order l1 l2)
+  (x y : type-Decidable-Total-Order T)
+  where
+
+  commutative-min-Total-Order : min-Total-Order T x y ＝ min-Total-Order T y x
+  commutative-min-Total-Order
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+          | is-leq-or-strict-greater-Decidable-Total-Order T y x
+  ... | inl x≤y | inl y≤x =
+    antisymmetric-leq-Decidable-Total-Order T x y x≤y y≤x
+  ... | inl x≤y | inr x<y = refl
+  ... | inr y<x | inl y≤x = refl
+  ... | inr y<x | inr x<y =
+    ex-falso
+      (pr1
+        ( x<y)
+        ( antisymmetric-leq-Decidable-Total-Order T x y (pr2 x<y) (pr2 y<x)))
+```
+
+### `max` is commutative
+
+```agda
+  commutative-max-Total-Order : max-Total-Order T x y ＝ max-Total-Order T y x
+  commutative-max-Total-Order
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+          | is-leq-or-strict-greater-Decidable-Total-Order T y x
+  ... | inl x≤y | inl y≤x =
+    antisymmetric-leq-Decidable-Total-Order T y x y≤x x≤y
+  ... | inl x≤y | inr x<y = refl
+  ... | inr y<x | inl y≤x = refl
+  ... | inr y<x | inr x<y =
+    ex-falso
+      (pr1
+        ( x<y)
+        ( antisymmetric-leq-Decidable-Total-Order T x y (pr2 x<y) (pr2 y<x)))
+```
+
+### `min x y` is the greatest lower bound of `x` and `y`
+
+```agda
+  min-is-greatest-binary-lower-bound-Decidable-Total-Order :
+    is-greatest-binary-lower-bound-Poset
+      ( poset-Decidable-Total-Order T)
+      ( x)
+      ( y)
+      ( min-Total-Order T x y)
+  pr1 (min-is-greatest-binary-lower-bound-Decidable-Total-Order z) (z≤x , z≤y)
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = z≤x
+  ... | inr y<x = z≤y
+  pr1 (pr2 (min-is-greatest-binary-lower-bound-Decidable-Total-Order z) z≤min)
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = z≤min
+  ... | inr y<x = transitive-leq-Decidable-Total-Order T z y x (pr2 y<x) z≤min
+  pr2 (pr2 (min-is-greatest-binary-lower-bound-Decidable-Total-Order z) z≤min)
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = transitive-leq-Decidable-Total-Order T z x y x≤y z≤min
+  ... | inr y<x = z≤min
+
+  has-greatest-binary-lower-bound-Decidable-Total-Order :
+    has-greatest-binary-lower-bound-Poset (poset-Decidable-Total-Order T) x y
+  pr1 has-greatest-binary-lower-bound-Decidable-Total-Order =
+    min-Total-Order T x y
+  pr2 has-greatest-binary-lower-bound-Decidable-Total-Order =
+    min-is-greatest-binary-lower-bound-Decidable-Total-Order
+```
+
+### `max x y` is the least upper bound of `x` and `y`
+
+```agda
+  max-is-least-binary-upper-bound-Decidable-Total-Order :
+    is-least-binary-upper-bound-Poset
+      ( poset-Decidable-Total-Order T)
+      ( x)
+      ( y)
+      ( max-Total-Order T x y)
+  pr1 (max-is-least-binary-upper-bound-Decidable-Total-Order z) (x≤z , y≤z)
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = y≤z
+  ... | inr y<x = x≤z
+  pr1 (pr2 (max-is-least-binary-upper-bound-Decidable-Total-Order z) min≤z)
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = transitive-leq-Decidable-Total-Order T x y z min≤z x≤y
+  ... | inr y<x = min≤z
+  pr2 (pr2 (max-is-least-binary-upper-bound-Decidable-Total-Order z) min≤z)
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = min≤z
+  ... | inr y<x = transitive-leq-Decidable-Total-Order T y x z min≤z (pr2 y<x)
+
+  has-least-binary-upper-bound-Decidable-Total-Order :
+    has-least-binary-upper-bound-Poset (poset-Decidable-Total-Order T) x y
+  pr1 has-least-binary-upper-bound-Decidable-Total-Order = max-Total-Order T x y
+  pr2 has-least-binary-upper-bound-Decidable-Total-Order =
+    max-is-least-binary-upper-bound-Decidable-Total-Order
+```