------------------------------------------------------------------------ -- The Agda standard library -- -- Many properties which hold for `∼` also hold for `flip ∼`. Unlike -- the module `Relation.Binary.Construct.Flip.Ord` this module does not -- flip the underlying equality. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Relation.Binary.Construct.Flip.EqAndOrd where open import Data.Product.Base using (_,_) open import Function.Base using (flip; _∘_) open import Level using (Level) open import Relation.Binary.Core using (Rel; REL; _⇒_) open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder; Poset; TotalOrder; DecTotalOrder ; StrictPartialOrder; StrictTotalOrder; TotalPreorder) open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence; IsPreorder; IsPartialOrder ; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder ; IsStrictTotalOrder; IsTotalPreorder) open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive; Asymmetric; Total; _Respects_ ; _Respects₂_; Minimum; Maximum; Irreflexive; Antisymmetric ; Trichotomous; Decidable; tri<; tri>; tri≈) 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 { isStrictPartialOrder = isStrictPartialOrder O.isStrictPartialOrder ; 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 strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂ → StrictTotalOrder a ℓ₁ ℓ₂ strictTotalOrder O = record { isStrictTotalOrder = isStrictTotalOrder O.isStrictTotalOrder } where module O = StrictTotalOrder O