------------------------------------------------------------------------
-- The Agda standard library
--
-- The lifting of a non-strict order to incorporate a new supremum
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
-- This module is designed to be used with
-- Relation.Nullary.Construct.Add.Supremum
open import Relation.Binary.Core using (Rel; _⇒_)
module Relation.Binary.Construct.Add.Supremum.NonStrict
{a ℓ} {A : Set a} (_≤_ : Rel A ℓ) where
open import Level using (_⊔_)
open import Data.Sum.Base as Sum
open import Relation.Binary.Structures
using (IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder; IsDecTotalOrder)
open import Relation.Binary.Definitions
using (Maximum; Transitive; Total; Decidable; Irrelevant; Antisymmetric)
import Relation.Nullary.Decidable.Core as Dec using (map′)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; refl; cong)
import Relation.Binary.PropositionalEquality.Properties as ≡
open import Relation.Nullary.Negation.Core using (¬_)
open import Relation.Nullary.Decidable.Core using (yes; no)
open import Relation.Nullary.Construct.Add.Supremum using (⊤⁺; _⁺; [_]; ≡-dec)
import Relation.Binary.Construct.Add.Supremum.Equality as Equality
------------------------------------------------------------------------
-- Definition
infix 4 _≤⁺_ _≤⊤⁺
data _≤⁺_ : Rel (A ⁺) (a ⊔ ℓ) where
[_] : {k l : A} → k ≤ l → [ k ] ≤⁺ [ l ]
_≤⊤⁺ : (k : A ⁺) → k ≤⁺ ⊤⁺
------------------------------------------------------------------------
-- Properties
[≤]-injective : ∀ {k l} → [ k ] ≤⁺ [ l ] → k ≤ l
[≤]-injective [ p ] = p
≤⁺-trans : Transitive _≤_ → Transitive _≤⁺_
≤⁺-trans ≤-trans [ p ] [ q ] = [ ≤-trans p q ]
≤⁺-trans ≤-trans p (l ≤⊤⁺) = _ ≤⊤⁺
≤⁺-maximum : Maximum _≤⁺_ ⊤⁺
≤⁺-maximum = _≤⊤⁺
≤⁺-dec : Decidable _≤_ → Decidable _≤⁺_
≤⁺-dec _≤?_ k ⊤⁺ = yes (k ≤⊤⁺)
≤⁺-dec _≤?_ ⊤⁺ [ l ] = no (λ ())
≤⁺-dec _≤?_ [ k ] [ l ] = Dec.map′ [_] [≤]-injective (k ≤? l)
≤⁺-total : Total _≤_ → Total _≤⁺_
≤⁺-total ≤-total k ⊤⁺ = inj₁ (k ≤⊤⁺)
≤⁺-total ≤-total ⊤⁺ l = inj₂ (l ≤⊤⁺)
≤⁺-total ≤-total [ k ] [ l ] = Sum.map [_] [_] (≤-total k l)
≤⁺-irrelevant : Irrelevant _≤_ → Irrelevant _≤⁺_
≤⁺-irrelevant ≤-irr [ p ] [ q ] = cong _ (≤-irr p q)
≤⁺-irrelevant ≤-irr (k ≤⊤⁺) (k ≤⊤⁺) = refl
------------------------------------------------------------------------
-- Relational properties + propositional equality
≤⁺-reflexive-≡ : (_≡_ ⇒ _≤_) → (_≡_ ⇒ _≤⁺_)
≤⁺-reflexive-≡ ≤-reflexive {[ x ]} refl = [ ≤-reflexive refl ]
≤⁺-reflexive-≡ ≤-reflexive {⊤⁺} refl = ⊤⁺ ≤⊤⁺
≤⁺-antisym-≡ : Antisymmetric _≡_ _≤_ → Antisymmetric _≡_ _≤⁺_
≤⁺-antisym-≡ antisym (_ ≤⊤⁺) (_ ≤⊤⁺) = refl
≤⁺-antisym-≡ antisym [ p ] [ q ] = cong [_] (antisym p q)
------------------------------------------------------------------------
-- Relation properties + setoid equality
module _ {e} {_≈_ : Rel A e} where
open Equality _≈_
≤⁺-reflexive : (_≈_ ⇒ _≤_) → (_≈⁺_ ⇒ _≤⁺_)
≤⁺-reflexive ≤-reflexive [ p ] = [ ≤-reflexive p ]
≤⁺-reflexive ≤-reflexive ⊤⁺≈⊤⁺ = ⊤⁺ ≤⊤⁺
≤⁺-antisym : Antisymmetric _≈_ _≤_ → Antisymmetric _≈⁺_ _≤⁺_
≤⁺-antisym ≤-antisym [ p ] [ q ] = [ ≤-antisym p q ]
≤⁺-antisym ≤-antisym (_ ≤⊤⁺) (_ ≤⊤⁺) = ⊤⁺≈⊤⁺
------------------------------------------------------------------------
-- Structures + propositional equality
≤⁺-isPreorder-≡ : IsPreorder _≡_ _≤_ → IsPreorder _≡_ _≤⁺_
≤⁺-isPreorder-≡ ≤-isPreorder = record
{ isEquivalence = ≡.isEquivalence
; reflexive = ≤⁺-reflexive-≡ reflexive
; trans = ≤⁺-trans trans
} where open IsPreorder ≤-isPreorder
≤⁺-isPartialOrder-≡ : IsPartialOrder _≡_ _≤_ → IsPartialOrder _≡_ _≤⁺_
≤⁺-isPartialOrder-≡ ≤-isPartialOrder = record
{ isPreorder = ≤⁺-isPreorder-≡ isPreorder
; antisym = ≤⁺-antisym-≡ antisym
} where open IsPartialOrder ≤-isPartialOrder
≤⁺-isDecPartialOrder-≡ : IsDecPartialOrder _≡_ _≤_ → IsDecPartialOrder _≡_ _≤⁺_
≤⁺-isDecPartialOrder-≡ ≤-isDecPartialOrder = record
{ isPartialOrder = ≤⁺-isPartialOrder-≡ isPartialOrder
; _≟_ = ≡-dec _≟_
; _≤?_ = ≤⁺-dec _≤?_
} where open IsDecPartialOrder ≤-isDecPartialOrder
≤⁺-isTotalOrder-≡ : IsTotalOrder _≡_ _≤_ → IsTotalOrder _≡_ _≤⁺_
≤⁺-isTotalOrder-≡ ≤-isTotalOrder = record
{ isPartialOrder = ≤⁺-isPartialOrder-≡ isPartialOrder
; total = ≤⁺-total total
} where open IsTotalOrder ≤-isTotalOrder
≤⁺-isDecTotalOrder-≡ : IsDecTotalOrder _≡_ _≤_ → IsDecTotalOrder _≡_ _≤⁺_
≤⁺-isDecTotalOrder-≡ ≤-isDecTotalOrder = record
{ isTotalOrder = ≤⁺-isTotalOrder-≡ isTotalOrder
; _≟_ = ≡-dec _≟_
; _≤?_ = ≤⁺-dec _≤?_
} where open IsDecTotalOrder ≤-isDecTotalOrder
------------------------------------------------------------------------
-- Structures + setoid equality
module _ {e} {_≈_ : Rel A e} where
open Equality _≈_
≤⁺-isPreorder : IsPreorder _≈_ _≤_ → IsPreorder _≈⁺_ _≤⁺_
≤⁺-isPreorder ≤-isPreorder = record
{ isEquivalence = ≈⁺-isEquivalence isEquivalence
; reflexive = ≤⁺-reflexive reflexive
; trans = ≤⁺-trans trans
} where open IsPreorder ≤-isPreorder
≤⁺-isPartialOrder : IsPartialOrder _≈_ _≤_ → IsPartialOrder _≈⁺_ _≤⁺_
≤⁺-isPartialOrder ≤-isPartialOrder = record
{ isPreorder = ≤⁺-isPreorder isPreorder
; antisym = ≤⁺-antisym antisym
} where open IsPartialOrder ≤-isPartialOrder
≤⁺-isDecPartialOrder : IsDecPartialOrder _≈_ _≤_ → IsDecPartialOrder _≈⁺_ _≤⁺_
≤⁺-isDecPartialOrder ≤-isDecPartialOrder = record
{ isPartialOrder = ≤⁺-isPartialOrder isPartialOrder
; _≟_ = ≈⁺-dec _≟_
; _≤?_ = ≤⁺-dec _≤?_
} where open IsDecPartialOrder ≤-isDecPartialOrder
≤⁺-isTotalOrder : IsTotalOrder _≈_ _≤_ → IsTotalOrder _≈⁺_ _≤⁺_
≤⁺-isTotalOrder ≤-isTotalOrder = record
{ isPartialOrder = ≤⁺-isPartialOrder isPartialOrder
; total = ≤⁺-total total
} where open IsTotalOrder ≤-isTotalOrder
≤⁺-isDecTotalOrder : IsDecTotalOrder _≈_ _≤_ → IsDecTotalOrder _≈⁺_ _≤⁺_
≤⁺-isDecTotalOrder ≤-isDecTotalOrder = record
{ isTotalOrder = ≤⁺-isTotalOrder isTotalOrder
; _≟_ = ≈⁺-dec _≟_
; _≤?_ = ≤⁺-dec _≤?_
} where open IsDecTotalOrder ≤-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