------------------------------------------------------------------------
-- 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ᶜ)