{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Binary.Construct.On where
open import Data.Product.Base using (_,_)
open import Function.Base using (_on_; _∘_)
open import Induction.WellFounded using (WellFounded; Acc; acc)
open import Level using (Level)
open import Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Bundles
using (Preorder; Setoid; DecSetoid; Poset; DecPoset; StrictPartialOrder; TotalOrder; DecTotalOrder; StrictTotalOrder)
open import Relation.Binary.Structures
using (IsEquivalence; IsDecEquivalence; IsPreorder; IsPartialOrder; IsDecPartialOrder; IsStrictPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictTotalOrder)
open import Relation.Binary.Definitions
using (Reflexive; Irreflexive; Symmetric; Transitive; Antisymmetric; Asymmetric; Decidable; Total; Trichotomous; _Respects_; _Respects₂_)
private
variable
a b p ℓ ℓ₁ ℓ₂ : Level
A : Set a
B : Set b
module _ (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 : (∼ : 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)
accessible : ∀ {∼ : Rel A ℓ} {x} → Acc ∼ (f x) → Acc (∼ on f) x
accessible (acc rs) = acc (λ fy<fx → accessible (rs fy<fx))
wellFounded : {∼ : Rel A ℓ} → WellFounded ∼ → WellFounded (∼ on f)
wellFounded wf x = accessible (wf (f x))
module _ (f : B → A) {≈ : Rel A ℓ₁} where
isEquivalence : IsEquivalence ≈ →
IsEquivalence (≈ on f)
isEquivalence eq = record
{ refl = reflexive f ≈ Eq.refl
; sym = symmetric f ≈ Eq.sym
; trans = transitive f ≈ Eq.trans
} where module Eq = IsEquivalence eq
isDecEquivalence : IsDecEquivalence ≈ →
IsDecEquivalence (≈ on f)
isDecEquivalence dec = record
{ isEquivalence = isEquivalence Dec.isEquivalence
; _≟_ = decidable f ≈ Dec._≟_
} where module Dec = IsDecEquivalence dec
module _ (f : B → A) {≈ : Rel A ℓ₁} {∼ : Rel A ℓ₂} where
isPreorder : IsPreorder ≈ ∼ → IsPreorder (≈ on f) (∼ on f)
isPreorder pre = record
{ isEquivalence = isEquivalence f Pre.isEquivalence
; reflexive = implies f ≈ ∼ Pre.reflexive
; trans = transitive f ∼ Pre.trans
} where module Pre = IsPreorder pre
isPartialOrder : IsPartialOrder ≈ ∼ →
IsPartialOrder (≈ on f) (∼ on f)
isPartialOrder po = record
{ isPreorder = isPreorder Po.isPreorder
; antisym = antisymmetric f ≈ ∼ Po.antisym
} where module Po = IsPartialOrder po
isDecPartialOrder : IsDecPartialOrder ≈ ∼ →
IsDecPartialOrder (≈ on f) (∼ on f)
isDecPartialOrder dpo = record
{ isPartialOrder = isPartialOrder DPO.isPartialOrder
; _≟_ = decidable f _ DPO._≟_
; _≤?_ = decidable f _ DPO._≤?_
} where module DPO = IsDecPartialOrder dpo
isStrictPartialOrder : IsStrictPartialOrder ≈ ∼ →
IsStrictPartialOrder (≈ on f) (∼ on f)
isStrictPartialOrder spo = record
{ isEquivalence = isEquivalence f Spo.isEquivalence
; irrefl = irreflexive f ≈ ∼ Spo.irrefl
; trans = transitive f ∼ Spo.trans
; <-resp-≈ = respects₂ f ∼ ≈ Spo.<-resp-≈
} where module Spo = IsStrictPartialOrder spo
isTotalOrder : IsTotalOrder ≈ ∼ →
IsTotalOrder (≈ on f) (∼ on f)
isTotalOrder to = record
{ isPartialOrder = isPartialOrder To.isPartialOrder
; total = total f ∼ To.total
} where module To = IsTotalOrder to
isDecTotalOrder : IsDecTotalOrder ≈ ∼ →
IsDecTotalOrder (≈ on f) (∼ on f)
isDecTotalOrder dec = record
{ isTotalOrder = isTotalOrder Dec.isTotalOrder
; _≟_ = decidable f ≈ Dec._≟_
; _≤?_ = decidable f ∼ Dec._≤?_
} where module Dec = IsDecTotalOrder dec
isStrictTotalOrder : IsStrictTotalOrder ≈ ∼ →
IsStrictTotalOrder (≈ on f) (∼ on f)
isStrictTotalOrder sto = record
{ isStrictPartialOrder = isStrictPartialOrder Sto.isStrictPartialOrder
; compare = trichotomous _ _ _ Sto.compare
} where module Sto = IsStrictTotalOrder sto
preorder : (P : Preorder a ℓ₁ ℓ₂) →
(B → Preorder.Carrier P) →
Preorder _ _ _
preorder P f = record
{ isPreorder = isPreorder f (Preorder.isPreorder P)
}
setoid : (S : Setoid a ℓ) →
(B → Setoid.Carrier S) →
Setoid _ _
setoid S f = record
{ isEquivalence = isEquivalence f (Setoid.isEquivalence S)
}
decSetoid : (D : DecSetoid a ℓ) →
(B → DecSetoid.Carrier D) →
DecSetoid _ _
decSetoid D f = record
{ isDecEquivalence = isDecEquivalence f (DecSetoid.isDecEquivalence D)
}
poset : ∀ (P : Poset a ℓ₁ ℓ₂) →
(B → Poset.Carrier P) →
Poset _ _ _
poset P f = record
{ isPartialOrder = isPartialOrder f (Poset.isPartialOrder P)
}
decPoset : (D : DecPoset a ℓ₁ ℓ₂) →
(B → DecPoset.Carrier D) →
DecPoset _ _ _
decPoset D f = record
{ isDecPartialOrder =
isDecPartialOrder f (DecPoset.isDecPartialOrder D)
}
strictPartialOrder : (S : StrictPartialOrder a ℓ₁ ℓ₂) →
(B → StrictPartialOrder.Carrier S) →
StrictPartialOrder _ _ _
strictPartialOrder S f = record
{ isStrictPartialOrder =
isStrictPartialOrder f (StrictPartialOrder.isStrictPartialOrder S)
}
totalOrder : (T : TotalOrder a ℓ₁ ℓ₂) →
(B → TotalOrder.Carrier T) →
TotalOrder _ _ _
totalOrder T f = record
{ isTotalOrder = isTotalOrder f (TotalOrder.isTotalOrder T)
}
decTotalOrder : (D : DecTotalOrder a ℓ₁ ℓ₂) →
(B → DecTotalOrder.Carrier D) →
DecTotalOrder _ _ _
decTotalOrder D f = record
{ isDecTotalOrder = isDecTotalOrder f (DecTotalOrder.isDecTotalOrder D)
}
strictTotalOrder : (S : StrictTotalOrder a ℓ₁ ℓ₂) →
(B → StrictTotalOrder.Carrier S) →
StrictTotalOrder _ _ _
strictTotalOrder S f = record
{ isStrictTotalOrder =
isStrictTotalOrder f (StrictTotalOrder.isStrictTotalOrder S)
}