------------------------------------------------------------------------ -- 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. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} open import Relation.Binary module Relation.Binary.Construct.Converse where open import Function.Base using (flip; _∘_) open import Data.Product ------------------------------------------------------------------------ -- Properties module _ {a ℓ} {A : Set a} (∼ : 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 _ {a ℓ₁ ℓ₂} {A : Set a} {≈ : 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 _ {a ℓ₁ ℓ₂} {A : Set a} (∼₁ : Rel A ℓ₁) (∼₂ : Rel A ℓ₂) where resp₂ : ∼₁ Respects₂ ∼₂ → (flip ∼₁) Respects₂ ∼₂ resp₂ (resp₁ , resp₂) = resp₂ , resp₁ module _ {a b ℓ} {A : Set a} {B : Set b} (∼ : REL A B ℓ) where dec : Decidable ∼ → Decidable (flip ∼) dec dec = flip dec ------------------------------------------------------------------------ -- Structures module _ {a ℓ} {A : Set a} {≈ : Rel A ℓ} where 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 module _ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {∼ : Rel A ℓ₂} where 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 module _ {a ℓ} where 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 module _ {a ℓ₁ ℓ₂} where 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
Generated from commit 2fd14c996b195ef101dff8919e837907ca0a08aa.