Source code on Github
------------------------------------------------------------------------
-- The Agda standard library
--
-- The lifting of a non-strict order to incorporate a new infimum
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

-- This module is designed to be used with
-- Relation.Nullary.Construct.Add.Infimum

open import Relation.Binary

module Relation.Binary.Construct.Add.Infimum.NonStrict
  {a } {A : Set a} (_≤_ : Rel A ) where

open import Level using (_⊔_)
open import Data.Sum.Base as Sum
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl)
import Relation.Binary.Construct.Add.Infimum.Equality as Equality
open import Relation.Nullary hiding (Irrelevant)
open import Relation.Nullary.Construct.Add.Infimum
import Relation.Nullary.Decidable as Dec

------------------------------------------------------------------------
-- Definition

infix 5 _≤₋_
data _≤₋_ : Rel (A ) (a  ) where
  ⊥₋≤_  : (l : A )          ⊥₋    ≤₋ l
  [_] : {k l : A}  k  l  [ k ] ≤₋ [ l ]

------------------------------------------------------------------------
-- Relational properties

[≤]-injective :  {k l}  [ k ] ≤₋ [ l ]  k  l
[≤]-injective [ p ] = p

≤₋-trans : Transitive _≤_  Transitive _≤₋_
≤₋-trans ≤-trans (⊥₋≤ l) q     = ⊥₋≤ _
≤₋-trans ≤-trans [ p ]   [ q ] = [ ≤-trans p q ]

≤₋-minimum : Minimum _≤₋_ ⊥₋
≤₋-minimum = ⊥₋≤_

≤₋-dec : Decidable _≤_  Decidable _≤₋_
≤₋-dec _≤?_ ⊥₋    l     = yes (⊥₋≤ l)
≤₋-dec _≤?_ [ k ] ⊥₋    = no  ())
≤₋-dec _≤?_ [ k ] [ l ] = Dec.map′ [_] [≤]-injective (k ≤? l)

≤₋-total : Total _≤_  Total _≤₋_
≤₋-total ≤-total ⊥₋    l     = inj₁ (⊥₋≤ l)
≤₋-total ≤-total k     ⊥₋    = inj₂ (⊥₋≤ k)
≤₋-total ≤-total [ k ] [ l ] = Sum.map [_] [_] (≤-total k l)

≤₋-irrelevant : Irrelevant _≤_  Irrelevant _≤₋_
≤₋-irrelevant ≤-irr (⊥₋≤ k) (⊥₋≤ k) = P.refl
≤₋-irrelevant ≤-irr [ p ]   [ q ]   = P.cong _ (≤-irr p q)

------------------------------------------------------------------------
-- Relational properties + propositional equality

≤₋-reflexive-≡ : (_≡_  _≤_)  (_≡_  _≤₋_)
≤₋-reflexive-≡ ≤-reflexive {[ x ]} refl = [ ≤-reflexive refl ]
≤₋-reflexive-≡ ≤-reflexive {⊥₋}    refl = ⊥₋≤ ⊥₋

≤₋-antisym-≡ : Antisymmetric _≡_ _≤_  Antisymmetric _≡_ _≤₋_
≤₋-antisym-≡ antisym (⊥₋≤ _) (⊥₋≤ _) = refl
≤₋-antisym-≡ antisym [ p ] [ q ]       = P.cong [_] (antisym p q)

------------------------------------------------------------------------
-- Relational properties + setoid equality

module _ {e} {_≈_ : Rel A e} where

  open Equality _≈_

  ≤₋-reflexive : (_≈_  _≤_)  (_≈₋_  _≤₋_)
  ≤₋-reflexive ≤-reflexive ⊥₋≈⊥₋ = ⊥₋≤ ⊥₋
  ≤₋-reflexive ≤-reflexive [ p ] = [ ≤-reflexive p ]

  ≤₋-antisym : Antisymmetric _≈_ _≤_  Antisymmetric _≈₋_ _≤₋_
  ≤₋-antisym ≤≥⇒≈ (⊥₋≤ _) (⊥₋≤ _) = ⊥₋≈⊥₋
  ≤₋-antisym ≤≥⇒≈ [ p ] [ q ] = [ ≤≥⇒≈ p q ]

------------------------------------------------------------------------
-- Structures + propositional equality

≤₋-isPreorder-≡ : IsPreorder _≡_ _≤_  IsPreorder _≡_ _≤₋_
≤₋-isPreorder-≡ ≤-isPreorder = record
  { isEquivalence = P.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