------------------------------------------------------------------------
-- 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  _≤₋_
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