------------------------------------------------------------------------
-- 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ᶜ)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4