------------------------------------------------------------------------
-- The Agda standard library
--
-- Many properties which hold for _∼_ also hold for _∼_ on f
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Relation.Binary

module Relation.Binary.Construct.On where

open import Function
open import Data.Product

module _ {a b} {A : Set a} {B : Set b} (f : B → A) where

  implies : ∀ {ℓ₁ ℓ₂} (≈ : Rel A ℓ₁) (∼ : Rel A ℓ₂) →
            ≈ ⇒ ∼ → (≈ on f) ⇒ (∼ on f)
  implies _ _ impl = impl

  reflexive : ∀ {ℓ} (∼ : Rel A ℓ) → Reflexive ∼ → Reflexive (∼ on f)
  reflexive _ refl = refl

  irreflexive : ∀ {ℓ₁ ℓ₂} (≈ : Rel A ℓ₁) (∼ : Rel A ℓ₂) →
                Irreflexive ≈ ∼ → Irreflexive (≈ on f) (∼ on f)
  irreflexive _ _ irrefl = irrefl

  symmetric : ∀ {ℓ} (∼ : Rel A ℓ) → Symmetric ∼ → Symmetric (∼ on f)
  symmetric _ sym = sym

  transitive : ∀ {ℓ} (∼ : Rel A ℓ) → Transitive ∼ → Transitive (∼ on f)
  transitive _ trans = trans

  antisymmetric : ∀ {ℓ₁ ℓ₂} (≈ : Rel A ℓ₁) (≤ : Rel A ℓ₂) →
                  Antisymmetric ≈ ≤ → Antisymmetric (≈ on f) (≤ on f)
  antisymmetric _ _ antisym = antisym

  asymmetric : ∀ {ℓ} (< : Rel A ℓ) → Asymmetric < → Asymmetric (< on f)
  asymmetric _ asym = asym

  respects : ∀ {ℓ p} (∼ : Rel A ℓ) (P : A → Set p) →
             P Respects ∼ → (P ∘ f) Respects (∼ on f)
  respects _ _ resp = resp

  respects₂ : ∀ {ℓ₁ ℓ₂} (∼₁ : Rel A ℓ₁) (∼₂ : Rel A ℓ₂) →
              ∼₁ Respects₂ ∼₂ → (∼₁ on f) Respects₂ (∼₂ on f)
  respects₂ _ _ (resp₁ , resp₂) =
    ((λ {_} {_} {_} → resp₁) , λ {_} {_} {_} → resp₂)

  decidable : ∀ {ℓ} (∼ : Rel A ℓ) → Decidable ∼ → Decidable (∼ on f)
  decidable _ dec = λ x y → dec (f x) (f y)

  total : ∀ {ℓ} (∼ : Rel A ℓ) → Total ∼ → Total (∼ on f)
  total _ tot = λ x y → tot (f x) (f y)

  trichotomous : ∀ {ℓ₁ ℓ₂} (≈ : Rel A ℓ₁) (< : Rel A ℓ₂) →
                 Trichotomous ≈ < → Trichotomous (≈ on f) (< on f)
  trichotomous _ _ compare = λ x y → compare (f x) (f y)

  isEquivalence : ∀ {ℓ} {≈ : Rel A ℓ} →
                  IsEquivalence ≈ → IsEquivalence (≈ on f)
  isEquivalence {≈ = ≈} eq = record
    { refl  = reflexive  ≈ Eq.refl
    ; sym   = symmetric  ≈ Eq.sym
    ; trans = transitive ≈ Eq.trans
    }
    where module Eq = IsEquivalence eq

  isPreorder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {∼ : Rel A ℓ₂} →
               IsPreorder ≈ ∼ → IsPreorder (≈ on f) (∼ on f)
  isPreorder {≈ = ≈} {∼} pre = record
    { isEquivalence = isEquivalence Pre.isEquivalence
    ; reflexive     = implies ≈ ∼ Pre.reflexive
    ; trans         = transitive ∼ Pre.trans
    }
    where module Pre = IsPreorder pre

  isDecEquivalence : ∀ {ℓ} {≈ : Rel A ℓ} →
                     IsDecEquivalence ≈ → IsDecEquivalence (≈ on f)
  isDecEquivalence {≈ = ≈} dec = record
    { isEquivalence = isEquivalence Dec.isEquivalence
    ; _≟_           = decidable ≈ Dec._≟_
    }
    where module Dec = IsDecEquivalence dec

  isPartialOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
                   IsPartialOrder ≈ ≤ →
                   IsPartialOrder (≈ on f) (≤ on f)
  isPartialOrder {≈ = ≈} {≤} po = record
    { isPreorder = isPreorder Po.isPreorder
    ; antisym    = antisymmetric ≈ ≤ Po.antisym
    }
    where module Po = IsPartialOrder po

  isDecPartialOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
                      IsDecPartialOrder ≈ ≤ →
                      IsDecPartialOrder (≈ on f) (≤ on f)
  isDecPartialOrder dpo = record
    { isPartialOrder = isPartialOrder DPO.isPartialOrder
    ; _≟_            = decidable _ DPO._≟_
    ; _≤?_           = decidable _ DPO._≤?_
    }
    where module DPO = IsDecPartialOrder dpo

  isStrictPartialOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
                         IsStrictPartialOrder ≈ < →
                         IsStrictPartialOrder (≈ on f) (< on f)
  isStrictPartialOrder {≈ = ≈} {<} spo = record
    { isEquivalence = isEquivalence Spo.isEquivalence
    ; irrefl        = irreflexive ≈ < Spo.irrefl
    ; trans         = transitive < Spo.trans
    ; <-resp-≈      = respects₂ < ≈ Spo.<-resp-≈
    }
    where module Spo = IsStrictPartialOrder spo

  isTotalOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
                 IsTotalOrder ≈ ≤ →
                 IsTotalOrder (≈ on f) (≤ on f)
  isTotalOrder {≈ = ≈} {≤} to = record
    { isPartialOrder = isPartialOrder To.isPartialOrder
    ; total          = total ≤ To.total
    }
    where module To = IsTotalOrder to

  isDecTotalOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
                    IsDecTotalOrder ≈ ≤ →
                    IsDecTotalOrder (≈ on f) (≤ on f)
  isDecTotalOrder {≈ = ≈} {≤} dec = record
    { isTotalOrder = isTotalOrder Dec.isTotalOrder
    ; _≟_          = decidable ≈ Dec._≟_
    ; _≤?_         = decidable ≤ Dec._≤?_
    }
    where module Dec = IsDecTotalOrder dec

  isStrictTotalOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
                       IsStrictTotalOrder ≈ < →
                       IsStrictTotalOrder (≈ on f) (< on f)
  isStrictTotalOrder {≈ = ≈} {<} sto = record
    { isEquivalence = isEquivalence Sto.isEquivalence
    ; trans         = transitive < Sto.trans
    ; compare       = trichotomous ≈ < Sto.compare
    }
    where module Sto = IsStrictTotalOrder sto

preorder : ∀ {p₁ p₂ p₃ b} {B : Set b} (P : Preorder p₁ p₂ p₃) →
           (B → Preorder.Carrier P) → Preorder _ _ _
preorder P f = record
  { isPreorder = isPreorder f (Preorder.isPreorder P)
  }

setoid : ∀ {s₁ s₂ b} {B : Set b} (S : Setoid s₁ s₂) →
         (B → Setoid.Carrier S) → Setoid _ _
setoid S f = record
  { isEquivalence = isEquivalence f (Setoid.isEquivalence S)
  }

decSetoid : ∀ {d₁ d₂ b} {B : Set b} (D : DecSetoid d₁ d₂) →
            (B → DecSetoid.Carrier D) → DecSetoid _ _
decSetoid D f = record
  { isDecEquivalence = isDecEquivalence f (DecSetoid.isDecEquivalence D)
  }

poset : ∀ {p₁ p₂ p₃ b} {B : Set b} (P : Poset p₁ p₂ p₃) →
        (B → Poset.Carrier P) → Poset _ _ _
poset P f = record
  { isPartialOrder = isPartialOrder f (Poset.isPartialOrder P)
  }

decPoset : ∀ {d₁ d₂ d₃ b} {B : Set b} (D : DecPoset d₁ d₂ d₃) →
           (B → DecPoset.Carrier D) → DecPoset _ _ _
decPoset D f = record
  { isDecPartialOrder =
      isDecPartialOrder f (DecPoset.isDecPartialOrder D)
  }

strictPartialOrder :
  ∀ {s₁ s₂ s₃ b} {B : Set b} (S : StrictPartialOrder s₁ s₂ s₃) →
  (B → StrictPartialOrder.Carrier S) → StrictPartialOrder _ _ _
strictPartialOrder S f = record
  { isStrictPartialOrder =
      isStrictPartialOrder f (StrictPartialOrder.isStrictPartialOrder S)
  }

totalOrder : ∀ {t₁ t₂ t₃ b} {B : Set b} (T : TotalOrder t₁ t₂ t₃) →
             (B → TotalOrder.Carrier T) → TotalOrder _ _ _
totalOrder T f = record
  { isTotalOrder = isTotalOrder f (TotalOrder.isTotalOrder T)
  }

decTotalOrder :
  ∀ {d₁ d₂ d₃ b} {B : Set b} (D : DecTotalOrder d₁ d₂ d₃) →
  (B → DecTotalOrder.Carrier D) → DecTotalOrder _ _ _
decTotalOrder D f = record
  { isDecTotalOrder = isDecTotalOrder f (DecTotalOrder.isDecTotalOrder D)
  }

strictTotalOrder :
  ∀ {s₁ s₂ s₃ b} {B : Set b} (S : StrictTotalOrder s₁ s₂ s₃) →
  (B → StrictTotalOrder.Carrier S) → StrictTotalOrder _ _ _
strictTotalOrder S f = record
  { isStrictTotalOrder =
      isStrictTotalOrder f (StrictTotalOrder.isStrictTotalOrder S)
  }