------------------------------------------------------------------------
-- Many properties which hold for _∼_ also hold for _∼_ on₁ f
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.On {A B : Set} (f : B  A) where

open import Data.Function
open import Data.Product

implies :         ( on₁ f)  ( on₁ f)
implies _ _ impl = impl

reflexive :    Reflexive   Reflexive ( on₁ f)
reflexive _ refl = refl

irreflexive :     Irreflexive    Irreflexive ( on₁ f) ( on₁ f)
irreflexive _ _ irrefl = irrefl

symmetric :    Symmetric   Symmetric ( on₁ f)
symmetric _ sym = sym

transitive :    Transitive   Transitive ( on₁ f)
transitive _ trans = trans

antisymmetric :    
                Antisymmetric    Antisymmetric ( on₁ f) ( on₁ f)
antisymmetric _ _ antisym = antisym

asymmetric :  <  Asymmetric <  Asymmetric (< on₁ f)
asymmetric _ asym = asym

respects :   P  P Respects   (P ∘₀ f) Respects ( on₁ f)
respects _ _ resp = resp

respects₂ :  ∼₁ ∼₂  ∼₁ Respects₂ ∼₂  (∼₁ on₁ f) Respects₂ (∼₂ on₁ f)
respects₂ _ _ (resp₁ , resp₂) =
  ((λ {_} {_} {_}  resp₁) , λ {_} {_} {_}  resp₂)

decidable :    Decidable   Decidable ( on₁ f)
decidable _ dec = λ x y  dec (f x) (f y)

total :    Total   Total ( on₁ f)
total _ tot = λ x y  tot (f x) (f y)

trichotomous :   < 
               Trichotomous  <  Trichotomous ( on₁ f) (< on₁ f)
trichotomous _ _ compare = λ x y  compare (f x) (f y)

isEquivalence :  {}  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 :  { }  IsPreorder    IsPreorder ( on₁ f) ( on₁ f)
isPreorder {} {} pre = record
  { isEquivalence = isEquivalence Pre.isEquivalence
  ; reflexive     = implies   Pre.reflexive
  ; trans         = transitive  Pre.trans
  ; ∼-resp-≈      = respects₂   Pre.∼-resp-≈
  }
  where module Pre = IsPreorder pre

isDecEquivalence :  {} 
                   IsDecEquivalence   IsDecEquivalence ( on₁ f)
isDecEquivalence {} dec = record
  { isEquivalence = isEquivalence Dec.isEquivalence
  ; _≟_           = decidable  Dec._≟_
  }
  where module Dec = IsDecEquivalence dec

isPartialOrder :  { } 
                 IsPartialOrder   
                 IsPartialOrder ( on₁ f) ( on₁ f)
isPartialOrder {} {} po = record
  { isPreorder = isPreorder Po.isPreorder
  ; antisym    = antisymmetric   Po.antisym
  }
  where module Po = IsPartialOrder po

isStrictPartialOrder :  { <} 
                       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 :  { } 
               IsTotalOrder   
               IsTotalOrder ( on₁ f) ( on₁ f)
isTotalOrder {} {} to = record
  { isPartialOrder = isPartialOrder To.isPartialOrder
  ; total          = total  To.total
  }
  where module To = IsTotalOrder to

isDecTotalOrder :  { } 
                  IsDecTotalOrder   
                  IsDecTotalOrder ( on₁ f) ( on₁ f)
isDecTotalOrder {} {} dec = record
  { isTotalOrder = isTotalOrder Dec.isTotalOrder
  ; _≟_          = decidable  Dec._≟_
  ; _≤?_         = decidable  Dec._≤?_
  }
  where module Dec = IsDecTotalOrder dec

isStrictTotalOrder :  { <} 
                     IsStrictTotalOrder  < 
                       IsStrictTotalOrder ( on₁ f) (< on₁ f)
isStrictTotalOrder {} {<} sto = record
  { isEquivalence = isEquivalence Sto.isEquivalence
  ; trans         = transitive < Sto.trans
  ; compare       = trichotomous  < Sto.compare
  ; <-resp-≈      = respects₂ <  Sto.<-resp-≈
  }
  where module Sto = IsStrictTotalOrder sto