From 64eddf06bc6de9248dbf28f758a3faf05f8a44b7 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 2 Oct 2024 10:28:25 +0100
Subject: [PATCH 1/6] add `Raw` bundles for binary relation hierarchy

---
 CHANGELOG.md                         |   5 ++
 src/Relation/Binary/Bundles/Raw.agda | 118 +++++++++++++++++++++++++++
 2 files changed, 123 insertions(+)
 create mode 100644 src/Relation/Binary/Bundles/Raw.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 57c92734ca..14346f3c0a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -110,6 +110,11 @@ New modules
 
 * `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`
 
+* Raw bundles for the `Relation.Binary.Bundles` hierarchy:
+  ```agda
+  Relation.Binary.Bundles.Raw
+  ```
+
 Additions to existing modules
 -----------------------------
 
diff --git a/src/Relation/Binary/Bundles/Raw.agda b/src/Relation/Binary/Bundles/Raw.agda
new file mode 100644
index 0000000000..fd324a6383
--- /dev/null
+++ b/src/Relation/Binary/Bundles/Raw.agda
@@ -0,0 +1,118 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Raw bundles for homogeneous binary relations
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via `Relation.Binary`.
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Bundles.Raw where
+
+open import Function.Base using (flip)
+open import Level using (Level; suc; _⊔_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Nullary.Negation.Core using (¬_)
+
+
+------------------------------------------------------------------------
+-- RawSetoid
+------------------------------------------------------------------------
+
+record RawSetoid a ℓ : Set (suc (a ⊔ ℓ)) where
+  infix 4 _≈_
+  field
+    Carrier              : Set a
+    _≈_                  : Rel Carrier ℓ
+
+  infix 4 _≉_
+  _≉_ : Rel Carrier _
+  x ≉ y = ¬ (x ≈ y)
+
+
+------------------------------------------------------------------------
+-- RawPreorder
+------------------------------------------------------------------------
+
+record RawPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _≲_
+  field
+    Carrier    : Set c
+    _≈_        : Rel Carrier ℓ₁  -- The underlying equality.
+    _≲_        : Rel Carrier ℓ₂  -- The relation.
+
+  rawSetoid : RawSetoid c ℓ₁
+  rawSetoid = record { _≈_ = _≈_ }
+
+  open RawSetoid rawSetoid public
+    using (_≉_)
+
+  infix 4 _⋦_
+  _⋦_ : Rel Carrier _
+  x ⋦ y = ¬ (x ≲ y)
+
+  infix 4 _≳_
+  _≳_ = flip _≲_
+
+  infix 4 _⋧_
+  _⋧_ = flip _⋦_
+
+
+------------------------------------------------------------------------
+-- RawPartialOrders
+------------------------------------------------------------------------
+
+record RawPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _≤_
+  field
+    Carrier        : Set c
+    _≈_            : Rel Carrier ℓ₁
+    _≤_            : Rel Carrier ℓ₂
+
+  rawPreorder : RawPreorder c ℓ₁ ℓ₂
+  rawPreorder = record { _≈_ = _≈_ ; _≲_ = _≤_ }
+
+  open RawPreorder rawPreorder public
+    hiding (Carrier; _≈_; _≲_)
+    renaming (_⋦_ to _≰_; _≳_ to _≥_; _⋧_ to _≱_)
+
+
+record RawStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _<_
+  field
+    Carrier              : Set c
+    _≈_                  : Rel Carrier ℓ₁
+    _<_                  : Rel Carrier ℓ₂
+
+  rawSetoid : RawSetoid c ℓ₁
+  rawSetoid = record { _≈_ = _≈_ }
+
+  open RawSetoid rawSetoid public
+    using (_≉_)
+
+  infix 4 _≮_
+  _≮_ : Rel Carrier _
+  x ≮ y = ¬ (x < y)
+
+  infix 4 _>_
+  _>_ = flip _<_
+
+  infix 4 _≯_
+  _≯_ = flip _≮_
+
+
+------------------------------------------------------------------------
+-- RawApartnessRelation
+------------------------------------------------------------------------
+
+record RawApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _#_
+  field
+    Carrier             : Set c
+    _≈_                 : Rel Carrier ℓ₁
+    _#_                 : Rel Carrier ℓ₂
+
+  infix 4 _¬#_
+  _¬#_ : Rel Carrier _
+  x ¬# y = ¬ (x # y)

From 39235983bfc3c40d32fbd124ecbbf02e2e64d4b2 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 2 Oct 2024 12:05:22 +0100
Subject: [PATCH 2/6] added `rawX` manifest fields to each `X` bundle

---
 src/Relation/Binary/Bundles.agda | 50 ++++++++++++++++++--------------
 1 file changed, 28 insertions(+), 22 deletions(-)

diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda
index 5d29cabe57..25197537af 100644
--- a/src/Relation/Binary/Bundles.agda
+++ b/src/Relation/Binary/Bundles.agda
@@ -14,6 +14,7 @@ open import Function.Base using (flip)
 open import Level using (Level; suc; _⊔_)
 open import Relation.Nullary.Negation.Core using (¬_)
 open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles.Raw
 open import Relation.Binary.Structures -- most of it
 
 ------------------------------------------------------------------------
@@ -29,9 +30,11 @@ record PartialSetoid a ℓ : Set (suc (a ⊔ ℓ)) where
 
   open IsPartialEquivalence isPartialEquivalence public
 
-  infix 4 _≉_
-  _≉_ : Rel Carrier _
-  x ≉ y = ¬ (x ≈ y)
+  rawSetoid : RawSetoid _ _
+  rawSetoid = record { _≈_ = _≈_ }
+
+  open RawSetoid rawSetoid public
+    hiding (Carrier; _≈_ )
 
 
 record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
@@ -94,15 +97,11 @@ record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
 
     open Setoid setoid public
 
-  infix 4 _⋦_
-  _⋦_ : Rel Carrier _
-  x ⋦ y = ¬ (x ≲ y)
-
-  infix 4 _≳_
-  _≳_ = flip _≲_
+  rawPreorder : RawPreorder _ _ _
+  rawPreorder = record { _≈_ = _≈_ ; _≲_ = _≲_ }
 
-  infix 4 _⋧_
-  _⋧_ = flip _⋦_
+  open RawPreorder rawPreorder public
+    hiding (Carrier; _≈_ ; _≲_)
 
   -- Deprecated.
   infix 4 _∼_
@@ -153,14 +152,17 @@ record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     }
 
   open Preorder preorder public
-    hiding (Carrier; _≈_; _≲_; isPreorder)
+    hiding (Carrier; _≈_; _≲_; isPreorder; _⋦_; _≳_; _⋧_)
     renaming
-    ( _⋦_ to _≰_; _≳_ to _≥_; _⋧_ to _≱_
-    ; ≲-respˡ-≈ to ≤-respˡ-≈
+    ( ≲-respˡ-≈ to ≤-respˡ-≈
     ; ≲-respʳ-≈ to ≤-respʳ-≈
     ; ≲-resp-≈  to ≤-resp-≈
     )
 
+  open RawPreorder rawPreorder public
+    renaming ( _⋦_ to _≰_; _≳_ to _≥_; _⋧_ to _≱_)
+    hiding (Carrier; _≈_ ; _≲_; _≉_; rawSetoid)
+
 
 record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix 4 _≈_ _≤_
@@ -211,15 +213,11 @@ record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂))
 
     open Setoid setoid public
 
-  infix 4 _≮_
-  _≮_ : Rel Carrier _
-  x ≮ y = ¬ (x < y)
+  rawStrictPartialOrder : RawStrictPartialOrder _ _ _
+  rawStrictPartialOrder = record { _≈_ = _≈_ ; _<_ = _<_ }
 
-  infix 4 _>_
-  _>_ = flip _<_
-
-  infix 4 _≯_
-  _≯_ = flip _≮_
+  open RawStrictPartialOrder rawStrictPartialOrder public
+    hiding (Carrier; _≈_ ; _<_)
 
 
 record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
@@ -390,3 +388,11 @@ record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) w
     isApartnessRelation : IsApartnessRelation _≈_ _#_
 
   open IsApartnessRelation isApartnessRelation public
+    hiding (_¬#_)
+
+  rawApartnessRelation : RawApartnessRelation _ _ _
+  rawApartnessRelation = record { _≈_ = _≈_ ; _#_ = _#_ }
+
+  open RawApartnessRelation rawApartnessRelation public
+    hiding (Carrier; _≈_ ; _#_)
+  

From deaf59ea976c974614b38daf05733eb5873db994 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 2 Oct 2024 12:16:09 +0100
Subject: [PATCH 3/6] fixed knock-on ambiguity bugs

---
 src/Relation/Binary/Bundles.agda          | 2 +-
 src/Relation/Binary/Properties/Poset.agda | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda
index 25197537af..b03a6bc58c 100644
--- a/src/Relation/Binary/Bundles.agda
+++ b/src/Relation/Binary/Bundles.agda
@@ -395,4 +395,4 @@ record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) w
 
   open RawApartnessRelation rawApartnessRelation public
     hiding (Carrier; _≈_ ; _#_)
-  
+
diff --git a/src/Relation/Binary/Properties/Poset.agda b/src/Relation/Binary/Properties/Poset.agda
index d25f3af79a..712881de7d 100644
--- a/src/Relation/Binary/Properties/Poset.agda
+++ b/src/Relation/Binary/Properties/Poset.agda
@@ -25,7 +25,7 @@ open Poset P renaming (Carrier to A)
 
 import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict
 import Relation.Binary.Properties.Preorder preorder as PreorderProperties
-open Eq using (_≉_)
+
 
 ------------------------------------------------------------------------
 -- The _≥_ relation is also a poset.

From da2dd6a13df9e6b3c147bca2c3a79a9b7930bc74 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 2 Oct 2024 12:27:24 +0100
Subject: [PATCH 4/6] fixed knock-on ambiguity bugs

---
 CHANGELOG.md                                                   | 1 +
 src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda   | 2 +-
 src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda | 2 +-
 3 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 14346f3c0a..fbbb337894 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -114,6 +114,7 @@ New modules
   ```agda
   Relation.Binary.Bundles.Raw
   ```
+  plus adding `rawX` fields to each of `Relation.Binary.Bundles.X`.
 
 Additions to existing modules
 -----------------------------
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
index 49da62b10b..8b3ba8b55e 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -29,7 +29,7 @@ open import Relation.Unary using (Pred; _∩_)
 
 open import Data.Tree.AVL.Indexed sto as AVL
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
-open StrictTotalOrder sto renaming (Carrier to Key; trans to <-trans); open Eq using (_≉_; sym; trans)
+open StrictTotalOrder sto renaming (Carrier to Key; trans to <-trans); open Eq using (sym; trans)
 
 open import Relation.Binary.Construct.Add.Extrema.Strict _<_ using ([<]-injective)
 
diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
index fefb27764f..2368c44bcd 100644
--- a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
+++ b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
@@ -30,7 +30,7 @@ open import Relation.Nullary using (Reflects; ¬_; yes; no)
 open import Relation.Nullary.Negation using (contradiction)
 
 open StrictTotalOrder strictTotalOrder renaming (Carrier to Key) hiding (trans)
-open Eq using (_≉_; refl; sym; trans)
+open Eq using (refl; sym; trans)
 open import Data.Tree.AVL strictTotalOrder using (tree)
 open import Data.Tree.AVL.Indexed strictTotalOrder using (key)
 import Data.Tree.AVL.Indexed.Relation.Unary.Any strictTotalOrder as IAny

From c44977a98415265167326fa9f60557aea2272683 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 2 Oct 2024 13:39:38 +0100
Subject: [PATCH 5/6] tighten `import`s

---
 .../AVL/Map/Membership/Propositional.agda     | 36 ++++++-------------
 1 file changed, 11 insertions(+), 25 deletions(-)

diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional.agda b/src/Data/Tree/AVL/Map/Membership/Propositional.agda
index 7f5151600f..c040f63a0e 100644
--- a/src/Data/Tree/AVL/Map/Membership/Propositional.agda
+++ b/src/Data/Tree/AVL/Map/Membership/Propositional.agda
@@ -13,40 +13,26 @@ module Data.Tree.AVL.Map.Membership.Propositional
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
   where
 
-open import Data.Bool.Base using (true; false)
-open import Data.Maybe.Base using (just; nothing; is-just)
-open import Data.Product.Base using (_×_; ∃-syntax; _,_; proj₁; proj₂)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent renaming (Pointwise to _×ᴿ_)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-open import Function.Base using (_∘_; _∘′_)
+open import Data.Product.Base using (_×_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent
+  using ()
+  renaming (Pointwise to _×ᴿ_)
 open import Level using (Level)
 
-open import Relation.Binary.Definitions using (Transitive; Symmetric; _Respectsˡ_)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Construct.Intersection using (_∩_)
-open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; cong) renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans)
-open import Relation.Nullary using (Reflects; ¬_; yes; no)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Nullary.Negation.Core using (¬_)
+
+open StrictTotalOrder strictTotalOrder using (_≈_) renaming (Carrier to Key)
+open import Data.Tree.AVL.Map strictTotalOrder using (Map)
+open import Data.Tree.AVL.Map.Relation.Unary.Any strictTotalOrder using (Any)
 
-open StrictTotalOrder strictTotalOrder renaming (Carrier to Key) hiding (trans)
-open Eq using (_≉_; refl; sym; trans)
-open import Data.Tree.AVL strictTotalOrder using (tree)
-open import Data.Tree.AVL.Indexed strictTotalOrder using (key)
-import Data.Tree.AVL.Indexed.Relation.Unary.Any strictTotalOrder as IAny
-import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties strictTotalOrder as IAnyₚ
-open import Data.Tree.AVL.Key strictTotalOrder using (⊥⁺<[_]<⊤⁺)
-open import Data.Tree.AVL.Map strictTotalOrder
-open import Data.Tree.AVL.Map.Relation.Unary.Any strictTotalOrder as Mapₚ using (Any)
-open import Data.Tree.AVL.Relation.Unary.Any strictTotalOrder as Any using (tree)
 
 private
   variable
-    v p q : Level
+    v : Level
     V : Set v
     m : Map V
-    k k′ : Key
-    x x′ y y′ : V
     kx : Key × V
 
 infix 4 _≈ₖᵥ_

From d9a6a5009e461528fe7a645afeb9a3f90a6f9d60 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 7 Oct 2024 18:33:37 +0100
Subject: [PATCH 6/6] response to review feedback: refactor in favou rof a
 single underlying `RawRelation`

---
 src/Relation/Binary/Bundles.agda     | 36 ++++++-------
 src/Relation/Binary/Bundles/Raw.agda | 80 ++++------------------------
 2 files changed, 29 insertions(+), 87 deletions(-)

diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda
index b03a6bc58c..297ef96f08 100644
--- a/src/Relation/Binary/Bundles.agda
+++ b/src/Relation/Binary/Bundles.agda
@@ -97,15 +97,13 @@ record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
 
     open Setoid setoid public
 
-  rawPreorder : RawPreorder _ _ _
-  rawPreorder = record { _≈_ = _≈_ ; _≲_ = _≲_ }
-
-  open RawPreorder rawPreorder public
-    hiding (Carrier; _≈_ ; _≲_)
+  rawRelation : RawRelation _ _ _
+  rawRelation = record { _≈_ = _≈_ ; _∼_ = _≲_ }
 
+  open RawRelation rawRelation public
+    renaming (_≁_ to _⋦_; _∼ᵒ_ to _≳_; _≁ᵒ_ to _⋧_)
+    hiding (Carrier; _≈_)
   -- Deprecated.
-  infix 4 _∼_
-  _∼_ = _≲_
   {-# WARNING_ON_USAGE _∼_
   "Warning: _∼_ was deprecated in v2.0.
   Please use _≲_ instead. "
@@ -159,9 +157,9 @@ record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     ; ≲-resp-≈  to ≤-resp-≈
     )
 
-  open RawPreorder rawPreorder public
-    renaming ( _⋦_ to _≰_; _≳_ to _≥_; _⋧_ to _≱_)
-    hiding (Carrier; _≈_ ; _≲_; _≉_; rawSetoid)
+  open RawRelation rawRelation public
+    renaming (_≁_ to _≰_; _∼ᵒ_ to _≥_; _≁ᵒ_ to _≱_)
+    hiding (Carrier; _≈_ ; _∼_; _≉_; rawSetoid)
 
 
 record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
@@ -213,11 +211,12 @@ record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂))
 
     open Setoid setoid public
 
-  rawStrictPartialOrder : RawStrictPartialOrder _ _ _
-  rawStrictPartialOrder = record { _≈_ = _≈_ ; _<_ = _<_ }
+  rawRelation : RawRelation _ _ _
+  rawRelation = record { _≈_ = _≈_ ; _∼_ = _<_ }
 
-  open RawStrictPartialOrder rawStrictPartialOrder public
-    hiding (Carrier; _≈_ ; _<_)
+  open RawRelation rawRelation public
+    renaming (_≁_ to _≮_; _∼ᵒ_ to _>_; _≁ᵒ_ to _≯_)
+    hiding (Carrier; _≈_ ; _∼_)
 
 
 record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
@@ -390,9 +389,10 @@ record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) w
   open IsApartnessRelation isApartnessRelation public
     hiding (_¬#_)
 
-  rawApartnessRelation : RawApartnessRelation _ _ _
-  rawApartnessRelation = record { _≈_ = _≈_ ; _#_ = _#_ }
+  rawRelation : RawRelation _ _ _
+  rawRelation = record { _≈_ = _≈_ ; _∼_ = _#_ }
 
-  open RawApartnessRelation rawApartnessRelation public
-    hiding (Carrier; _≈_ ; _#_)
+  open RawRelation rawRelation public
+    renaming (_≁_ to _¬#_; _∼ᵒ_ to _#ᵒ_; _≁ᵒ_ to _¬#ᵒ_)
+    hiding (Carrier; _≈_ ; _∼_)
 
diff --git a/src/Relation/Binary/Bundles/Raw.agda b/src/Relation/Binary/Bundles/Raw.agda
index fd324a6383..778054acc8 100644
--- a/src/Relation/Binary/Bundles/Raw.agda
+++ b/src/Relation/Binary/Bundles/Raw.agda
@@ -32,15 +32,15 @@ record RawSetoid a ℓ : Set (suc (a ⊔ ℓ)) where
 
 
 ------------------------------------------------------------------------
--- RawPreorder
+-- RawRelation: basis for Relation.Binary.Bundles.*Order
 ------------------------------------------------------------------------
 
-record RawPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
-  infix 4 _≈_ _≲_
+record RawRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _∼_
   field
     Carrier    : Set c
     _≈_        : Rel Carrier ℓ₁  -- The underlying equality.
-    _≲_        : Rel Carrier ℓ₂  -- The relation.
+    _∼_        : Rel Carrier ℓ₂  -- The underlying relation.
 
   rawSetoid : RawSetoid c ℓ₁
   rawSetoid = record { _≈_ = _≈_ }
@@ -48,71 +48,13 @@ record RawPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   open RawSetoid rawSetoid public
     using (_≉_)
 
-  infix 4 _⋦_
-  _⋦_ : Rel Carrier _
-  x ⋦ y = ¬ (x ≲ y)
+  infix 4 _≁_
+  _≁_ : Rel Carrier _
+  x ≁ y = ¬ (x ∼ y)
 
-  infix 4 _≳_
-  _≳_ = flip _≲_
+  infix 4 _∼ᵒ_
+  _∼ᵒ_ = flip _∼_
 
-  infix 4 _⋧_
-  _⋧_ = flip _⋦_
+  infix 4 _≁ᵒ_
+  _≁ᵒ_ = flip _≁_
 
-
-------------------------------------------------------------------------
--- RawPartialOrders
-------------------------------------------------------------------------
-
-record RawPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
-  infix 4 _≈_ _≤_
-  field
-    Carrier        : Set c
-    _≈_            : Rel Carrier ℓ₁
-    _≤_            : Rel Carrier ℓ₂
-
-  rawPreorder : RawPreorder c ℓ₁ ℓ₂
-  rawPreorder = record { _≈_ = _≈_ ; _≲_ = _≤_ }
-
-  open RawPreorder rawPreorder public
-    hiding (Carrier; _≈_; _≲_)
-    renaming (_⋦_ to _≰_; _≳_ to _≥_; _⋧_ to _≱_)
-
-
-record RawStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
-  infix 4 _≈_ _<_
-  field
-    Carrier              : Set c
-    _≈_                  : Rel Carrier ℓ₁
-    _<_                  : Rel Carrier ℓ₂
-
-  rawSetoid : RawSetoid c ℓ₁
-  rawSetoid = record { _≈_ = _≈_ }
-
-  open RawSetoid rawSetoid public
-    using (_≉_)
-
-  infix 4 _≮_
-  _≮_ : Rel Carrier _
-  x ≮ y = ¬ (x < y)
-
-  infix 4 _>_
-  _>_ = flip _<_
-
-  infix 4 _≯_
-  _≯_ = flip _≮_
-
-
-------------------------------------------------------------------------
--- RawApartnessRelation
-------------------------------------------------------------------------
-
-record RawApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
-  infix 4 _≈_ _#_
-  field
-    Carrier             : Set c
-    _≈_                 : Rel Carrier ℓ₁
-    _#_                 : Rel Carrier ℓ₂
-
-  infix 4 _¬#_
-  _¬#_ : Rel Carrier _
-  x ¬# y = ¬ (x # y)