    ------------------------------------------------------------------------
    -- 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.Core using (Rel; _⇒_)

    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 using (inj₁; inj₂)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
    import Relation.Binary.PropositionalEquality.Properties as ≡
      using (isEquivalence)
    import Relation.Binary.Construct.Add.Infimum.Equality as Equality
      using (_≈₋_; ⊥₋≈⊥₋; ≈₋-isEquivalence; ≈₋-isDecEquivalence; ≈₋-refl; ≈₋-dec
            ; [_])
    open import Relation.Binary.Structures
      using (IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder
            ; IsDecTotalOrder)
    open import Relation.Binary.Definitions
      using (Minimum; Transitive; Total; Decidable; Irrelevant; Antisymmetric)
    open import Relation.Nullary.Construct.Add.Infimum using (⊥₋; [_]; _₋; ≡-dec)
    open import Relation.Nullary.Decidable.Core using (yes; no; map′)
    import Relation.Nullary.Decidable.Core as Dec using (map′)

    ------------------------------------------------------------------------
    -- 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) = refl
    ≤₋-irrelevant ≤-irr [ p ]   [ q ]   = 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 ]     = 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 = ≡.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