From 8876cf6cbe2100f9b9968fff1058410b15845ed6 Mon Sep 17 00:00:00 2001
From: whatisRT <andre.knispel@gmx.de>
Date: Fri, 11 Oct 2024 15:11:56 +0200
Subject: [PATCH] Make `HasOrder` follow the same structure as everything else

---
 Class/HasOrder.agda                           | 158 +----------------
 Class/HasOrder/Core.agda                      | 160 ++++++++++++++++++
 .../{Instances.agda => Instance.agda}         |   4 +-
 3 files changed, 164 insertions(+), 158 deletions(-)
 create mode 100644 Class/HasOrder/Core.agda
 rename Class/HasOrder/{Instances.agda => Instance.agda} (95%)

diff --git a/Class/HasOrder.agda b/Class/HasOrder.agda
index 6086fa6..b21efcb 100644
--- a/Class/HasOrder.agda
+++ b/Class/HasOrder.agda
@@ -2,159 +2,5 @@
 
 module Class.HasOrder where
 
-open import Class.Decidable
-open import Data.Empty
-open import Data.Product
-open import Data.Sum
-open import Function
-open import Level
-open import Relation.Binary
-open import Relation.Binary using () renaming (Decidable to Decidable²)
-open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary
-
-open Equivalence
-
-module _ {a} {A : Set a} where
-  module _ {_≈_ : Rel A a} where
-
-    record HasPreorder : Set (suc a) where
-      infix 4 _≤_ _<_ _≥_ _>_
-      field
-        _≤_ _<_       : Rel A a
-        ≤-isPreorder  : IsPreorder _≈_ _≤_
-        <-irrefl      : Irreflexive _≈_ _<_
-        ≤⇔<∨≈         : ∀ {x y} → x ≤ y ⇔ (x < y ⊎ x ≈ y)
-
-      _≥_ = flip _≤_
-      _>_ = flip _<_
-
-      open IsPreorder ≤-isPreorder public
-        using ()
-        renaming (isEquivalence to ≈-isEquivalence; refl to ≤-refl; trans to ≤-trans)
-
-      _≤?_ : ⦃ _≤_ ⁇² ⦄ → Decidable _≤_
-      _≤?_ = dec²
-
-      _<?_ : ⦃ _<_ ⁇² ⦄ → Decidable _<_
-      _<?_ = dec²
-
-      infix 4 _<?_ _≤?_
-
-      <⇒≤∧≉ : ∀ {x y} → x < y → x ≤ y × ¬ (x ≈ y)
-      <⇒≤∧≉ x<y = from ≤⇔<∨≈ (inj₁ x<y) , λ x≈y → <-irrefl x≈y x<y
-
-      ≤∧≉⇒< : ∀ {x y} → x ≤ y × ¬ (x ≈ y) → x < y
-      ≤∧≉⇒< {x} {y} (x≤y , ¬x≈y) with to ≤⇔<∨≈ x≤y
-      ... | inj₁ x<y = x<y
-      ... | inj₂ x≈y = ⊥-elim (¬x≈y x≈y)
-
-      ≤-antisym⇒<-asym : Antisymmetric _≈_ _≤_ → Asymmetric _<_
-      ≤-antisym⇒<-asym antisym x<y y<x =
-        proj₂ (<⇒≤∧≉ x<y) $ antisym (proj₁ $ <⇒≤∧≉ x<y) (proj₁ $ <⇒≤∧≉ y<x)
-
-    open HasPreorder ⦃...⦄
-
-    record HasDecPreorder : Set (suc a) where
-      field ⦃ hasPreorder ⦄ : HasPreorder
-            ⦃ dec-≤ ⦄ : _≤_ ⁇²
-            ⦃ dec-< ⦄ : _<_ ⁇²
-
-    record HasPartialOrder : Set (suc a) where
-      field
-        ⦃ hasPreorder ⦄ : HasPreorder
-        ≤-antisym : Antisymmetric _≈_ _≤_
-
-      ≤-isPartialOrder : IsPartialOrder _≈_ _≤_
-      ≤-isPartialOrder = record { isPreorder = ≤-isPreorder ; antisym = ≤-antisym }
-
-      <-asymmetric : Asymmetric _<_
-      <-asymmetric = ≤-antisym⇒<-asym ≤-antisym
-
-      open IsEquivalence ≈-isEquivalence renaming (sym to ≈-sym)
-
-      <-trans : Transitive _<_
-      <-trans i<j j<k =
-        let
-          j≤k = proj₁ $ <⇒≤∧≉ j<k; i≤j = proj₁ $ <⇒≤∧≉ i<j
-          i≈k⇒j≈k = λ i≈k → ≤-antisym j≤k $ ≤-trans (from ≤⇔<∨≈ $ inj₂ (≈-sym i≈k)) i≤j
-        in
-          ≤∧≉⇒< (≤-trans i≤j j≤k , (proj₂ $ <⇒≤∧≉ j<k) ∘ i≈k⇒j≈k)
-
-      <⇒¬>⊎≈ : ∀ {x y} → x < y → ¬ (y < x ⊎ y ≈ x)
-      <⇒¬>⊎≈ x<y (inj₁ y<x) = <-asymmetric x<y y<x
-      <⇒¬>⊎≈ x<y (inj₂ x≈y) = <-irrefl (≈-sym x≈y) x<y
-
-    record HasDecPartialOrder : Set (suc a) where
-      field
-        ⦃ hasPartialOrder ⦄ : HasPartialOrder
-        ⦃ dec-≤ ⦄ : _≤_ ⁇²
-        ⦃ dec-< ⦄ : _<_ ⁇²
-
-  HasPreorder≡        = HasPreorder {_≈_ = _≡_}
-  HasDecPreorder≡     = HasDecPreorder {_≈_ = _≡_}
-  HasPartialOrder≡    = HasPartialOrder {_≈_ = _≡_}
-  HasDecPartialOrder≡ = HasDecPartialOrder {_≈_ = _≡_}
-
-open HasPreorder ⦃...⦄ public
-open HasPartialOrder ⦃...⦄ public hiding (hasPreorder)
-open HasDecPartialOrder ⦃...⦄ public hiding (hasPartialOrder)
-
-module _ {a} {A : Set a} {_≈_ : Rel A a} where
-
-  module _ {_≤_ : Rel A a} where
-    import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as SNS
-
-    module _ (≤-isPreorder : IsPreorder _≈_ _≤_)
-             (_≈?_ : Decidable² _≈_) where
-
-      hasPreorderFromNonStrict : HasPreorder
-      hasPreorderFromNonStrict = record
-        { _≤_           = _≤_
-        ; _<_           = SNS._<_
-        ; ≤-isPreorder  = ≤-isPreorder
-        ; <-irrefl      = SNS.<-irrefl
-        ; ≤⇔<∨≈         = λ {a b} → mk⇔
-          (λ a≤b → case (a ≈? b) of λ where (yes p) → inj₂ p ; (no ¬p) → inj₁ (a≤b , ¬p))
-          λ where (inj₁ a<b) → proj₁ a<b ; (inj₂ a≈b) → IsPreorder.reflexive ≤-isPreorder a≈b
-        }
-
-      hasPartialOrderFromNonStrict : Antisymmetric _≈_ _≤_ → HasPartialOrder
-      hasPartialOrderFromNonStrict antsym  = record
-        { hasPreorder = hasPreorderFromNonStrict
-        ; ≤-antisym = antsym
-        }
-
-  module _ {_<_ : Rel A a} where
-
-    import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_ as SNS
-
-    module _ (<-isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_) where
-
-        hasPreorderFromStrictPartialOrder : HasPreorder
-        hasPreorderFromStrictPartialOrder = record
-          { _≤_ = SNS._≤_
-          ; _<_ = _<_
-          ; ≤-isPreorder = SNS.isPreorder₂ <-isStrictPartialOrder
-          ; <-irrefl = <-isStrictPartialOrder .IsStrictPartialOrder.irrefl
-          ; ≤⇔<∨≈ = mk⇔ id id
-          }
-
-        instance _ = hasPreorderFromStrictPartialOrder
-
-        hasPartialOrderFromStrictPartialOrder : HasPartialOrder
-        hasPartialOrderFromStrictPartialOrder = record
-          { hasPreorder = hasPreorderFromStrictPartialOrder
-          ; ≤-antisym = SNS.isPartialOrder <-isStrictPartialOrder .IsPartialOrder.antisym
-          }
-
-
-    module _ (<-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_) where
-
-      private spo = IsStrictTotalOrder.isStrictPartialOrder <-isStrictTotalOrder
-
-      hasPreorderFromStrictTotalOrder : HasPreorder
-      hasPreorderFromStrictTotalOrder = hasPreorderFromStrictPartialOrder spo
-
-      hasPartialOrderFromStrictTotalOrder : HasPartialOrder
-      hasPartialOrderFromStrictTotalOrder = hasPartialOrderFromStrictPartialOrder spo
+open import Class.HasOrder.Core public
+open import Class.HasOrder.Instance public
diff --git a/Class/HasOrder/Core.agda b/Class/HasOrder/Core.agda
new file mode 100644
index 0000000..8a2c056
--- /dev/null
+++ b/Class/HasOrder/Core.agda
@@ -0,0 +1,160 @@
+{-# OPTIONS --safe #-}
+
+module Class.HasOrder.Core where
+
+open import Class.Decidable
+open import Data.Empty
+open import Data.Product
+open import Data.Sum
+open import Function
+open import Level
+open import Relation.Binary
+open import Relation.Binary using () renaming (Decidable to Decidable²)
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+
+open Equivalence
+
+module _ {a} {A : Set a} where
+  module _ {_≈_ : Rel A a} where
+
+    record HasPreorder : Set (suc a) where
+      infix 4 _≤_ _<_ _≥_ _>_
+      field
+        _≤_ _<_       : Rel A a
+        ≤-isPreorder  : IsPreorder _≈_ _≤_
+        <-irrefl      : Irreflexive _≈_ _<_
+        ≤⇔<∨≈         : ∀ {x y} → x ≤ y ⇔ (x < y ⊎ x ≈ y)
+
+      _≥_ = flip _≤_
+      _>_ = flip _<_
+
+      open IsPreorder ≤-isPreorder public
+        using ()
+        renaming (isEquivalence to ≈-isEquivalence; refl to ≤-refl; trans to ≤-trans)
+
+      _≤?_ : ⦃ _≤_ ⁇² ⦄ → Decidable _≤_
+      _≤?_ = dec²
+
+      _<?_ : ⦃ _<_ ⁇² ⦄ → Decidable _<_
+      _<?_ = dec²
+
+      infix 4 _<?_ _≤?_
+
+      <⇒≤∧≉ : ∀ {x y} → x < y → x ≤ y × ¬ (x ≈ y)
+      <⇒≤∧≉ x<y = from ≤⇔<∨≈ (inj₁ x<y) , λ x≈y → <-irrefl x≈y x<y
+
+      ≤∧≉⇒< : ∀ {x y} → x ≤ y × ¬ (x ≈ y) → x < y
+      ≤∧≉⇒< {x} {y} (x≤y , ¬x≈y) with to ≤⇔<∨≈ x≤y
+      ... | inj₁ x<y = x<y
+      ... | inj₂ x≈y = ⊥-elim (¬x≈y x≈y)
+
+      ≤-antisym⇒<-asym : Antisymmetric _≈_ _≤_ → Asymmetric _<_
+      ≤-antisym⇒<-asym antisym x<y y<x =
+        proj₂ (<⇒≤∧≉ x<y) $ antisym (proj₁ $ <⇒≤∧≉ x<y) (proj₁ $ <⇒≤∧≉ y<x)
+
+    open HasPreorder ⦃...⦄
+
+    record HasDecPreorder : Set (suc a) where
+      field ⦃ hasPreorder ⦄ : HasPreorder
+            ⦃ dec-≤ ⦄ : _≤_ ⁇²
+            ⦃ dec-< ⦄ : _<_ ⁇²
+
+    record HasPartialOrder : Set (suc a) where
+      field
+        ⦃ hasPreorder ⦄ : HasPreorder
+        ≤-antisym : Antisymmetric _≈_ _≤_
+
+      ≤-isPartialOrder : IsPartialOrder _≈_ _≤_
+      ≤-isPartialOrder = record { isPreorder = ≤-isPreorder ; antisym = ≤-antisym }
+
+      <-asymmetric : Asymmetric _<_
+      <-asymmetric = ≤-antisym⇒<-asym ≤-antisym
+
+      open IsEquivalence ≈-isEquivalence renaming (sym to ≈-sym)
+
+      <-trans : Transitive _<_
+      <-trans i<j j<k =
+        let
+          j≤k = proj₁ $ <⇒≤∧≉ j<k; i≤j = proj₁ $ <⇒≤∧≉ i<j
+          i≈k⇒j≈k = λ i≈k → ≤-antisym j≤k $ ≤-trans (from ≤⇔<∨≈ $ inj₂ (≈-sym i≈k)) i≤j
+        in
+          ≤∧≉⇒< (≤-trans i≤j j≤k , (proj₂ $ <⇒≤∧≉ j<k) ∘ i≈k⇒j≈k)
+
+      <⇒¬>⊎≈ : ∀ {x y} → x < y → ¬ (y < x ⊎ y ≈ x)
+      <⇒¬>⊎≈ x<y (inj₁ y<x) = <-asymmetric x<y y<x
+      <⇒¬>⊎≈ x<y (inj₂ x≈y) = <-irrefl (≈-sym x≈y) x<y
+
+    record HasDecPartialOrder : Set (suc a) where
+      field
+        ⦃ hasPartialOrder ⦄ : HasPartialOrder
+        ⦃ dec-≤ ⦄ : _≤_ ⁇²
+        ⦃ dec-< ⦄ : _<_ ⁇²
+
+  HasPreorder≡        = HasPreorder {_≈_ = _≡_}
+  HasDecPreorder≡     = HasDecPreorder {_≈_ = _≡_}
+  HasPartialOrder≡    = HasPartialOrder {_≈_ = _≡_}
+  HasDecPartialOrder≡ = HasDecPartialOrder {_≈_ = _≡_}
+
+open HasPreorder ⦃...⦄ public
+open HasPartialOrder ⦃...⦄ public hiding (hasPreorder)
+open HasDecPartialOrder ⦃...⦄ public hiding (hasPartialOrder)
+
+module _ {a} {A : Set a} {_≈_ : Rel A a} where
+
+  module _ {_≤_ : Rel A a} where
+    import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as SNS
+
+    module _ (≤-isPreorder : IsPreorder _≈_ _≤_)
+             (_≈?_ : Decidable² _≈_) where
+
+      hasPreorderFromNonStrict : HasPreorder
+      hasPreorderFromNonStrict = record
+        { _≤_           = _≤_
+        ; _<_           = SNS._<_
+        ; ≤-isPreorder  = ≤-isPreorder
+        ; <-irrefl      = SNS.<-irrefl
+        ; ≤⇔<∨≈         = λ {a b} → mk⇔
+          (λ a≤b → case (a ≈? b) of λ where (yes p) → inj₂ p ; (no ¬p) → inj₁ (a≤b , ¬p))
+          λ where (inj₁ a<b) → proj₁ a<b ; (inj₂ a≈b) → IsPreorder.reflexive ≤-isPreorder a≈b
+        }
+
+      hasPartialOrderFromNonStrict : Antisymmetric _≈_ _≤_ → HasPartialOrder
+      hasPartialOrderFromNonStrict antsym  = record
+        { hasPreorder = hasPreorderFromNonStrict
+        ; ≤-antisym = antsym
+        }
+
+  module _ {_<_ : Rel A a} where
+
+    import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_ as SNS
+
+    module _ (<-isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_) where
+
+        hasPreorderFromStrictPartialOrder : HasPreorder
+        hasPreorderFromStrictPartialOrder = record
+          { _≤_ = SNS._≤_
+          ; _<_ = _<_
+          ; ≤-isPreorder = SNS.isPreorder₂ <-isStrictPartialOrder
+          ; <-irrefl = <-isStrictPartialOrder .IsStrictPartialOrder.irrefl
+          ; ≤⇔<∨≈ = mk⇔ id id
+          }
+
+        instance _ = hasPreorderFromStrictPartialOrder
+
+        hasPartialOrderFromStrictPartialOrder : HasPartialOrder
+        hasPartialOrderFromStrictPartialOrder = record
+          { hasPreorder = hasPreorderFromStrictPartialOrder
+          ; ≤-antisym = SNS.isPartialOrder <-isStrictPartialOrder .IsPartialOrder.antisym
+          }
+
+
+    module _ (<-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_) where
+
+      private spo = IsStrictTotalOrder.isStrictPartialOrder <-isStrictTotalOrder
+
+      hasPreorderFromStrictTotalOrder : HasPreorder
+      hasPreorderFromStrictTotalOrder = hasPreorderFromStrictPartialOrder spo
+
+      hasPartialOrderFromStrictTotalOrder : HasPartialOrder
+      hasPartialOrderFromStrictTotalOrder = hasPartialOrderFromStrictPartialOrder spo
diff --git a/Class/HasOrder/Instances.agda b/Class/HasOrder/Instance.agda
similarity index 95%
rename from Class/HasOrder/Instances.agda
rename to Class/HasOrder/Instance.agda
index 7590c9d..9c21070 100644
--- a/Class/HasOrder/Instances.agda
+++ b/Class/HasOrder/Instance.agda
@@ -1,10 +1,10 @@
 {-# OPTIONS --safe #-}
 
-module Class.HasOrder.Instances where
+module Class.HasOrder.Instance where
 
 open import Class.DecEq
 open import Class.Decidable
-open import Class.HasOrder
+open import Class.HasOrder.Core
 open import Data.Integer using (ℤ)
 open import Data.Nat using (ℕ)
 open import Data.Rational using (ℚ)