------------------------------------------------------------------------ -- The Agda standard library -- -- Ways to give instances of certain structures where some fields can -- be given in terms of others ------------------------------------------------------------------------ -- The contents of this module should be accessed via `Relation.Binary`. {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Core using (Rel) module Relation.Binary.Structures.Biased {a ℓ} {A : Set a} -- The underlying set (_≈_ : Rel A ℓ) -- The underlying equality relation where open import Level using (Level; _⊔_) open import Relation.Binary.Consequences using (tri⇒irr; tri⇒asym; trans∧tri⇒resp) open import Relation.Binary.Definitions using (Transitive; Trichotomous) open import Relation.Binary.Structures _≈_ private variable ℓ₂ : Level -- To construct a StrictTotalOrder you only need to prove transitivity and -- trichotomy as the current implementation of `Trichotomous` subsumes -- irreflexivity and asymmetry. record IsStrictTotalOrderᶜ (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where field isEquivalence : IsEquivalence trans : Transitive _<_ compare : Trichotomous _≈_ _<_ isStrictTotalOrderᶜ : IsStrictTotalOrder _<_ isStrictTotalOrderᶜ = record { isStrictPartialOrder = record { isEquivalence = isEquivalence ; irrefl = tri⇒irr compare ; trans = trans ; <-resp-≈ = trans∧tri⇒resp Eq.sym Eq.trans trans compare } ; compare = compare } where module Eq = IsEquivalence isEquivalence open IsStrictTotalOrderᶜ public using (isStrictTotalOrderᶜ)