------------------------------------------------------------------------
-- The Agda standard library
--
-- The lifting of a 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.Strict
  {a } {A : Set a} (_<_ : Rel A ) where

open import Level
open import Function.Base using (_∘′_)

import Relation.Nullary.Construct.Add.Infimum as I
open import Relation.Nullary.Construct.Add.Extrema
open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; refl)
import Relation.Binary.Construct.Add.Infimum.Strict as AddInfimum
import Relation.Binary.Construct.Add.Supremum.Strict as AddSupremum
import Relation.Binary.Construct.Add.Extrema.Equality as Equality
import Relation.Binary.Construct.Add.Extrema.NonStrict as NonStrict
open import Relation.Binary.Definitions
  using (Asymmetric; Transitive; Decidable; Irrelevant; Trichotomous; Irreflexive; Trans; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
open import Relation.Binary.Structures
  using (IsStrictPartialOrder; IsDecStrictPartialOrder; IsStrictTotalOrder)

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

private
  module Inf = AddInfimum _<_
  module Sup = AddSupremum Inf._<₋_

open Sup using () renaming (_<⁺_ to _<±_) public

------------------------------------------------------------------------
-- Useful pattern synonyms

pattern ⊥±<[_] l = Sup.[ Inf.⊥₋<[ l ] ]
pattern [_] p    = Sup.[ Inf.[ p ] ]
pattern ⊥±<⊤±    = Sup.[ I.⊥₋ ]<⊤⁺
pattern [_]<⊤± k = Sup.[ I.[ k ] ]<⊤⁺

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

[<]-injective :  {k l}  [ k ]  [ l ]  k < l
[<]-injective = Inf.[<]-injective ∘′ Sup.[<]-injective

<±-asym : Asymmetric _<_  Asymmetric _<±_
<±-asym = Sup.<⁺-asym ∘′ Inf.<₋-asym

<±-trans : Transitive _<_  Transitive _<±_
<±-trans = Sup.<⁺-trans ∘′ Inf.<₋-trans

<±-dec : Decidable _<_  Decidable _<±_
<±-dec = Sup.<⁺-dec ∘′ Inf.<₋-dec

<±-irrelevant : Irrelevant _<_  Irrelevant _<±_
<±-irrelevant = Sup.<⁺-irrelevant ∘′ Inf.<₋-irrelevant

module _ {r} {_≤_ : Rel A r} where

  open NonStrict _≤_

  <±-transʳ : Trans _≤_ _<_ _<_  Trans _≤±_ _<±_ _<±_
  <±-transʳ = Sup.<⁺-transʳ ∘′ Inf.<₋-transʳ

  <±-transˡ : Trans _<_ _≤_ _<_  Trans _<±_ _≤±_ _<±_
  <±-transˡ = Sup.<⁺-transˡ ∘′ Inf.<₋-transˡ

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

<±-cmp-≡ : Trichotomous _≡_ _<_  Trichotomous _≡_ _<±_
<±-cmp-≡ = Sup.<⁺-cmp-≡ ∘′ Inf.<₋-cmp-≡

<±-irrefl-≡ : Irreflexive _≡_ _<_  Irreflexive _≡_ _<±_
<±-irrefl-≡ = Sup.<⁺-irrefl-≡ ∘′ Inf.<₋-irrefl-≡

<±-respˡ-≡ : _<±_ Respectsˡ _≡_
<±-respˡ-≡ = Sup.<⁺-respˡ-≡

<±-respʳ-≡ : _<±_ Respectsʳ _≡_
<±-respʳ-≡ = Sup.<⁺-respʳ-≡

<±-resp-≡ : _<±_ Respects₂ _≡_
<±-resp-≡ = Sup.<⁺-resp-≡

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

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

  open Equality _≈_

  <±-cmp : Trichotomous _≈_ _<_  Trichotomous _≈±_ _<±_
  <±-cmp = Sup.<⁺-cmp ∘′ Inf.<₋-cmp

  <±-irrefl : Irreflexive _≈_ _<_  Irreflexive _≈±_ _<±_
  <±-irrefl = Sup.<⁺-irrefl ∘′ Inf.<₋-irrefl

  <±-respˡ-≈± : _<_ Respectsˡ _≈_  _<±_ Respectsˡ _≈±_
  <±-respˡ-≈± = Sup.<⁺-respˡ-≈⁺ ∘′ Inf.<₋-respˡ-≈₋

  <±-respʳ-≈± : _<_ Respectsʳ _≈_  _<±_ Respectsʳ _≈±_
  <±-respʳ-≈± = Sup.<⁺-respʳ-≈⁺ ∘′ Inf.<₋-respʳ-≈₋

  <±-resp-≈± : _<_ Respects₂ _≈_  _<±_ Respects₂ _≈±_
  <±-resp-≈± = Sup.<⁺-resp-≈⁺ ∘′ Inf.<₋-resp-≈₋

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

<±-isStrictPartialOrder-≡ : IsStrictPartialOrder _≡_ _<_ 
                            IsStrictPartialOrder _≡_ _<±_
<±-isStrictPartialOrder-≡ =
  Sup.<⁺-isStrictPartialOrder-≡ ∘′ Inf.<₋-isStrictPartialOrder-≡

<±-isDecStrictPartialOrder-≡ : IsDecStrictPartialOrder _≡_ _<_ 
                               IsDecStrictPartialOrder _≡_ _<±_
<±-isDecStrictPartialOrder-≡ =
  Sup.<⁺-isDecStrictPartialOrder-≡ ∘′ Inf.<₋-isDecStrictPartialOrder-≡

<±-isStrictTotalOrder-≡ : IsStrictTotalOrder _≡_ _<_ 
                          IsStrictTotalOrder _≡_ _<±_
<±-isStrictTotalOrder-≡ =
  Sup.<⁺-isStrictTotalOrder-≡ ∘′ Inf.<₋-isStrictTotalOrder-≡

------------------------------------------------------------------------
-- Structures + setoid equality

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

  open Equality _≈_

  <±-isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_ 
                            IsStrictPartialOrder _≈±_ _<±_
  <±-isStrictPartialOrder =
    Sup.<⁺-isStrictPartialOrder ∘′ Inf.<₋-isStrictPartialOrder

  <±-isDecStrictPartialOrder : IsDecStrictPartialOrder _≈_ _<_ 
                               IsDecStrictPartialOrder _≈±_ _<±_
  <±-isDecStrictPartialOrder =
    Sup.<⁺-isDecStrictPartialOrder ∘′ Inf.<₋-isDecStrictPartialOrder

  <±-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_ 
                          IsStrictTotalOrder _≈±_ _<±_
  <±-isStrictTotalOrder =
    Sup.<⁺-isStrictTotalOrder ∘′ Inf.<₋-isStrictTotalOrder