{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Structures
using (IsStrictPartialOrder; IsDecStrictPartialOrder; IsStrictTotalOrder)
open import Relation.Binary.Definitions
using (Asymmetric; Transitive; Decidable; Irrelevant; Irreflexive; Trans; Trichotomous; tri≈; tri>; tri<; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
module Relation.Binary.Construct.Add.Supremum.Strict
{a r} {A : Set a} (_<_ : Rel A r) where
open import Level using (_⊔_)
open import Data.Product.Base using (_,_; map)
open import Function.Base
open import Relation.Nullary hiding (Irrelevant)
import Relation.Nullary.Decidable as Dec
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; subst)
import Relation.Binary.PropositionalEquality.Properties as ≡
open import Relation.Nullary.Construct.Add.Supremum
import Relation.Binary.Construct.Add.Supremum.Equality as Equality
import Relation.Binary.Construct.Add.Supremum.NonStrict as NonStrict
infix 4 _<⁺_
data _<⁺_ : Rel (A ⁺) (a ⊔ r) where
[_] : {k l : A} → k < l → [ k ] <⁺ [ l ]
[_]<⊤⁺ : (k : A) → [ k ] <⁺ ⊤⁺
[<]-injective : ∀ {k l} → [ k ] <⁺ [ l ] → k < l
[<]-injective [ p ] = p
<⁺-asym : Asymmetric _<_ → Asymmetric _<⁺_
<⁺-asym <-asym [ p ] [ q ] = <-asym p q
<⁺-trans : Transitive _<_ → Transitive _<⁺_
<⁺-trans <-trans [ p ] [ q ] = [ <-trans p q ]
<⁺-trans <-trans [ p ] [ k ]<⊤⁺ = [ _ ]<⊤⁺
<⁺-dec : Decidable _<_ → Decidable _<⁺_
<⁺-dec _<?_ [ k ] [ l ] = Dec.map′ [_] [<]-injective (k <? l)
<⁺-dec _<?_ [ k ] ⊤⁺ = yes [ k ]<⊤⁺
<⁺-dec _<?_ ⊤⁺ [ l ] = no (λ ())
<⁺-dec _<?_ ⊤⁺ ⊤⁺ = no (λ ())
<⁺-irrelevant : Irrelevant _<_ → Irrelevant _<⁺_
<⁺-irrelevant <-irr [ p ] [ q ] = cong _ (<-irr p q)
<⁺-irrelevant <-irr [ k ]<⊤⁺ [ k ]<⊤⁺ = refl
module _ {r} {_≤_ : Rel A r} where
open NonStrict _≤_
<⁺-transʳ : Trans _≤_ _<_ _<_ → Trans _≤⁺_ _<⁺_ _<⁺_
<⁺-transʳ <-transʳ [ p ] [ q ] = [ <-transʳ p q ]
<⁺-transʳ <-transʳ [ p ] [ k ]<⊤⁺ = [ _ ]<⊤⁺
<⁺-transˡ : Trans _<_ _≤_ _<_ → Trans _<⁺_ _≤⁺_ _<⁺_
<⁺-transˡ <-transˡ [ p ] [ q ] = [ <-transˡ p q ]
<⁺-transˡ <-transˡ [ p ] ([ _ ] ≤⊤⁺) = [ _ ]<⊤⁺
<⁺-transˡ <-transˡ [ k ]<⊤⁺ (⊤⁺ ≤⊤⁺) = [ k ]<⊤⁺
<⁺-cmp-≡ : Trichotomous _≡_ _<_ → Trichotomous _≡_ _<⁺_
<⁺-cmp-≡ <-cmp ⊤⁺ ⊤⁺ = tri≈ (λ ()) refl (λ ())
<⁺-cmp-≡ <-cmp ⊤⁺ [ l ] = tri> (λ ()) (λ ()) [ l ]<⊤⁺
<⁺-cmp-≡ <-cmp [ k ] ⊤⁺ = tri< [ k ]<⊤⁺ (λ ()) (λ ())
<⁺-cmp-≡ <-cmp [ k ] [ l ] with <-cmp k l
... | tri< a ¬b ¬c = tri< [ a ] (¬b ∘ []-injective) (¬c ∘ [<]-injective)
... | tri≈ ¬a refl ¬c = tri≈ (¬a ∘ [<]-injective) refl (¬c ∘ [<]-injective)
... | tri> ¬a ¬b c = tri> (¬a ∘ [<]-injective) (¬b ∘ []-injective) [ c ]
<⁺-irrefl-≡ : Irreflexive _≡_ _<_ → Irreflexive _≡_ _<⁺_
<⁺-irrefl-≡ <-irrefl refl [ x ] = <-irrefl refl x
<⁺-respˡ-≡ : _<⁺_ Respectsˡ _≡_
<⁺-respˡ-≡ = subst (_<⁺ _)
<⁺-respʳ-≡ : _<⁺_ Respectsʳ _≡_
<⁺-respʳ-≡ = subst (_ <⁺_)
<⁺-resp-≡ : _<⁺_ Respects₂ _≡_
<⁺-resp-≡ = <⁺-respʳ-≡ , <⁺-respˡ-≡
module _ {e} {_≈_ : Rel A e} where
open Equality _≈_
<⁺-cmp : Trichotomous _≈_ _<_ → Trichotomous _≈⁺_ _<⁺_
<⁺-cmp <-cmp ⊤⁺ ⊤⁺ = tri≈ (λ ()) ⊤⁺≈⊤⁺ (λ ())
<⁺-cmp <-cmp ⊤⁺ [ l ] = tri> (λ ()) (λ ()) [ l ]<⊤⁺
<⁺-cmp <-cmp [ k ] ⊤⁺ = tri< [ k ]<⊤⁺ (λ ()) (λ ())
<⁺-cmp <-cmp [ k ] [ l ] with <-cmp k l
... | tri< a ¬b ¬c = tri< [ a ] (¬b ∘ [≈]-injective) (¬c ∘ [<]-injective)
... | tri≈ ¬a b ¬c = tri≈ (¬a ∘ [<]-injective) [ b ] (¬c ∘ [<]-injective)
... | tri> ¬a ¬b c = tri> (¬a ∘ [<]-injective) (¬b ∘ [≈]-injective) [ c ]
<⁺-irrefl : Irreflexive _≈_ _<_ → Irreflexive _≈⁺_ _<⁺_
<⁺-irrefl <-irrefl [ p ] [ q ] = <-irrefl p q
<⁺-respˡ-≈⁺ : _<_ Respectsˡ _≈_ → _<⁺_ Respectsˡ _≈⁺_
<⁺-respˡ-≈⁺ <-respˡ-≈ [ p ] [ q ] = [ <-respˡ-≈ p q ]
<⁺-respˡ-≈⁺ <-respˡ-≈ [ p ] ([ l ]<⊤⁺) = [ _ ]<⊤⁺
<⁺-respˡ-≈⁺ <-respˡ-≈ ⊤⁺≈⊤⁺ q = q
<⁺-respʳ-≈⁺ : _<_ Respectsʳ _≈_ → _<⁺_ Respectsʳ _≈⁺_
<⁺-respʳ-≈⁺ <-respʳ-≈ [ p ] [ q ] = [ <-respʳ-≈ p q ]
<⁺-respʳ-≈⁺ <-respʳ-≈ ⊤⁺≈⊤⁺ q = q
<⁺-resp-≈⁺ : _<_ Respects₂ _≈_ → _<⁺_ Respects₂ _≈⁺_
<⁺-resp-≈⁺ = map <⁺-respʳ-≈⁺ <⁺-respˡ-≈⁺
<⁺-isStrictPartialOrder-≡ : IsStrictPartialOrder _≡_ _<_ →
IsStrictPartialOrder _≡_ _<⁺_
<⁺-isStrictPartialOrder-≡ strict = record
{ isEquivalence = ≡.isEquivalence
; irrefl = <⁺-irrefl-≡ irrefl
; trans = <⁺-trans trans
; <-resp-≈ = <⁺-resp-≡
} where open IsStrictPartialOrder strict
<⁺-isDecStrictPartialOrder-≡ : IsDecStrictPartialOrder _≡_ _<_ →
IsDecStrictPartialOrder _≡_ _<⁺_
<⁺-isDecStrictPartialOrder-≡ dectot = record
{ isStrictPartialOrder = <⁺-isStrictPartialOrder-≡ isStrictPartialOrder
; _≟_ = ≡-dec _≟_
; _<?_ = <⁺-dec _<?_
} where open IsDecStrictPartialOrder dectot
<⁺-isStrictTotalOrder-≡ : IsStrictTotalOrder _≡_ _<_ →
IsStrictTotalOrder _≡_ _<⁺_
<⁺-isStrictTotalOrder-≡ strictot = record
{ isStrictPartialOrder = <⁺-isStrictPartialOrder-≡ isStrictPartialOrder
; compare = <⁺-cmp-≡ compare
} where open IsStrictTotalOrder strictot
module _ {e} {_≈_ : Rel A e} where
open Equality _≈_
<⁺-isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_ →
IsStrictPartialOrder _≈⁺_ _<⁺_
<⁺-isStrictPartialOrder strict = record
{ isEquivalence = ≈⁺-isEquivalence isEquivalence
; irrefl = <⁺-irrefl irrefl
; trans = <⁺-trans trans
; <-resp-≈ = <⁺-resp-≈⁺ <-resp-≈
} where open IsStrictPartialOrder strict
<⁺-isDecStrictPartialOrder : IsDecStrictPartialOrder _≈_ _<_ →
IsDecStrictPartialOrder _≈⁺_ _<⁺_
<⁺-isDecStrictPartialOrder dectot = record
{ isStrictPartialOrder = <⁺-isStrictPartialOrder isStrictPartialOrder
; _≟_ = ≈⁺-dec _≟_
; _<?_ = <⁺-dec _<?_
} where open IsDecStrictPartialOrder dectot
<⁺-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_ →
IsStrictTotalOrder _≈⁺_ _<⁺_
<⁺-isStrictTotalOrder strictot = record
{ isStrictPartialOrder = <⁺-isStrictPartialOrder isStrictPartialOrder
; compare = <⁺-cmp compare
} where open IsStrictTotalOrder strictot