Imported Upstream version 0.12

1 files changed, 4 insertions, 2 deletions

diff --git a/src/Relation/Binary.agda b/src/Relation/Binary.agda
index 27fc8e0..54fef09 100644
--- a/src/Relation/Binary.agda
+++ b/src/Relation/Binary.agda
@@ -358,7 +358,6 @@ record IsStrictTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
     isEquivalence : IsEquivalence _≈_
     trans         : Transitive _<_
     compare       : Trichotomous _≈_ _<_
-    <-resp-≈      : _<_ Respects₂ _≈_
 
   infix 4 _≟_ _<?_
 
@@ -376,10 +375,13 @@ record IsStrictTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
 
   module Eq = IsDecEquivalence isDecEquivalence
 
+  <-resp-≈ : _<_ Respects₂ _≈_
+  <-resp-≈ = trans∧tri⟶resp≈ Eq.sym Eq.trans trans compare
+
   isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
   isStrictPartialOrder = record
     { isEquivalence = isEquivalence
-    ; irrefl        = tri⟶irr <-resp-≈ Eq.sym compare
+    ; irrefl        = tri⟶irr compare
     ; trans         = trans
     ; <-resp-≈      = <-resp-≈
     }