1 files changed, 45 insertions, 33 deletions

diff --git a/src/Relation/Binary.agda b/src/Relation/Binary.agda
index 54fef09..26fa333 100644
--- a/src/Relation/Binary.agda
+++ b/src/Relation/Binary.agda
@@ -6,21 +6,18 @@
 
 module Relation.Binary where
 
+open import Agda.Builtin.Equality using (_≡_)
 open import Data.Product
 open import Data.Sum
 open import Function
 open import Level
 import Relation.Binary.PropositionalEquality.Core as PropEq
-open import Relation.Binary.Consequences as Consequences
-open import Relation.Binary.Core as Core using (_≡_)
-import Relation.Binary.Indexed.Core as I
+open import Relation.Binary.Consequences
 
 ------------------------------------------------------------------------
 -- Simple properties and equivalence relations
 
-open Core public hiding (_≡_; refl; _≢_)
-
-open Consequences public using (Total)
+open import Relation.Binary.Core public
 
 ------------------------------------------------------------------------
 -- Preorders
@@ -40,9 +37,14 @@ record IsPreorder {a ℓ₁ ℓ₂} {A : Set a}
   refl : Reflexive _∼_
   refl = reflexive Eq.refl
 
+  ∼-respˡ-≈ : _∼_ Respectsˡ _≈_
+  ∼-respˡ-≈ x≈y x∼z = trans (reflexive (Eq.sym x≈y)) x∼z
+
+  ∼-respʳ-≈ : _∼_ Respectsʳ _≈_
+  ∼-respʳ-≈ x≈y z∼x = trans z∼x (reflexive x≈y)
+
   ∼-resp-≈ : _∼_ Respects₂ _≈_
-  ∼-resp-≈ = (λ x≈y z∼x → trans z∼x (reflexive x≈y))
-           , (λ x≈y x∼z → trans (reflexive $ Eq.sym x≈y) x∼z)
+  ∼-resp-≈ = ∼-respʳ-≈ , ∼-respˡ-≈
 
 record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix 4 _≈_ _∼_
@@ -78,19 +80,6 @@ record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
   preorder : Preorder c c ℓ
   preorder = record { isPreorder = isPreorder }
 
-  -- A trivially indexed setoid.
-
-  indexedSetoid : ∀ {i} {I : Set i} → I.Setoid I c _
-  indexedSetoid = record
-    { Carrier = λ _ → Carrier
-    ; _≈_     = _≈_
-    ; isEquivalence = record
-      { refl  = refl
-      ; sym   = sym
-      ; trans = trans
-      }
-    }
-
 ------------------------------------------------------------------------
 -- Decidable equivalence relations
 
@@ -128,7 +117,11 @@ record IsPartialOrder {a ℓ₁ ℓ₂} {A : Set a}
     antisym    : Antisymmetric _≈_ _≤_
 
   open IsPreorder isPreorder public
-         renaming (∼-resp-≈ to ≤-resp-≈)
+    renaming
+    ( ∼-respˡ-≈ to ≤-respˡ-≈
+    ; ∼-respʳ-≈ to ≤-respʳ-≈
+    ; ∼-resp-≈  to ≤-resp-≈
+    )
 
 record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix 4 _≈_ _≤_
@@ -207,6 +200,21 @@ record IsStrictPartialOrder {a ℓ₁ ℓ₂} {A : Set a}
 
   module Eq = IsEquivalence isEquivalence
 
+  asym : Asymmetric _<_
+  asym {x} {y} = trans∧irr⟶asym Eq.refl trans irrefl {x = x} {y}
+
+  <-respʳ-≈ : _<_ Respectsʳ _≈_
+  <-respʳ-≈ = proj₁ <-resp-≈
+
+  <-respˡ-≈ : _<_ Respectsˡ _≈_
+  <-respˡ-≈ = proj₂ <-resp-≈
+
+  asymmetric = asym
+  {-# WARNING_ON_USAGE asymmetric
+  "Warning: asymmetric was deprecated in v0.16.
+  Please use asym instead."
+  #-}
+
 record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix 4 _≈_ _<_
   field
@@ -217,10 +225,6 @@ record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂))
 
   open IsStrictPartialOrder isStrictPartialOrder public
 
-  asymmetric : Asymmetric _<_
-  asymmetric {x} {y} =
-    trans∧irr⟶asym Eq.refl trans irrefl {x = x} {y = y}
-
 ------------------------------------------------------------------------
 -- Decidable strict partial orders
 
@@ -308,15 +312,13 @@ record IsDecTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
     _≟_          : Decidable _≈_
     _≤?_         : Decidable _≤_
 
-  private
-    module TO = IsTotalOrder isTotalOrder
-  open TO public hiding (module Eq)
+  open IsTotalOrder isTotalOrder public hiding (module Eq)
 
   module Eq where
 
     isDecEquivalence : IsDecEquivalence _≈_
     isDecEquivalence = record
-      { isEquivalence = TO.isEquivalence
+      { isEquivalence = isEquivalence
       ; _≟_           = _≟_
       }
 
@@ -349,7 +351,10 @@ record DecTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
 ------------------------------------------------------------------------
 -- Strict total orders
 
--- Note that these orders are decidable (see compare).
+-- 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.
 
 record IsStrictTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
                           (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂) :
@@ -375,8 +380,14 @@ record IsStrictTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
 
   module Eq = IsDecEquivalence isDecEquivalence
 
+  <-respˡ-≈ : _<_ Respectsˡ _≈_
+  <-respˡ-≈ = trans∧tri⟶respˡ≈ Eq.trans trans compare
+
+  <-respʳ-≈ : _<_ Respectsʳ _≈_
+  <-respʳ-≈ = trans∧tri⟶respʳ≈ Eq.sym Eq.trans trans compare
+
   <-resp-≈ : _<_ Respects₂ _≈_
-  <-resp-≈ = trans∧tri⟶resp≈ Eq.sym Eq.trans trans compare
+  <-resp-≈ = <-respʳ-≈ , <-respˡ-≈
 
   isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
   isStrictPartialOrder = record
@@ -386,7 +397,8 @@ record IsStrictTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
     ; <-resp-≈      = <-resp-≈
     }
 
-  open IsStrictPartialOrder isStrictPartialOrder public using (irrefl)
+  open IsStrictPartialOrder isStrictPartialOrder public
+    using (irrefl; asym)
 
 record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix 4 _≈_ _<_