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