De-symmetrising Relation.Binary.Bundles.Preorder._∼_ (#2099)

Author: jamesmckinna

CHANGELOG.md

@@ -797,6 +797,23 @@ Non-backwards compatible changes
   IO.Instances
   ```
 
+### (Issue #2096) Introduction of flipped relation symbol for `Relation.Binary.Bundles.Preorder`
+
+* Previously, the relation symbol `_∼_`  was (notationally) symmetric, so that its
+  converse relation could only be discussed *semantically* in terms of `flip _∼_`
+  in `Relation.Binary.Properties.Preorder`, `Relation.Binary.Construct.Flip.{Ord|EqAndOrd}`
+
+* Now, the symbol `_∼_` has been renamed to a new symbol `_≲_`, with `_≳_`
+  introduced as a definition in `Relation.Binary.Bundles.Preorder` whose properties
+  in `Relation.Binary.Properties.Preorder` now refer to it. Partial backwards compatible
+  has been achieved by redeclaring a deprecated version of the old name in the record.
+  Therefore, only _declarations_ of `PartialOrder` records will need their field names
+  updating.
+
+* NB (issues #1214 #2098) the corresponding situation regarding the `flip`ped
+  relation symbols `_≥_`, `_>_` (and their negated versions!) has not (yet)
+  been addressed.
+
 ### Standardisation of `insertAt`/`updateAt`/`removeAt`
 
 * Previously, the names and argument order of index-based insertion, update and removal functions for
@@ -840,7 +857,6 @@ Non-backwards compatible changes
 
 * The old names (and the names of all proofs about these functions) have been deprecated appropriately.
 
-
 ### Changes to triple reasoning interface
 
 * The module `Relation.Binary.Reasoning.Base.Triple` now takes an extra proof that the strict
@@ -1251,6 +1267,11 @@ Deprecated names
   push-function-into-if ↦ if-float
   ```
 
+* In `Data.Container.Related`:
+  ```
+  _∼[_]_  ↦  _≲[_]_
+  ```
+
 * In `Data.Fin.Base`: two new, hopefully more memorable, names `↑ˡ` `↑ʳ`
   for the 'left', resp. 'right' injection of a Fin m into a 'larger' type,
   `Fin (m + n)`, resp. `Fin (n + m)`, with argument order to reflect the
@@ -1661,6 +1682,16 @@ Deprecated names
   fromForeign ↦ Foreign.Haskell.Coerce.coerce
   ```
 
+* In `Relation.Binary.Bundles.Preorder`:
+  ```
+  _∼_  ↦  _≲_
+  ```
+
+* In `Relation.Binary.Indexed.Heterogeneous.Bundles.Preorder`:
+  ```
+  _∼_  ↦  _≲_
+  ```
+
 * In `Relation.Binary.Properties.Preorder`:
   ```
   invIsPreorder ↦ converse-isPreorder

src/Data/Container/Related.agda

@@ -33,7 +33,23 @@ open Related public
                Setoid (s ⊔ p ⊔ ℓ) (p ⊔ ℓ)
 [ k ]-Equality C X = Related.InducedEquivalence₂ k (_∈_ {C = C} {X = X})
 
-infix 4 _∼[_]_
-_∼[_]_ : ∀ {s p x} {C : Container s p} {X : Set x} →
+infix 4 _≲[_]_
+_≲[_]_ : ∀ {s p x} {C : Container s p} {X : Set x} →
          ⟦ C ⟧ X → Kind → ⟦ C ⟧ X → Set (p ⊔ x)
-_∼[_]_ {C = C} {X} xs k ys = Preorder._∼_ ([ k ]-Order C X) xs ys
+_≲[_]_ {C = C} {X} xs k ys = Preorder._≲_ ([ k ]-Order C X) xs ys
+
+
+
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+infix 4 _∼[_]_
+_∼[_]_ = _≲[_]_
+{-# WARNING_ON_USAGE _∼[_]_
+"Warning: _∼[_]_ was deprecated in v2.0. Please use _≲[_]_ instead. "
+#-}

src/Data/Container/Relation/Unary/Any/Properties.agda

@@ -64,7 +64,7 @@ module _ {s p} {C : Container s p} {x} {X : Set x}
 -- ◇ is a congruence for bag and set equality and related preorders.
 
   cong : ∀ {k} {xs₁ xs₂ : ⟦ C ⟧ X} →
-         (∀ x → Related k (P₁ x) (P₂ x)) → xs₁ ∼[ k ] xs₂ →
+         (∀ x → Related k (P₁ x) (P₂ x)) → xs₁ ≲[ k ] xs₂ →
          Related k (◇ C P₁ xs₁) (◇ C P₂ xs₂)
   cong {k} {xs₁} {xs₂} P₁↔P₂ xs₁≈xs₂ =
     ◇ C P₁ xs₁               ↔⟨ ↔∈ C ⟩
@@ -185,8 +185,8 @@ module _ {s p} (C : Container s p) {x y} {X : Set x} {Y : Set y}
          {ℓ} (P : Pred Y ℓ) where
 
   map-cong : ∀ {k} {f₁ f₂ : X → Y} {xs₁ xs₂ : ⟦ C ⟧ X} →
-             f₁ ≗ f₂ → xs₁ ∼[ k ] xs₂ →
-             map f₁ xs₁ ∼[ k ] map f₂ xs₂
+             f₁ ≗ f₂ → xs₁ ≲[ k ] xs₂ →
+             map f₁ xs₁ ≲[ k ] map f₂ xs₂
   map-cong {f₁ = f₁} {f₂} {xs₁} {xs₂} f₁≗f₂ xs₁≈xs₂ {x} =
     x ∈ map f₁ xs₁           ↔⟨ map↔∘ C (_≡_ x) f₁ ⟩
     ◇ C (λ y → x ≡ f₁ y) xs₁ ∼⟨ cong (Related.↔⇒ ∘ helper) xs₁≈xs₂ ⟩
@@ -286,7 +286,7 @@ module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s
 
 module _ {s p} {C : Container s p} {x} {X : Set x} where
 
-  linear-identity : ∀ {xs : ⟦ C ⟧ X} (m : C ⊸ C) → ⟪ m ⟫⊸ xs ∼[ bag ] xs
+  linear-identity : ∀ {xs : ⟦ C ⟧ X} (m : C ⊸ C) → ⟪ m ⟫⊸ xs ≲[ bag ] xs
   linear-identity {xs} m {x} =
     x ∈ ⟪ m ⟫⊸ xs  ↔⟨ remove-linear (_≡_ x) m ⟩
     x ∈        xs  ∎

src/Data/List/Relation/Binary/BagAndSetEquality.agda

@@ -72,8 +72,8 @@ open Related public using (Kind; SymmetricKind) renaming
 
 infix 4 _∼[_]_
 
-_∼[_]_ : List A → Kind → List A → Set _
-_∼[_]_ {A = A} xs k ys = Preorder._∼_ ([ k ]-Order A) xs ys
+_∼[_]_ : ∀ {a} {A : Set a} → List A → Kind → List A → Set _
+_∼[_]_ {A = A} xs k ys = Preorder._≲_ ([ k ]-Order A) xs ys
 
 private
   module Eq  {k a} {A : Set a} = Setoid ([ k ]-Equality A)

src/Effect/Monad/Partiality.agda

@@ -301,7 +301,7 @@ module _ {A : Set a} {_∼_ : A → A → Set ℓ} where
   preorder pre k = record
     { Carrier    = A ⊥
     ; _≈_        = _≡_
-    ; _∼_        = Rel k
+    ; _≲_        = Rel k
     ; isPreorder = record
       { isEquivalence = P.isEquivalence
       ; reflexive     = refl′

src/Function/Related.agda

@@ -404,7 +404,7 @@ InducedPreorder₁ : Kind → ∀ {a s} {A : Set a} →
                    (A → Set s) → Preorder _ _ _
 InducedPreorder₁ k S = record
   { _≈_        = _≡_
-  ; _∼_        = InducedRelation₁ k S
+  ; _≲_        = InducedRelation₁ k S
   ; isPreorder = record
     { isEquivalence = P.isEquivalence
     ; reflexive     = reflexive ∘
@@ -437,7 +437,7 @@ InducedPreorder₂ : Kind → ∀ {a b s} {A : Set a} {B : Set b} →
                    (A → B → Set s) → Preorder _ _ _
 InducedPreorder₂ k _S_ = record
   { _≈_        = _≡_
-  ; _∼_        = InducedRelation₂ k _S_
+  ; _≲_        = InducedRelation₂ k _S_
   ; isPreorder = record
     { isEquivalence = P.isEquivalence
     ; reflexive     = λ x≡y {z} →

src/Function/Related/Propositional.agda

@@ -339,7 +339,7 @@ InducedRelation₁ k P = λ x y → P x ∼[ k ] P y
 InducedPreorder₁ : Kind → (P : A → Set p) → Preorder _ _ _
 InducedPreorder₁ k P = record
   { _≈_        = _≡_
-  ; _∼_        = InducedRelation₁ k P
+  ; _≲_        = InducedRelation₁ k P
   ; isPreorder = record
     { isEquivalence = P.isEquivalence
     ; reflexive     = reflexive ∘
@@ -369,7 +369,7 @@ InducedRelation₂ k _S_ = λ x y → ∀ {z} → (z S x) ∼[ k ] (z S y)
 InducedPreorder₂ : Kind → ∀ {s} → (A → B → Set s) → Preorder _ _ _
 InducedPreorder₂ k _S_ = record
   { _≈_        = _≡_
-  ; _∼_        = InducedRelation₂ k _S_
+  ; _≲_        = InducedRelation₂ k _S_
   ; isPreorder = record
     { isEquivalence = P.isEquivalence
     ; reflexive     = λ x≡y {z} →

src/Relation/Binary/Bundles.agda

@@ -10,6 +10,7 @@
 
 module Relation.Binary.Bundles where
 
+open import Function.Base using (flip)
 open import Level
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Binary.Core
@@ -73,12 +74,12 @@ record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where
 ------------------------------------------------------------------------
 
 record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
-  infix 4 _≈_ _∼_
+  infix 4 _≈_ _≲_
   field
     Carrier    : Set c
     _≈_        : Rel Carrier ℓ₁  -- The underlying equality.
-    _∼_        : Rel Carrier ℓ₂  -- The relation.
-    isPreorder : IsPreorder _≈_ _∼_
+    _≲_        : Rel Carrier ℓ₂  -- The relation.
+    isPreorder : IsPreorder _≈_ _≲_
 
   open IsPreorder isPreorder public
     hiding (module Eq)
@@ -91,6 +92,12 @@ record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
 
     open Setoid setoid public
 
+  infix 4 _≳_
+  _≳_ = flip _≲_
+
+  infix 4 _∼_ -- for deprecation
+  _∼_ = _≲_
+
 
 record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix 4 _≈_ _≲_
@@ -107,7 +114,7 @@ record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   preorder = record { isPreorder = isPreorder }
 
   open Preorder preorder public
-    using (module Eq)
+    using (module Eq; _≳_)
 
 
 ------------------------------------------------------------------------
@@ -331,3 +338,18 @@ record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) w
     isApartnessRelation : IsApartnessRelation _≈_ _#_
 
   open IsApartnessRelation isApartnessRelation public
+
+
+
+
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+{-# WARNING_ON_USAGE Preorder._∼_
+"Warning: Preorder._∼_ was deprecated in v2.0. Please use Preorder._≲_ instead. "
+#-}

src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda

@@ -104,7 +104,7 @@ module _ {i t} {I : Set i} (T : Rel I t) where
   preorder : Preorder _ _ _
   preorder = record
     { _≈_        = _≡_
-    ; _∼_        = Star T
+    ; _≲_        = Star T
     ; isPreorder = isPreorder
     }
 

src/Relation/Binary/HeterogeneousEquality.agda

@@ -219,7 +219,7 @@ preorder : Set ℓ → Preorder ℓ ℓ ℓ
 preorder A = record
   { Carrier    = A
   ; _≈_        = _≡_
-  ; _∼_        = λ x y → x ≅ y
+  ; _≲_        = λ x y → x ≅ y
   ; isPreorder = isPreorder-≡
   }
 

src/Relation/Binary/Indexed/Heterogeneous/Bundles.agda

@@ -33,11 +33,28 @@ record IndexedSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
 
 record IndexedPreorder {i} (I : Set i) c ℓ₁ ℓ₂ :
                        Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where
-  infix 4 _≈_ _∼_
+  infix 4 _≈_ _≲_
   field
     Carrier    : I → Set c
     _≈_        : IRel Carrier ℓ₁  -- The underlying equality.
-    _∼_        : IRel Carrier ℓ₂  -- The relation.
-    isPreorder : IsIndexedPreorder Carrier _≈_ _∼_
+    _≲_        : IRel Carrier ℓ₂  -- The relation.
+    isPreorder : IsIndexedPreorder Carrier _≈_ _≲_
 
   open IsIndexedPreorder isPreorder public
+
+  infix 4 _∼_
+  _∼_ = _≲_
+
+
+
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+{-# WARNING_ON_USAGE IndexedPreorder._∼_
+"Warning: IndexedPreorder._∼_ was deprecated in v2.0. Please use IndexedPreorder._≲_ instead. "
+#-}

src/Relation/Binary/Indexed/Heterogeneous/Construct/At.agda

@@ -27,9 +27,9 @@ module _ {a i} {I : Set i} {A : I → Set a} where
     }
     where open IsIndexedEquivalence isEq
 
-  isPreorder : ∀ {ℓ₁ ℓ₂} {_≈_ : IRel A ℓ₁} {_∼_ : IRel A ℓ₂} →
-               IsIndexedPreorder A _≈_ _∼_ →
-               (index : I) → IsPreorder (_≈_ {index}) _∼_
+  isPreorder : ∀ {ℓ₁ ℓ₂} {_≈_ : IRel A ℓ₁} {_≲_ : IRel A ℓ₂} →
+               IsIndexedPreorder A _≈_ _≲_ →
+               (index : I) → IsPreorder (_≈_ {index}) _≲_
   isPreorder isPreorder index = record
     { isEquivalence = isEquivalence O.isEquivalence index
     ; reflexive     = O.reflexive
@@ -54,7 +54,7 @@ module _ {a i} {I : Set i} where
   preorder O index = record
     { Carrier    = O.Carrier index
     ; _≈_        = O._≈_
-    ; _∼_        = O._∼_
+    ; _≲_        = O._≲_
     ; isPreorder = isPreorder O.isPreorder index
     }
     where module O = IndexedPreorder O

src/Relation/Binary/Indexed/Heterogeneous/Structures.agda

@@ -34,13 +34,13 @@ record IsIndexedEquivalence : Set (i ⊔ a ⊔ ℓ) where
   reflexive P.refl = refl
 
 
-record IsIndexedPreorder {ℓ₂} (_∼_ : IRel A ℓ₂) : Set (i ⊔ a ⊔ ℓ ⊔ ℓ₂) where
+record IsIndexedPreorder {ℓ₂} (_≲_ : IRel A ℓ₂) : Set (i ⊔ a ⊔ ℓ ⊔ ℓ₂) where
   field
     isEquivalence : IsIndexedEquivalence
-    reflexive     : ∀ {i j} → (_≈_ {i} {j}) ⟨ _⇒_ ⟩ _∼_
-    trans         : Transitive A _∼_
+    reflexive     : ∀ {i j} → (_≈_ {i} {j}) ⟨ _⇒_ ⟩ _≲_
+    trans         : Transitive A _≲_
 
   module Eq = IsIndexedEquivalence isEquivalence
 
-  refl : Reflexive A _∼_
+  refl : Reflexive A _≲_
   refl = reflexive Eq.refl

src/Relation/Binary/Morphism/Bundles.agda

@@ -70,7 +70,7 @@ record PreorderHomomorphism (S₁ : Preorder ℓ₁ ℓ₂ ℓ₃)
   open Preorder
   field
     ⟦_⟧                 : Carrier S₁ → Carrier S₂
-    isOrderHomomorphism : IsOrderHomomorphism (_≈_ S₁) (_≈_ S₂) (_∼_ S₁) (_∼_ S₂) ⟦_⟧
+    isOrderHomomorphism : IsOrderHomomorphism (_≈_ S₁) (_≈_ S₂) (_≲_ S₁) (_≲_ S₂) ⟦_⟧
 
   open IsOrderHomomorphism isOrderHomomorphism public