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] 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; _≈_ ; _#_)
+