------------------------------------------------------------------------
-- The Agda standard library
--
-- The lifting of a non-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.NonStrict
{a ℓ} {A : Set a} (_≤_ : Rel A ℓ) where
open import Function.Base
open import Relation.Binary.Structures
using (IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder
; IsDecTotalOrder)
open import Relation.Binary.Definitions
using (Decidable; Transitive; Minimum; Maximum; Total; Irrelevant
; Antisymmetric)
open import Relation.Nullary.Construct.Add.Extrema using (⊥±; ⊤±; [_])
import Relation.Nullary.Construct.Add.Infimum as I using (⊥₋; [_])
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
import Relation.Binary.Construct.Add.Infimum.NonStrict as AddInfimum
import Relation.Binary.Construct.Add.Supremum.NonStrict as AddSupremum
import Relation.Binary.Construct.Add.Extrema.Equality as Equality
------------------------------------------------------------------------
-- Definition
private
module Inf = AddInfimum _≤_
module Sup = AddSupremum Inf._≤₋_
open Sup using () renaming (_≤⁺_ to _≤±_) public
------------------------------------------------------------------------
-- Useful pattern synonyms
pattern ⊥±≤⊥± = Sup.[ Inf.⊥₋≤ I.⊥₋ ]
pattern ⊥±≤[_] l = Sup.[ Inf.⊥₋≤ I.[ l ] ]
pattern [_] p = Sup.[ Inf.[ p ] ]
pattern ⊥±≤⊤± = ⊥± Sup.≤⊤⁺
pattern [_]≤⊤± k = [ k ] Sup.≤⊤⁺
pattern ⊤±≤⊤± = ⊤± Sup.≤⊤⁺
⊥±≤_ : ∀ k → ⊥± ≤± k
⊥±≤ ⊥± = ⊥±≤⊥±
⊥±≤ [ k ] = ⊥±≤[ k ]
⊥±≤ ⊤± = ⊥±≤⊤±
_≤⊤± : ∀ k → k ≤± ⊤±
⊥± ≤⊤± = ⊥±≤⊤±
[ k ] ≤⊤± = [ k ]≤⊤±
⊤± ≤⊤± = ⊤±≤⊤±
------------------------------------------------------------------------
-- Relational properties
[≤]-injective : ∀ {k l} → [ k ] ≤± [ l ] → k ≤ l
[≤]-injective = Inf.[≤]-injective ∘′ Sup.[≤]-injective
≤±-trans : Transitive _≤_ → Transitive _≤±_
≤±-trans = Sup.≤⁺-trans ∘′ Inf.≤₋-trans
≤±-minimum : Minimum _≤±_ ⊥±
≤±-minimum = ⊥±≤_
≤±-maximum : Maximum _≤±_ ⊤±
≤±-maximum = _≤⊤±
≤±-dec : Decidable _≤_ → Decidable _≤±_
≤±-dec = Sup.≤⁺-dec ∘′ Inf.≤₋-dec
≤±-total : Total _≤_ → Total _≤±_
≤±-total = Sup.≤⁺-total ∘′ Inf.≤₋-total
≤±-irrelevant : Irrelevant _≤_ → Irrelevant _≤±_
≤±-irrelevant = Sup.≤⁺-irrelevant ∘′ Inf.≤₋-irrelevant
------------------------------------------------------------------------
-- Relational properties + propositional equality
≤±-reflexive-≡ : (_≡_ ⇒ _≤_) → (_≡_ ⇒ _≤±_)
≤±-reflexive-≡ = Sup.≤⁺-reflexive-≡ ∘′ Inf.≤₋-reflexive-≡
≤±-antisym-≡ : Antisymmetric _≡_ _≤_ → Antisymmetric _≡_ _≤±_
≤±-antisym-≡ = Sup.≤⁺-antisym-≡ ∘′ Inf.≤₋-antisym-≡
------------------------------------------------------------------------
-- Relational properties + setoid equality
module _ {e} {_≈_ : Rel A e} where
open Equality _≈_
≤±-reflexive : (_≈_ ⇒ _≤_) → (_≈±_ ⇒ _≤±_)
≤±-reflexive = Sup.≤⁺-reflexive ∘′ Inf.≤₋-reflexive
≤±-antisym : Antisymmetric _≈_ _≤_ → Antisymmetric _≈±_ _≤±_
≤±-antisym = Sup.≤⁺-antisym ∘′ Inf.≤₋-antisym
------------------------------------------------------------------------
-- Structures + propositional equality
≤±-isPreorder-≡ : IsPreorder _≡_ _≤_ → IsPreorder _≡_ _≤±_
≤±-isPreorder-≡ = Sup.≤⁺-isPreorder-≡ ∘′ Inf.≤₋-isPreorder-≡
≤±-isPartialOrder-≡ : IsPartialOrder _≡_ _≤_ → IsPartialOrder _≡_ _≤±_
≤±-isPartialOrder-≡ = Sup.≤⁺-isPartialOrder-≡ ∘′ Inf.≤₋-isPartialOrder-≡
≤±-isDecPartialOrder-≡ : IsDecPartialOrder _≡_ _≤_ → IsDecPartialOrder _≡_ _≤±_
≤±-isDecPartialOrder-≡ = Sup.≤⁺-isDecPartialOrder-≡ ∘′ Inf.≤₋-isDecPartialOrder-≡
≤±-isTotalOrder-≡ : IsTotalOrder _≡_ _≤_ → IsTotalOrder _≡_ _≤±_
≤±-isTotalOrder-≡ = Sup.≤⁺-isTotalOrder-≡ ∘′ Inf.≤₋-isTotalOrder-≡
≤±-isDecTotalOrder-≡ : IsDecTotalOrder _≡_ _≤_ → IsDecTotalOrder _≡_ _≤±_
≤±-isDecTotalOrder-≡ = Sup.≤⁺-isDecTotalOrder-≡ ∘′ Inf.≤₋-isDecTotalOrder-≡
------------------------------------------------------------------------
-- Structures + setoid equality
module _ {e} {_≈_ : Rel A e} where
open Equality _≈_
≤±-isPreorder : IsPreorder _≈_ _≤_ → IsPreorder _≈±_ _≤±_
≤±-isPreorder = Sup.≤⁺-isPreorder ∘′ Inf.≤₋-isPreorder
≤±-isPartialOrder : IsPartialOrder _≈_ _≤_ → IsPartialOrder _≈±_ _≤±_
≤±-isPartialOrder = Sup.≤⁺-isPartialOrder ∘′ Inf.≤₋-isPartialOrder
≤±-isDecPartialOrder : IsDecPartialOrder _≈_ _≤_ → IsDecPartialOrder _≈±_ _≤±_
≤±-isDecPartialOrder = Sup.≤⁺-isDecPartialOrder ∘′ Inf.≤₋-isDecPartialOrder
≤±-isTotalOrder : IsTotalOrder _≈_ _≤_ → IsTotalOrder _≈±_ _≤±_
≤±-isTotalOrder = Sup.≤⁺-isTotalOrder ∘′ Inf.≤₋-isTotalOrder
≤±-isDecTotalOrder : IsDecTotalOrder _≈_ _≤_ → IsDecTotalOrder _≈±_ _≤±_
≤±-isDecTotalOrder = Sup.≤⁺-isDecTotalOrder ∘′ Inf.≤₋-isDecTotalOrder
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