{-# OPTIONS --without-K --safe #-}
open import Relation.Binary
module Relation.Binary.Construct.Converse where
open import Function.Base using (flip; _∘_)
open import Data.Product
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
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