------------------------------------------------------------------------
-- The Agda standard library
--
-- The lifting of a strict order to incorporate new extrema
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
-- This module is designed to be used with
-- Relation.Nullary.Construct.Add.Extrema
open import Relation.Binary.Core using (Rel)
module Relation.Binary.Construct.Add.Extrema.Strict
{a ℓ} {A : Set a} (_<_ : Rel A ℓ) where
open import Level
open import Function.Base using (_∘′_)
import Relation.Nullary.Construct.Add.Infimum as I using (⊥₋; [_])
open import Relation.Nullary.Construct.Add.Extrema using (⊥±; ⊤±; [_])
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
import Relation.Binary.Construct.Add.Infimum.Strict as AddInfimum
import Relation.Binary.Construct.Add.Supremum.Strict as AddSupremum
import Relation.Binary.Construct.Add.Extrema.Equality as Equality
import Relation.Binary.Construct.Add.Extrema.NonStrict as NonStrict
open import Relation.Binary.Definitions
using (Asymmetric; Transitive; Decidable; Irrelevant; Trichotomous
; Irreflexive; Trans; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
open import Relation.Binary.Structures
using (IsStrictPartialOrder; IsDecStrictPartialOrder; IsStrictTotalOrder)
------------------------------------------------------------------------
-- Definition
private
module Inf = AddInfimum _<_
module Sup = AddSupremum Inf._<₋_
open Sup using () renaming (_<⁺_ to _<±_) public
------------------------------------------------------------------------
-- Useful pattern synonyms
pattern ⊥±<[_] l = Sup.[ Inf.⊥₋<[ l ] ]
pattern [_] p = Sup.[ Inf.[ p ] ]
pattern ⊥±<⊤± = Sup.[ I.⊥₋ ]<⊤⁺
pattern [_]<⊤± k = Sup.[ I.[ k ] ]<⊤⁺
------------------------------------------------------------------------
-- Relational properties
[<]-injective : ∀ {k l} → [ k ] <± [ l ] → k < l
[<]-injective = Inf.[<]-injective ∘′ Sup.[<]-injective
<±-asym : Asymmetric _<_ → Asymmetric _<±_
<±-asym = Sup.<⁺-asym ∘′ Inf.<₋-asym
<±-trans : Transitive _<_ → Transitive _<±_
<±-trans = Sup.<⁺-trans ∘′ Inf.<₋-trans
<±-dec : Decidable _<_ → Decidable _<±_
<±-dec = Sup.<⁺-dec ∘′ Inf.<₋-dec
<±-irrelevant : Irrelevant _<_ → Irrelevant _<±_
<±-irrelevant = Sup.<⁺-irrelevant ∘′ Inf.<₋-irrelevant
module _ {r} {_≤_ : Rel A r} where
open NonStrict _≤_
<±-transʳ : Trans _≤_ _<_ _<_ → Trans _≤±_ _<±_ _<±_
<±-transʳ = Sup.<⁺-transʳ ∘′ Inf.<₋-transʳ
<±-transˡ : Trans _<_ _≤_ _<_ → Trans _<±_ _≤±_ _<±_
<±-transˡ = Sup.<⁺-transˡ ∘′ Inf.<₋-transˡ
------------------------------------------------------------------------
-- Relational properties + propositional equality
<±-cmp-≡ : Trichotomous _≡_ _<_ → Trichotomous _≡_ _<±_
<±-cmp-≡ = Sup.<⁺-cmp-≡ ∘′ Inf.<₋-cmp-≡
<±-irrefl-≡ : Irreflexive _≡_ _<_ → Irreflexive _≡_ _<±_
<±-irrefl-≡ = Sup.<⁺-irrefl-≡ ∘′ Inf.<₋-irrefl-≡
<±-respˡ-≡ : _<±_ Respectsˡ _≡_
<±-respˡ-≡ = Sup.<⁺-respˡ-≡
<±-respʳ-≡ : _<±_ Respectsʳ _≡_
<±-respʳ-≡ = Sup.<⁺-respʳ-≡
<±-resp-≡ : _<±_ Respects₂ _≡_
<±-resp-≡ = Sup.<⁺-resp-≡
------------------------------------------------------------------------
-- Relational properties + setoid equality
module _ {e} {_≈_ : Rel A e} where
open Equality _≈_
<±-cmp : Trichotomous _≈_ _<_ → Trichotomous _≈±_ _<±_
<±-cmp = Sup.<⁺-cmp ∘′ Inf.<₋-cmp
<±-irrefl : Irreflexive _≈_ _<_ → Irreflexive _≈±_ _<±_
<±-irrefl = Sup.<⁺-irrefl ∘′ Inf.<₋-irrefl
<±-respˡ-≈± : _<_ Respectsˡ _≈_ → _<±_ Respectsˡ _≈±_
<±-respˡ-≈± = Sup.<⁺-respˡ-≈⁺ ∘′ Inf.<₋-respˡ-≈₋
<±-respʳ-≈± : _<_ Respectsʳ _≈_ → _<±_ Respectsʳ _≈±_
<±-respʳ-≈± = Sup.<⁺-respʳ-≈⁺ ∘′ Inf.<₋-respʳ-≈₋
<±-resp-≈± : _<_ Respects₂ _≈_ → _<±_ Respects₂ _≈±_
<±-resp-≈± = Sup.<⁺-resp-≈⁺ ∘′ Inf.<₋-resp-≈₋
------------------------------------------------------------------------
-- Structures + propositional equality
<±-isStrictPartialOrder-≡ : IsStrictPartialOrder _≡_ _<_ →
IsStrictPartialOrder _≡_ _<±_
<±-isStrictPartialOrder-≡ =
Sup.<⁺-isStrictPartialOrder-≡ ∘′ Inf.<₋-isStrictPartialOrder-≡
<±-isDecStrictPartialOrder-≡ : IsDecStrictPartialOrder _≡_ _<_ →
IsDecStrictPartialOrder _≡_ _<±_
<±-isDecStrictPartialOrder-≡ =
Sup.<⁺-isDecStrictPartialOrder-≡ ∘′ Inf.<₋-isDecStrictPartialOrder-≡
<±-isStrictTotalOrder-≡ : IsStrictTotalOrder _≡_ _<_ →
IsStrictTotalOrder _≡_ _<±_
<±-isStrictTotalOrder-≡ =
Sup.<⁺-isStrictTotalOrder-≡ ∘′ Inf.<₋-isStrictTotalOrder-≡
------------------------------------------------------------------------
-- Structures + setoid equality
module _ {e} {_≈_ : Rel A e} where
open Equality _≈_
<±-isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_ →
IsStrictPartialOrder _≈±_ _<±_
<±-isStrictPartialOrder =
Sup.<⁺-isStrictPartialOrder ∘′ Inf.<₋-isStrictPartialOrder
<±-isDecStrictPartialOrder : IsDecStrictPartialOrder _≈_ _<_ →
IsDecStrictPartialOrder _≈±_ _<±_
<±-isDecStrictPartialOrder =
Sup.<⁺-isDecStrictPartialOrder ∘′ Inf.<₋-isDecStrictPartialOrder
<±-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_ →
IsStrictTotalOrder _≈±_ _<±_
<±-isStrictTotalOrder =
Sup.<⁺-isStrictTotalOrder ∘′ Inf.<₋-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