From fe2b3bddc38d2a17809e5b4a5b31be81d8812ddb Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Thu, 12 Oct 2023 17:44:00 +0900
Subject: [PATCH 1/2] Change definition of IsStrictTotalOrder

---
 CHANGELOG.md                                  | 40 +++++++++++++++
 src/Data/Bool/Properties.agda                 |  5 +-
 src/Data/Char/Properties.agda                 |  5 +-
 src/Data/Fin/Properties.agda                  |  5 +-
 src/Data/Integer/Properties.agda              |  5 +-
 src/Data/List/Relation/Binary/Lex/Strict.agda |  5 +-
 src/Data/Nat/Binary/Properties.agda           |  5 +-
 src/Data/Nat/Properties.agda                  |  9 +---
 .../Product/Relation/Binary/Lex/Strict.agda   |  9 ++--
 src/Data/Rational/Properties.agda             |  5 +-
 .../Rational/Unnormalised/Properties.agda     |  5 +-
 src/Data/Sum/Relation/Binary/LeftOrder.agda   |  5 +-
 src/Data/Vec/Relation/Binary/Lex/Strict.agda  |  3 +-
 src/Induction/WellFounded.agda                |  4 +-
 src/Relation/Binary.agda                      |  1 +
 src/Relation/Binary/Bundles.agda              |  2 +-
 .../Binary/Construct/Add/Infimum/Strict.agda  | 10 ++--
 .../Binary/Construct/Add/Supremum/Strict.agda | 10 ++--
 .../Binary/Construct/Flip/EqAndOrd.agda       |  5 +-
 src/Relation/Binary/Construct/Flip/Ord.agda   |  5 +-
 .../Binary/Construct/NonStrictToStrict.agda   |  5 +-
 src/Relation/Binary/Construct/On.agda         |  5 +-
 .../Binary/Morphism/OrderMonomorphism.agda    |  5 +-
 src/Relation/Binary/Structures.agda           | 51 ++++++++++---------
 src/Relation/Binary/Structures/Biased.agda    | 49 ++++++++++++++++++
 25 files changed, 162 insertions(+), 96 deletions(-)
 create mode 100644 src/Relation/Binary/Structures/Biased.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 988355bd5a..cf452b2bd0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -918,6 +918,46 @@ Non-backwards compatible changes
 
 * The old names (and the names of all proofs about these functions) have been deprecated appropriately.
 
+### Changes to definition of `IsStrictTotalOrder`
+
+* The previous definition of the record `IsStrictTotalOrder` did not build upon `IsStrictPartialOrder`
+  as would be expected. Instead it omitted several fields like irreflexivity as they were derivable from the
+  proof of trichotomy. However, this led to problems further up the hierarchy where bundles such as `StrictTotalOrder`
+  which contained multiple distinct proofs of `IsStrictPartialOrder`.
+  
+* To remedy this the definition of `IsStrictTotalOrder` has been changed to so that it builds upon 
+  `IsStrictPartialOrder` as would be expected. 
+
+* To aid migration, the old record definition has been moved to `Relation.Binary.Structures.Biased`
+  which contains the `isStrictTotalOrderᶜ` smart constructor (which is re-exported by `Relation.Binary`) . 
+  Therefore the old code:
+  ```agda
+  <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
+  <-isStrictTotalOrder = record
+	{ isEquivalence = isEquivalence
+	; trans         = <-trans
+	; compare       = <-cmp
+	}
+  ```
+  can be migrated either by updating to the new record fields if you have a proof of `IsStrictPartialOrder`
+  available:
+  ```agda
+  <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
+  <-isStrictTotalOrder = record
+	{ isStrictPartialOrder = <-isStrictPartialOrder
+	; compare              = <-cmp
+	}
+  ```
+  or simply applying the smart constructor to the record definition as follows:
+  ```agda
+  <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
+  <-isStrictTotalOrder = isStrictTotalOrderᶜ record
+	{ isEquivalence = isEquivalence
+	; trans         = <-trans
+	; compare       = <-cmp
+	}
+  ```
+  
 ### Changes to triple reasoning interface
 
 * The module `Relation.Binary.Reasoning.Base.Triple` now takes an extra proof that the strict
diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index 3c1c25d245..e911390366 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -210,9 +210,8 @@ true  <? _     = no  (λ())
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
 <-isStrictTotalOrder = record
-  { isEquivalence = isEquivalence
-  ; trans         = <-trans
-  ; compare       = <-cmp
+  { isStrictPartialOrder = <-isStrictPartialOrder
+  ; compare              = <-cmp
   }
 
 -- Bundles
diff --git a/src/Data/Char/Properties.agda b/src/Data/Char/Properties.agda
index 970eb6249a..c399bf30e3 100644
--- a/src/Data/Char/Properties.agda
+++ b/src/Data/Char/Properties.agda
@@ -123,9 +123,8 @@ _<?_ = On.decidable toℕ ℕ._<_ ℕₚ._<?_
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
 <-isStrictTotalOrder = record
-  { isEquivalence = PropEq.isEquivalence
-  ; trans         = λ {a} {b} {c} → <-trans {a} {b} {c}
-  ; compare       = <-cmp
+  { isStrictPartialOrder = <-isStrictPartialOrder
+  ; compare              = <-cmp
   }
 
 <-strictPartialOrder : StrictPartialOrder _ _ _
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index ea7c43c90f..eb5a7f5011 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -406,9 +406,8 @@ m <? n = suc (toℕ m) ℕₚ.≤? toℕ n
 
 <-isStrictTotalOrder : IsStrictTotalOrder {A = Fin n} _≡_ _<_
 <-isStrictTotalOrder = record
-  { isEquivalence = P.isEquivalence
-  ; trans         = <-trans
-  ; compare       = <-cmp
+  { isStrictPartialOrder = <-isStrictPartialOrder
+  ; compare              = <-cmp
   }
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index 21b3f3d71c..bfe29c4079 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -331,9 +331,8 @@ _<?_ : Decidable _<_
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
 <-isStrictTotalOrder = record
-  { isEquivalence = isEquivalence
-  ; trans         = <-trans
-  ; compare       = <-cmp
+  { isStrictPartialOrder = <-isStrictPartialOrder
+  ; compare              = <-cmp
   }
 
 ------------------------------------------------------------------------
diff --git a/src/Data/List/Relation/Binary/Lex/Strict.agda b/src/Data/List/Relation/Binary/Lex/Strict.agda
index 7b7f5d2baf..277996594f 100644
--- a/src/Data/List/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/List/Relation/Binary/Lex/Strict.agda
@@ -121,9 +121,8 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
     <-isStrictTotalOrder : IsStrictTotalOrder _≈_ _≺_ →
                            IsStrictTotalOrder _≋_ _<_
     <-isStrictTotalOrder sto = record
-      { isEquivalence = Pointwise.isEquivalence isEquivalence
-      ; trans         = <-transitive isEquivalence <-resp-≈ trans
-      ; compare       = <-compare Eq.sym compare
+      { isStrictPartialOrder = <-isStrictPartialOrder isStrictPartialOrder
+      ; compare              = <-compare Eq.sym compare
       } where open IsStrictTotalOrder sto
 
 <-strictPartialOrder : ∀ {a ℓ₁ ℓ₂} → StrictPartialOrder a ℓ₁ ℓ₂ →
diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda
index 6109106b26..8c08974636 100644
--- a/src/Data/Nat/Binary/Properties.agda
+++ b/src/Data/Nat/Binary/Properties.agda
@@ -414,9 +414,8 @@ _<?_ = tri⇒dec< <-cmp
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
 <-isStrictTotalOrder = record
-  { isEquivalence = isEquivalence
-  ; trans         = <-trans
-  ; compare       = <-cmp
+  { isStrictPartialOrder = <-isStrictPartialOrder
+  ; compare              = <-cmp
   }
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index dcc6746f93..915d1d7d1b 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -32,12 +32,7 @@ open import Level using (0ℓ)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary.Core
   using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Binary.Bundles
-  using (DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder)
-open import Relation.Binary.Structures
-  using (IsDecEquivalence; IsPreorder; IsTotalPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder)
-open import Relation.Binary.Definitions
-  using (DecidableEquality; Irrelevant; Reflexive; Antisymmetric; Transitive; Total; Decidable; Connex; Irreflexive; Asymmetric; LeftTrans; RightTrans; Trichotomous; tri≈; tri>; tri<; _Respects₂_)
+open import Relation.Binary
 open import Relation.Binary.Consequences using (flip-Connex)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary hiding (Irrelevant)
@@ -402,7 +397,7 @@ _>?_ = flip _<?_
   }
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
-<-isStrictTotalOrder = record
+<-isStrictTotalOrder = isStrictTotalOrderᶜ record
   { isEquivalence = isEquivalence
   ; trans         = <-trans
   ; compare       = <-cmp
diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda
index 96adc9b9e1..42d139893d 100644
--- a/src/Data/Product/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/Product/Relation/Binary/Lex/Strict.agda
@@ -269,12 +269,9 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂}
                          IsStrictTotalOrder _≋_ _<ₗₑₓ_
   ×-isStrictTotalOrder spo₁ spo₂ =
     record
-      { isEquivalence = Pointwise.×-isEquivalence
-                          (isEquivalence spo₁) (isEquivalence spo₂)
-      ; trans         = ×-transitive {_<₁_ = _<₁_} {_<₂_ = _<₂_}
-                          (isEquivalence spo₁)
-                          (<-resp-≈ spo₁) (trans spo₁)
-                          (trans spo₂)
+      { isStrictPartialOrder = ×-isStrictPartialOrder
+                                 (isStrictPartialOrder spo₁)
+                                 (isStrictPartialOrder spo₂)
       ; compare       = ×-compare (Eq.sym spo₁) (compare spo₁)
                                                 (compare spo₂)
       }
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index eab0c0cf2c..79d34870ef 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -702,9 +702,8 @@ _>?_ = flip _<?_
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
 <-isStrictTotalOrder = record
-  { isEquivalence = isEquivalence
-  ; trans         = <-trans
-  ; compare       = <-cmp
+  { isStrictPartialOrder = <-isStrictPartialOrder
+  ; compare              = <-cmp
   }
 
 <-isDenseLinearOrder : IsDenseLinearOrder _≡_ _<_
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index 4e86729725..11b0b4a5d7 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -542,9 +542,8 @@ _>?_ = flip _<?_
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≃_ _<_
 <-isStrictTotalOrder = record
-  { isEquivalence = ≃-isEquivalence
-  ; trans         = <-trans
-  ; compare       = <-cmp
+  { isStrictPartialOrder = <-isStrictPartialOrder
+  ; compare              = <-cmp
   }
 
 <-isDenseLinearOrder : IsDenseLinearOrder _≃_ _<_
diff --git a/src/Data/Sum/Relation/Binary/LeftOrder.agda b/src/Data/Sum/Relation/Binary/LeftOrder.agda
index 397bc598dc..416d71f15a 100644
--- a/src/Data/Sum/Relation/Binary/LeftOrder.agda
+++ b/src/Data/Sum/Relation/Binary/LeftOrder.agda
@@ -192,9 +192,8 @@ module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
                            IsStrictTotalOrder ≈₂ ∼₂ →
                            IsStrictTotalOrder (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
   ⊎-<-isStrictTotalOrder sto₁ sto₂ = record
-    { isEquivalence = PW.⊎-isEquivalence (isEquivalence sto₁) (isEquivalence sto₂)
-    ; trans         = ⊎-<-transitive (trans sto₁) (trans sto₂)
-    ; compare       = ⊎-<-trichotomous (compare sto₁) (compare sto₂)
+    { isStrictPartialOrder = ⊎-<-isStrictPartialOrder (isStrictPartialOrder sto₁) (isStrictPartialOrder sto₂)
+    ; compare              = ⊎-<-trichotomous (compare sto₁) (compare sto₂)
     }
     where open IsStrictTotalOrder
 
diff --git a/src/Data/Vec/Relation/Binary/Lex/Strict.agda b/src/Data/Vec/Relation/Binary/Lex/Strict.agda
index 944edb4927..0cd7fde477 100644
--- a/src/Data/Vec/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/Strict.agda
@@ -168,8 +168,7 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
   <-isStrictTotalOrder : IsStrictTotalOrder _≈_ _≺_ →
                          ∀ {n} → IsStrictTotalOrder (_≋_ {n} {n}) _<_
   <-isStrictTotalOrder ≺-isStrictTotalOrder {n} = record
-    { isEquivalence = Pointwise.isEquivalence O.isEquivalence n
-    ; trans         = <-trans O.Eq.isPartialEquivalence O.<-resp-≈ O.trans
+    { isStrictPartialOrder = <-isStrictPartialOrder O.isStrictPartialOrder
     ; compare       = <-cmp O.Eq.sym O.compare
     } where module O = IsStrictTotalOrder ≺-isStrictTotalOrder
 
diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda
index fb3ed14255..1dac16c059 100644
--- a/src/Induction/WellFounded.agda
+++ b/src/Induction/WellFounded.agda
@@ -14,7 +14,7 @@ open import Induction
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions
-  using (Symmetric; Asymmetric; Irreflexive; _Respects₂_; 
+  using (Symmetric; Asymmetric; Irreflexive; _Respects₂_;
     _Respectsʳ_; _Respects_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Binary.Consequences using (asym⇒irr)
@@ -130,7 +130,7 @@ module _ {_<_ : Rel A r} where
   wf⇒asym : WellFounded _<_ → Asymmetric _<_
   wf⇒asym wf = acc⇒asym (wf _)
 
-  wf⇒irrefl : {_≈_ : Rel A ℓ} → _<_ Respects₂ _≈_ → 
+  wf⇒irrefl : {_≈_ : Rel A ℓ} → _<_ Respects₂ _≈_ →
               Symmetric _≈_ → WellFounded _<_ → Irreflexive _≈_ _<_
   wf⇒irrefl r s wf = asym⇒irr r s (wf⇒asym wf)
 
diff --git a/src/Relation/Binary.agda b/src/Relation/Binary.agda
index 95b2ca002a..efdd9921f9 100644
--- a/src/Relation/Binary.agda
+++ b/src/Relation/Binary.agda
@@ -14,4 +14,5 @@ module Relation.Binary where
 open import Relation.Binary.Core public
 open import Relation.Binary.Definitions public
 open import Relation.Binary.Structures public
+open import Relation.Binary.Structures.Biased public
 open import Relation.Binary.Bundles public
diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda
index 90e3c7e2ac..eb7975f376 100644
--- a/src/Relation/Binary/Bundles.agda
+++ b/src/Relation/Binary/Bundles.agda
@@ -100,7 +100,7 @@ record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   _≳_ = flip _≲_
 
   -- Deprecated.
-  infix 4 _∼_ 
+  infix 4 _∼_
   _∼_ = _≲_
   {-# WARNING_ON_USAGE _∼_
   "Warning: _∼_ was deprecated in v2.0.
diff --git a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
index ae96849340..5f3bdd7622 100644
--- a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
+++ b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
@@ -153,9 +153,8 @@ module _ {e} {_≈_ : Rel A e} where
 <₋-isStrictTotalOrder-≡ : IsStrictTotalOrder _≡_ _<_ →
                           IsStrictTotalOrder _≡_ _<₋_
 <₋-isStrictTotalOrder-≡ strictot = record
-  { isEquivalence = P.isEquivalence
-  ; trans         = <₋-trans trans
-  ; compare       = <₋-cmp-≡ compare
+  { isStrictPartialOrder = <₋-isStrictPartialOrder-≡ isStrictPartialOrder
+  ; compare              = <₋-cmp-≡ compare
   } where open IsStrictTotalOrder strictot
 
 ------------------------------------------------------------------------
@@ -185,7 +184,6 @@ module _ {e} {_≈_ : Rel A e} where
   <₋-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_ →
                           IsStrictTotalOrder _≈₋_ _<₋_
   <₋-isStrictTotalOrder strictot = record
-    { isEquivalence = ≈₋-isEquivalence isEquivalence
-    ; trans         = <₋-trans trans
-    ; compare       = <₋-cmp compare
+    { isStrictPartialOrder = <₋-isStrictPartialOrder isStrictPartialOrder
+    ; compare              = <₋-cmp compare
     } where open IsStrictTotalOrder strictot
diff --git a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
index d927cf45c4..733981deb0 100644
--- a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
+++ b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
@@ -154,9 +154,8 @@ module _ {e} {_≈_ : Rel A e} where
 <⁺-isStrictTotalOrder-≡ : IsStrictTotalOrder _≡_ _<_ →
                           IsStrictTotalOrder _≡_ _<⁺_
 <⁺-isStrictTotalOrder-≡ strictot = record
-  { isEquivalence = P.isEquivalence
-  ; trans         = <⁺-trans trans
-  ; compare       = <⁺-cmp-≡ compare
+  { isStrictPartialOrder = <⁺-isStrictPartialOrder-≡ isStrictPartialOrder
+  ; compare              = <⁺-cmp-≡ compare
   } where open IsStrictTotalOrder strictot
 
 ------------------------------------------------------------------------
@@ -186,7 +185,6 @@ module _ {e} {_≈_ : Rel A e} where
   <⁺-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_ →
                           IsStrictTotalOrder _≈⁺_ _<⁺_
   <⁺-isStrictTotalOrder strictot = record
-    { isEquivalence = ≈⁺-isEquivalence isEquivalence
-    ; trans         = <⁺-trans trans
-    ; compare       = <⁺-cmp compare
+    { isStrictPartialOrder = <⁺-isStrictPartialOrder isStrictPartialOrder
+    ; compare              = <⁺-cmp compare
     } where open IsStrictTotalOrder strictot
diff --git a/src/Relation/Binary/Construct/Flip/EqAndOrd.agda b/src/Relation/Binary/Construct/Flip/EqAndOrd.agda
index 78671dfbdc..122842f967 100644
--- a/src/Relation/Binary/Construct/Flip/EqAndOrd.agda
+++ b/src/Relation/Binary/Construct/Flip/EqAndOrd.agda
@@ -145,9 +145,8 @@ isStrictPartialOrder {< = <} O = record
 isStrictTotalOrder : IsStrictTotalOrder ≈ < →
                      IsStrictTotalOrder ≈ (flip <)
 isStrictTotalOrder {< = <} O = record
-  { isEquivalence = O.isEquivalence
-  ; trans         = trans < O.trans
-  ; compare       = compare _ O.compare
+  { isStrictPartialOrder = isStrictPartialOrder O.isStrictPartialOrder
+  ; compare              = compare _ O.compare
   } where module O = IsStrictTotalOrder O
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Binary/Construct/Flip/Ord.agda b/src/Relation/Binary/Construct/Flip/Ord.agda
index 742a315cc6..64d41fdb77 100644
--- a/src/Relation/Binary/Construct/Flip/Ord.agda
+++ b/src/Relation/Binary/Construct/Flip/Ord.agda
@@ -139,9 +139,8 @@ isStrictPartialOrder {≈ = ≈} {< = <} O = record
 isStrictTotalOrder : IsStrictTotalOrder ≈ < →
                      IsStrictTotalOrder (flip ≈) (flip <)
 isStrictTotalOrder {≈ = ≈} {< = <} O = record
-  { isEquivalence = isEquivalence O.isEquivalence
-  ; trans         = transitive < O.trans
-  ; compare       = trichotomous ≈ < O.compare
+  { isStrictPartialOrder = isStrictPartialOrder O.isStrictPartialOrder
+  ; compare              = trichotomous ≈ < O.compare
   } where module O = IsStrictTotalOrder O
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Binary/Construct/NonStrictToStrict.agda b/src/Relation/Binary/Construct/NonStrictToStrict.agda
index c2eb114004..f0402d7fb9 100644
--- a/src/Relation/Binary/Construct/NonStrictToStrict.agda
+++ b/src/Relation/Binary/Construct/NonStrictToStrict.agda
@@ -138,9 +138,8 @@ x < y = x ≤ y × x ≉ y
 <-isStrictTotalOrder₁ : Decidable _≈_ → IsTotalOrder _≈_ _≤_ →
                         IsStrictTotalOrder _≈_ _<_
 <-isStrictTotalOrder₁ ≟ tot = record
-  { isEquivalence = isEquivalence
-  ; trans         = <-trans isPartialOrder
-  ; compare       = <-trichotomous Eq.sym ≟ antisym total
+  { isStrictPartialOrder = <-isStrictPartialOrder isPartialOrder
+  ; compare              = <-trichotomous Eq.sym ≟ antisym total
   } where open IsTotalOrder tot
 
 <-isStrictTotalOrder₂ : IsDecTotalOrder _≈_ _≤_ →
diff --git a/src/Relation/Binary/Construct/On.agda b/src/Relation/Binary/Construct/On.agda
index c124f98dd8..5544edbf4a 100644
--- a/src/Relation/Binary/Construct/On.agda
+++ b/src/Relation/Binary/Construct/On.agda
@@ -150,9 +150,8 @@ module _ (f : B → A) {≈ : Rel A ℓ₁} {∼ : Rel A ℓ₂} where
   isStrictTotalOrder : IsStrictTotalOrder ≈ ∼ →
                        IsStrictTotalOrder (≈ on f) (∼ on f)
   isStrictTotalOrder sto = record
-    { isEquivalence = isEquivalence f Sto.isEquivalence
-    ; trans         = transitive f ∼ Sto.trans
-    ; compare       = trichotomous f ≈ ∼ Sto.compare
+    { isStrictPartialOrder = isStrictPartialOrder Sto.isStrictPartialOrder
+    ; compare              = trichotomous _ _ _ Sto.compare
     } where module Sto = IsStrictTotalOrder sto
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Binary/Morphism/OrderMonomorphism.agda b/src/Relation/Binary/Morphism/OrderMonomorphism.agda
index ca3ce3677a..12a80d1f31 100644
--- a/src/Relation/Binary/Morphism/OrderMonomorphism.agda
+++ b/src/Relation/Binary/Morphism/OrderMonomorphism.agda
@@ -105,7 +105,6 @@ isStrictPartialOrder O = record
 isStrictTotalOrder : IsStrictTotalOrder _≈₂_ _≲₂_ →
                      IsStrictTotalOrder _≈₁_ _≲₁_
 isStrictTotalOrder O = record
-  { isEquivalence = EqM.isEquivalence O.isEquivalence
-  ; trans         = trans O.trans
-  ; compare       = compare O.compare
+  { isStrictPartialOrder = isStrictPartialOrder O.isStrictPartialOrder
+  ; compare              = compare O.compare
   } where module O = IsStrictTotalOrder O
diff --git a/src/Relation/Binary/Structures.agda b/src/Relation/Binary/Structures.agda
index 751c774da3..4ac059ea12 100644
--- a/src/Relation/Binary/Structures.agda
+++ b/src/Relation/Binary/Structures.agda
@@ -235,16 +235,18 @@ record IsDecTotalOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
 
 
 -- Note that these orders are decidable. The current implementation
--- of `Trichotomous` subsumes irreflexivity and asymmetry. Any reasonable
--- definition capturing these three properties implies decidability
--- as `Trichotomous` necessarily separates out the equality case.
+-- of `Trichotomous` subsumes irreflexivity and asymmetry.
 
 record IsStrictTotalOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
   field
-    isEquivalence : IsEquivalence
-    trans         : Transitive _<_
-    compare       : Trichotomous _≈_ _<_
+    isStrictPartialOrder : IsStrictPartialOrder _<_
+    compare              : Trichotomous _≈_ _<_
+
+  open IsStrictPartialOrder isStrictPartialOrder public
+    hiding (module Eq)
 
+  -- `Trichotomous` necessarily separates out the equality case so
+  --  it implies decidability.
   infix 4 _≟_ _<?_
 
   _≟_ : Decidable _≈_
@@ -253,22 +255,6 @@ record IsStrictTotalOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) wher
   _<?_ : Decidable _<_
   _<?_ = tri⇒dec< compare
 
-  isDecEquivalence : IsDecEquivalence
-  isDecEquivalence = record
-    { isEquivalence = isEquivalence
-    ; _≟_           = _≟_
-    }
-
-  module Eq = IsDecEquivalence isDecEquivalence
-
-  isStrictPartialOrder : IsStrictPartialOrder _<_
-  isStrictPartialOrder = record
-    { isEquivalence = isEquivalence
-    ; irrefl        = tri⇒irr compare
-    ; trans         = trans
-    ; <-resp-≈      = trans∧tri⇒resp Eq.sym Eq.trans trans compare
-    }
-
   isDecStrictPartialOrder : IsDecStrictPartialOrder _<_
   isDecStrictPartialOrder = record
     { isStrictPartialOrder = isStrictPartialOrder
@@ -276,9 +262,26 @@ record IsStrictTotalOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) wher
     ; _<?_                 = _<?_
     }
 
-  open IsStrictPartialOrder isStrictPartialOrder public
-    using (irrefl; asym; <-respʳ-≈; <-respˡ-≈; <-resp-≈)
+  -- Redefine the `Eq` module to include decidability proofs
+  module Eq where
+
+    isDecEquivalence : IsDecEquivalence
+    isDecEquivalence = record
+      { isEquivalence = isEquivalence
+      ; _≟_           = _≟_
+      }
 
+    open IsDecEquivalence isDecEquivalence public
+
+  isDecEquivalence : IsDecEquivalence
+  isDecEquivalence = record
+    { isEquivalence = isEquivalence
+    ; _≟_           = _≟_
+    }
+  {-# WARNING_ON_USAGE isDecEquivalence
+  "Warning: isDecEquivalence was deprecated in v2.0.
+  Please use Eq.isDecEquivalence instead. "
+  #-}
 
 record IsDenseLinearOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
   field
diff --git a/src/Relation/Binary/Structures/Biased.agda b/src/Relation/Binary/Structures/Biased.agda
new file mode 100644
index 0000000000..83636aa5d6
--- /dev/null
+++ b/src/Relation/Binary/Structures/Biased.agda
@@ -0,0 +1,49 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Ways to give instances of certain structures where some fields can
+-- be given in terms of others
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via `Relation.Binary`.
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Core
+
+module Relation.Binary.Structures.Biased
+  {a ℓ} {A : Set a} -- The underlying set
+  (_≈_ : Rel A ℓ)   -- The underlying equality relation
+  where
+
+open import Level using (Level; _⊔_)
+open import Relation.Binary.Consequences
+open import Relation.Binary.Definitions
+open import Relation.Binary.Structures _≈_
+
+private
+  variable
+    ℓ₂ : Level
+
+-- To construct a StrictTotalOrder you only need to prove transitivity and
+-- trichotomy as the current implementation of `Trichotomous` subsumes
+-- irreflexivity and asymmetry.
+record IsStrictTotalOrderᶜ (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+  field
+    isEquivalence : IsEquivalence
+    trans         : Transitive _<_
+    compare       : Trichotomous _≈_ _<_
+
+  isStrictTotalOrderᶜ : IsStrictTotalOrder _<_
+  isStrictTotalOrderᶜ = record
+    { isStrictPartialOrder = record
+      { isEquivalence = isEquivalence
+      ; irrefl = tri⇒irr compare
+      ; trans = trans
+      ; <-resp-≈ = trans∧tri⇒resp Eq.sym Eq.trans trans compare
+      }
+    ; compare = compare
+    } where module Eq = IsEquivalence isEquivalence
+
+open IsStrictTotalOrderᶜ public
+  using (isStrictTotalOrderᶜ)

From 0e2d5dfad0f3cac4f730397f055f9b46194a1b9c Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Thu, 12 Oct 2023 17:49:50 +0900
Subject: [PATCH 2/2] Add comment about baised definition to main definition

---
 src/Relation/Binary/Structures.agda | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Relation/Binary/Structures.agda b/src/Relation/Binary/Structures.agda
index 4ac059ea12..bf11d67250 100644
--- a/src/Relation/Binary/Structures.agda
+++ b/src/Relation/Binary/Structures.agda
@@ -235,7 +235,9 @@ record IsDecTotalOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
 
 
 -- Note that these orders are decidable. The current implementation
--- of `Trichotomous` subsumes irreflexivity and asymmetry.
+-- of `Trichotomous` subsumes irreflexivity and asymmetry. See
+-- `Relation.Binary.Structures.Biased` for ways of constructing this
+-- record without having to prove `isStrictPartialOrder`.
 
 record IsStrictTotalOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
   field