Rename Relation.Binary.Construct.(Flip/Converse)

CHANGELOG.md

@@ -889,6 +889,14 @@ Major improvements
 Deprecated modules
 ------------------
 
+### Moving `Relation.Binary.Construct.(Converse/Flip)`
+
+* The following files have been moved:
+  ```agda
+  Relation.Binary.Construct.Converse               ↦ Relation.Binary.Construct.Flip.EqAndOrd
+  Relation.Binary.Construct.Flip                   ↦ Relation.Binary.Construct.Flip.Ord
+  ```
+
 ### Deprecation of old function hierarchy
 
 * The module `Function.Related` has been deprecated in favour of `Function.Related.Propositional`

src/Algebra/Construct/NaturalChoice/Base.agda

@@ -11,7 +11,7 @@ open import Algebra.Core
 open import Level as L hiding (_⊔_)
 open import Function.Base using (flip)
 open import Relation.Binary
-open import Relation.Binary.Construct.Converse using ()
+open import Relation.Binary.Construct.Flip.EqAndOrd using ()
   renaming (totalPreorder to flipOrder)
 import Relation.Binary.Properties.TotalOrder as TotalOrderProperties
 

src/Algebra/Construct/NaturalChoice/Max.agda

@@ -14,7 +14,7 @@ module Algebra.Construct.NaturalChoice.Max
 open import Algebra.Core
 open import Algebra.Definitions
 open import Algebra.Construct.NaturalChoice.Base
-open import Relation.Binary.Construct.Converse using ()
+open import Relation.Binary.Construct.Flip.EqAndOrd using ()
   renaming (totalOrder to flip)
 
 open TotalOrder totalOrder renaming (Carrier to A)

src/Algebra/Construct/NaturalChoice/MaxOp.agda

@@ -12,7 +12,7 @@ open import Algebra.Construct.NaturalChoice.Base
 import Algebra.Construct.NaturalChoice.MinOp as MinOp
 open import Function.Base using (flip)
 open import Relation.Binary
-open import Relation.Binary.Construct.Converse using ()
+open import Relation.Binary.Construct.Flip.EqAndOrd using ()
   renaming (totalPreorder to flipOrder)
 
 module Algebra.Construct.NaturalChoice.MaxOp

src/Data/Fin/Induction.agda

@@ -23,8 +23,8 @@ open import Induction.WellFounded as WF
 open import Level using (Level)
 open import Relation.Binary
   using (Rel; Decidable; IsPartialOrder; IsStrictPartialOrder; StrictPartialOrder)
-import Relation.Binary.Construct.Converse as Converse
-import Relation.Binary.Construct.Flip as Flip
+import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
+import Relation.Binary.Construct.Flip.Ord as Ord
 import Relation.Binary.Construct.NonStrictToStrict as ToStrict
 import Relation.Binary.Construct.On as On
 open import Relation.Binary.Definitions using (Tri; tri<; tri≈; tri>)
@@ -123,7 +123,7 @@ module _ {_≈_ : Rel (Fin n) ℓ} where
     pigeon : (xs : Vec (Fin n) n) → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_
     pigeon xs i∷xs↑ =
       let (i₁ , i₂ , i₁<i₂ , xs[i₁]≡xs[i₂]) = pigeonhole (n<1+n n) (Vec.lookup (i ∷ xs)) in
-      let xs[i₁]⊏xs[i₂] = Linkedₚ.lookup⁺ (Flip.transitive _⊏_ ⊏.trans) {xs = i ∷ xs} i∷xs↑ i₁<i₂ in
+      let xs[i₁]⊏xs[i₂] = Linkedₚ.lookup⁺ (Ord.transitive _⊏_ ⊏.trans) {xs = i ∷ xs} i∷xs↑ i₁<i₂ in
       let xs[i₁]⊏xs[i₁] = ⊏.<-respʳ-≈ (⊏.Eq.reflexive xs[i₁]≡xs[i₂]) xs[i₁]⊏xs[i₂] in
       contradiction xs[i₁]⊏xs[i₁] (⊏.irrefl ⊏.Eq.refl)
 
@@ -137,7 +137,7 @@ module _ {_≈_ : Rel (Fin n) ℓ} where
 
   spo-noetherian : ∀ {r} {_⊏_ : Rel (Fin n) r} →
                    IsStrictPartialOrder _≈_ _⊏_ → WellFounded (flip _⊏_)
-  spo-noetherian isSPO = spo-wellFounded (Converse.isStrictPartialOrder isSPO)
+  spo-noetherian isSPO = spo-wellFounded (EqAndOrd.isStrictPartialOrder isSPO)
 
   po-noetherian : ∀ {r} {_⊑_ : Rel (Fin n) r} → IsPartialOrder _≈_ _⊑_ →
                   WellFounded (flip (ToStrict._<_ _≈_ _⊑_))

src/Relation/Binary/Construct/Converse.agda

@@ -1,195 +1,17 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Many properties which hold for `∼` also hold for `flip ∼`. Unlike
--- the module `Relation.Binary.Construct.Flip` this module does not
--- flip the underlying equality.
+-- This module is DEPRECATED. Please use
+-- `Relation.Binary.Construct.Flip.EqAndOrd` instead.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary
-
 module Relation.Binary.Construct.Converse where
 
-open import Data.Product
-open import Function.Base using (flip; _∘_)
-open import Level using (Level)
-
-private
-  variable
-    a b p ℓ ℓ₁ ℓ₂ : Level
-    A B : Set a
-    ≈ ∼ ≤ < : Rel A ℓ
-
-------------------------------------------------------------------------
--- Properties
-
-module _ (∼ : Rel A ℓ) where
-
-  refl : Reflexive ∼ → Reflexive (flip ∼)
-  refl refl = refl
-
-  sym : Symmetric ∼ → Symmetric (flip ∼)
-  sym sym = sym
-
-  trans : Transitive ∼ → Transitive (flip ∼)
-  trans trans = flip trans
-
-  asym : Asymmetric ∼ → Asymmetric (flip ∼)
-  asym asym = asym
-
-  total : Total ∼ → Total (flip ∼)
-  total total x y = total y x
-
-  resp : ∀ {p} (P : A → Set p) → Symmetric ∼ →
-             P Respects ∼ → P Respects (flip ∼)
-  resp _ sym resp ∼ = resp (sym ∼)
-
-  max : ∀ {⊥} → Minimum ∼ ⊥ → Maximum (flip ∼) ⊥
-  max min = min
-
-  min : ∀ {⊤} → Maximum ∼ ⊤ → Minimum (flip ∼) ⊤
-  min max = max
-
-module _ {≈ : Rel A ℓ₁} (∼ : Rel A ℓ₂) where
-
-  reflexive : Symmetric ≈ → (≈ ⇒ ∼) → (≈ ⇒ flip ∼)
-  reflexive sym impl = impl ∘ sym
-
-  irrefl : Symmetric ≈ → Irreflexive ≈ ∼ → Irreflexive ≈ (flip ∼)
-  irrefl sym irrefl x≈y y∼x = irrefl (sym x≈y) y∼x
-
-  antisym : Antisymmetric ≈ ∼ → Antisymmetric ≈ (flip ∼)
-  antisym antisym = flip antisym
-
-  compare : Trichotomous ≈ ∼ → Trichotomous ≈ (flip ∼)
-  compare cmp x y with cmp x y
-  ... | tri< x<y x≉y y≮x = tri> y≮x x≉y x<y
-  ... | tri≈ x≮y x≈y y≮x = tri≈ y≮x x≈y x≮y
-  ... | tri> x≮y x≉y y<x = tri< y<x x≉y x≮y
-
-module _ (∼₁ : Rel A ℓ₁) (∼₂ : Rel A ℓ₂) where
-
-  resp₂ : ∼₁ Respects₂ ∼₂ → (flip ∼₁) Respects₂ ∼₂
-  resp₂ (resp₁ , resp₂) = resp₂ , resp₁
-
-module _ (∼ : REL A B ℓ) where
-
-  dec : Decidable ∼ → Decidable (flip ∼)
-  dec dec = flip dec
-
-------------------------------------------------------------------------
--- Structures
-
-isEquivalence : IsEquivalence ≈ → IsEquivalence (flip ≈)
-isEquivalence {≈ = ≈} eq = record
-  { refl  = refl  ≈ Eq.refl
-  ; sym   = sym   ≈ Eq.sym
-  ; trans = trans ≈ Eq.trans
-  } where module Eq = IsEquivalence eq
-
-isDecEquivalence : IsDecEquivalence ≈ → IsDecEquivalence (flip ≈)
-isDecEquivalence {≈ = ≈} eq = record
-  { isEquivalence = isEquivalence Dec.isEquivalence
-  ; _≟_           = dec ≈ Dec._≟_
-  } where module Dec = IsDecEquivalence eq
-
-isPreorder : IsPreorder ≈ ∼ → IsPreorder ≈ (flip ∼)
-isPreorder {≈ = ≈} {∼ = ∼} O = record
-  { isEquivalence = O.isEquivalence
-  ; reflexive     = reflexive ∼ O.Eq.sym O.reflexive
-  ; trans         = trans ∼ O.trans
-  } where module O = IsPreorder O
-
-isTotalPreorder : IsTotalPreorder ≈ ∼ → IsTotalPreorder ≈ (flip ∼)
-isTotalPreorder O = record
-  { isPreorder = isPreorder O.isPreorder
-  ; total      = total _ O.total
-  } where module O = IsTotalPreorder O
-
-isPartialOrder : IsPartialOrder ≈ ≤ → IsPartialOrder ≈ (flip ≤)
-isPartialOrder {≤ = ≤} O = record
-  { isPreorder = isPreorder O.isPreorder
-  ; antisym    = antisym ≤ O.antisym
-  } where module O = IsPartialOrder O
-
-isTotalOrder : IsTotalOrder ≈ ≤ → IsTotalOrder ≈ (flip ≤)
-isTotalOrder O = record
-  { isPartialOrder = isPartialOrder O.isPartialOrder
-  ; total          = total _ O.total
-  } where module O = IsTotalOrder O
-
-isDecTotalOrder : IsDecTotalOrder ≈ ≤ → IsDecTotalOrder ≈ (flip ≤)
-isDecTotalOrder O = record
-  { isTotalOrder = isTotalOrder O.isTotalOrder
-  ; _≟_          = O._≟_
-  ; _≤?_         = dec _ O._≤?_
-  } where module O = IsDecTotalOrder O
-
-isStrictPartialOrder : IsStrictPartialOrder ≈ < →
-                       IsStrictPartialOrder ≈ (flip <)
-isStrictPartialOrder {< = <} O = record
-  { isEquivalence = O.isEquivalence
-  ; irrefl        = irrefl < O.Eq.sym O.irrefl
-  ; trans         = trans < O.trans
-  ; <-resp-≈      = resp₂ _ _ O.<-resp-≈
-  } where module O = IsStrictPartialOrder O
-
-isStrictTotalOrder : IsStrictTotalOrder ≈ < →
-                     IsStrictTotalOrder ≈ (flip <)
-isStrictTotalOrder {< = <} O = record
-  { isEquivalence = O.isEquivalence
-  ; trans         = trans < O.trans
-  ; compare       = compare _ O.compare
-  } where module O = IsStrictTotalOrder O
-
-------------------------------------------------------------------------
--- Bundles
-
-setoid : Setoid a ℓ → Setoid a ℓ
-setoid S = record
-  { isEquivalence = isEquivalence S.isEquivalence
-  } where module S = Setoid S
-
-decSetoid : DecSetoid a ℓ → DecSetoid a ℓ
-decSetoid S = record
-  { isDecEquivalence = isDecEquivalence S.isDecEquivalence
-  } where module S = DecSetoid S
-
-preorder : Preorder a ℓ₁ ℓ₂ → Preorder a ℓ₁ ℓ₂
-preorder O = record
-  { isPreorder = isPreorder O.isPreorder
-  } where module O = Preorder O
-
-totalPreorder : TotalPreorder a ℓ₁ ℓ₂ → TotalPreorder a ℓ₁ ℓ₂
-totalPreorder O = record
-  { isTotalPreorder = isTotalPreorder O.isTotalPreorder
-  } where module O = TotalPreorder O
-
-poset : Poset a ℓ₁ ℓ₂ → Poset a ℓ₁ ℓ₂
-poset O = record
-  { isPartialOrder = isPartialOrder O.isPartialOrder
-  } where module O = Poset O
-
-totalOrder : TotalOrder a ℓ₁ ℓ₂ → TotalOrder a ℓ₁ ℓ₂
-totalOrder O = record
-  { isTotalOrder = isTotalOrder O.isTotalOrder
-  } where module O = TotalOrder O
-
-decTotalOrder : DecTotalOrder a ℓ₁ ℓ₂ → DecTotalOrder a ℓ₁ ℓ₂
-decTotalOrder O = record
-  { isDecTotalOrder = isDecTotalOrder O.isDecTotalOrder
-  } where module O = DecTotalOrder O
-
-strictPartialOrder : StrictPartialOrder a ℓ₁ ℓ₂ →
-                     StrictPartialOrder a ℓ₁ ℓ₂
-strictPartialOrder O = record
-  { isStrictPartialOrder = isStrictPartialOrder O.isStrictPartialOrder
-  } where module O = StrictPartialOrder O
+open import Relation.Binary.Construct.Flip.EqAndOrd public
 
-strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂ →
-                   StrictTotalOrder a ℓ₁ ℓ₂
-strictTotalOrder O = record
-  { isStrictTotalOrder = isStrictTotalOrder O.isStrictTotalOrder
-  } where module O = StrictTotalOrder O
+{-# WARNING_ON_IMPORT
+"Relation.Binary.Construct.Converse was deprecated in v2.0.
+Use Relation.Binary.Construct.Flip.EqAndOrd instead."
+#-}

src/Relation/Binary/Construct/Flip.Agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Relation.Binary.Construct.Flip.Ord` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Construct.Flip where
+
+open import Relation.Binary.Construct.Flip.Ord public
+
+{-# WARNING_ON_IMPORT
+"Relation.Binary.Construct.Flip was deprecated in v2.0.
+Use Relation.Binary.Construct.Flip.Ord instead."
+#-}