------------------------------------------------------------------------
-- The Agda standard library
--
-- Many properties which hold for `∼` also hold for `flip ∼`. Unlike
-- the module `Relation.Binary.Construct.Flip.EqAndOrd` this module
-- flips both the relation and the underlying equality.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary.Core using (Rel; REL; _⇒_)
open import Relation.Binary.Bundles
  using (Setoid; DecSetoid; Preorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder)
open import Relation.Binary.Structures
  using (IsEquivalence; IsDecEquivalence; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder)
open import Relation.Binary.Definitions
  using (Reflexive; Symmetric; Transitive; Asymmetric; Total; _Respects_; _Respects₂_; Minimum; Maximum; Irreflexive; Antisymmetric; Trichotomous; Decidable)

module Relation.Binary.Construct.Flip.Ord where

open import Data.Product.Base using (_,_)
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

  reflexive : Reflexive ∼ → Reflexive (flip ∼)
  reflexive refl = refl

  symmetric : Symmetric ∼ → Symmetric (flip ∼)
  symmetric sym = sym

  transitive : Transitive ∼ → Transitive (flip ∼)
  transitive trans = flip trans

  asymmetric : Asymmetric ∼ → Asymmetric (flip ∼)
  asymmetric asym = asym

  total : Total ∼ → Total (flip ∼)
  total total x y = total y x

  respects : ∀ (P : A → Set p) → Symmetric ∼ →
             P Respects ∼ → P Respects flip ∼
  respects _ sym resp ∼ = resp (sym ∼)

  max : ∀ {⊥} → Minimum ∼ ⊥ → Maximum (flip ∼) ⊥
  max min = min

  min : ∀ {⊤} → Maximum ∼ ⊤ → Minimum (flip ∼) ⊤
  min max = max

module _ (≈ : REL A B ℓ₁) (∼ : REL A B ℓ₂) where

  implies : ≈ ⇒ ∼ → flip ≈ ⇒ flip ∼
  implies impl = impl

  irreflexive : Irreflexive ≈ ∼ → Irreflexive (flip ≈) (flip ∼)
  irreflexive irrefl = irrefl

module _ (≈ : Rel A ℓ₁) (∼ : Rel A ℓ₂) where

  antisymmetric : Antisymmetric ≈ ∼ → Antisymmetric (flip ≈) (flip ∼)
  antisymmetric antisym = antisym

  trichotomous : Trichotomous ≈ ∼ → Trichotomous (flip ≈) (flip ∼)
  trichotomous compare x y = compare y x

module _ (∼₁ : Rel A ℓ₁) (∼₂ : Rel A ℓ₂) where

  respects₂ : Symmetric ∼₂ → ∼₁ Respects₂ ∼₂ → flip ∼₁ Respects₂ flip ∼₂
  respects₂ sym (resp₁ , resp₂) = (resp₂ ∘ sym , resp₁ ∘ sym)

module _ (∼ : REL A B ℓ) where

  decidable : Decidable ∼ → Decidable (flip ∼)
  decidable dec x y = dec y x

------------------------------------------------------------------------
-- Structures

isEquivalence : IsEquivalence ≈ → IsEquivalence (flip ≈)
isEquivalence {≈ = ≈} eq = record
  { refl  = reflexive  ≈ Eq.refl
  ; sym   = symmetric  ≈ Eq.sym
  ; trans = transitive ≈ Eq.trans
  } where module Eq = IsEquivalence eq

isDecEquivalence : IsDecEquivalence ≈ → IsDecEquivalence (flip ≈)
isDecEquivalence {≈ = ≈} dec = record
  { isEquivalence = isEquivalence Dec.isEquivalence
  ; _≟_           = decidable ≈ Dec._≟_
  } where module Dec = IsDecEquivalence dec

isPreorder : IsPreorder ≈ ∼ → IsPreorder (flip ≈) (flip ∼)
isPreorder {≈ = ≈} {∼ = ∼} O = record
  { isEquivalence = isEquivalence O.isEquivalence
  ; reflexive     = implies ≈ ∼ O.reflexive
  ; trans         = transitive ∼ O.trans
  } where module O = IsPreorder O

isPartialOrder : IsPartialOrder ≈ ≤ → IsPartialOrder (flip ≈) (flip ≤)
isPartialOrder {≈ = ≈} {≤ = ≤} O = record
  { isPreorder = isPreorder O.isPreorder
  ; antisym    = antisymmetric ≈ ≤ O.antisym
  } where module O = IsPartialOrder O

isTotalOrder : IsTotalOrder ≈ ≤ → IsTotalOrder (flip ≈) (flip ≤)
isTotalOrder {≈ = ≈} {≤ = ≤} O = record
  { isPartialOrder = isPartialOrder O.isPartialOrder
  ; total          = total ≤ O.total
  }
  where module O = IsTotalOrder O

isDecTotalOrder : IsDecTotalOrder ≈ ≤ → IsDecTotalOrder (flip ≈) (flip ≤)
isDecTotalOrder {≈ = ≈} {≤ = ≤} O = record
  { isTotalOrder = isTotalOrder O.isTotalOrder
  ; _≟_          = decidable ≈ O._≟_
  ; _≤?_         = decidable ≤ O._≤?_
  } where module O = IsDecTotalOrder O

isStrictPartialOrder : IsStrictPartialOrder ≈ < →
                       IsStrictPartialOrder (flip ≈) (flip <)
isStrictPartialOrder {≈ = ≈} {< = <} O = record
  { isEquivalence = isEquivalence O.isEquivalence
  ; irrefl        = irreflexive ≈ < O.irrefl
  ; trans         = transitive < O.trans
  ; <-resp-≈      = respects₂ < ≈ O.Eq.sym O.<-resp-≈
  } where module O = IsStrictPartialOrder O

isStrictTotalOrder : IsStrictTotalOrder ≈ < →
                     IsStrictTotalOrder (flip ≈) (flip <)
isStrictTotalOrder {≈ = ≈} {< = <} O = record
  { isStrictPartialOrder = isStrictPartialOrder O.isStrictPartialOrder
  ; compare              = trichotomous ≈ < O.compare
  } where module O = IsStrictTotalOrder O

------------------------------------------------------------------------
-- Bundles

setoid : Setoid a ℓ → Setoid a ℓ
setoid S = record
  { _≈_           = flip S._≈_
  ; isEquivalence = isEquivalence S.isEquivalence
  } where module S = Setoid S

decSetoid : DecSetoid a ℓ → DecSetoid a ℓ
decSetoid S = record
  { _≈_              = flip S._≈_
  ; 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

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