{-# OPTIONS --safe --cubical --postfix-projections #-}

module DepthComonads.Relation.Binary where

open import DepthComonads.Level

open import DepthComonads.Function using (_∘_; flip; id)
open import DepthComonads.Inspect  using (inspect;〖_〗)

open import DepthComonads.HLevels   using (isSet)
open import DepthComonads.Path as  hiding (sym; refl)

open import DepthComonads.Bool  using (Bool; true; false; bool; false≢true)
open import DepthComonads.Empty using (; ⊥-elim; ¬_)
open import DepthComonads.Sum   using (either; inl; inr; _⊎_; is-l)

open import DepthComonads.Dec      using (Dec; yes; no; does; Dec→Stable)
open import DepthComonads.Discrete using (Discrete; Discrete→isSet)
open import DepthComonads.Stable   using (Stable)

module _ (_~_ : A  A  Type b) where
  Reflexive : Type _
  Reflexive =  {x}  x ~ x

  Transitive : Type _
  Transitive =  {x y z}  x ~ y  y ~ z  x ~ z

  Symmetric : Type _
  Symmetric =  {x y}  x ~ y  y ~ x

  Decidable : Type _
  Decidable =  x y  Dec (x ~ y)

  Antisymmetric : Type _
  Antisymmetric =  {x y}  x ~ y  y ~ x  x  y

  Connected : Type _
  Connected =  {x y}  ¬ (x ~ y)  ¬ (y ~ x)  x  y

  Asymmetric : Type _
  Asymmetric =  {x y}  x ~ y  ¬ (y ~ x)

  Irreflexive : Type _
  Irreflexive =  {x}  ¬ (x ~ x)

  Total : Type _
  Total =  x y  (x ~ y)  (y ~ x)

record Preorder {ℓ₁} (𝑆 : Type ℓ₁) ℓ₂ : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂) where
  infix 4 _≤_
  field
    _≤_ : 𝑆  𝑆  Type ℓ₂
    refl : Reflexive _≤_
    trans : Transitive _≤_

  infix 4 _≰_ _≥_ _≱_
  _≰_ _≥_ _≱_ : 𝑆  𝑆  Type ℓ₂
  x  y = ¬ (x  y)
  x  y = y  x
  x  y = ¬ (y  x)

record StrictPreorder {ℓ₁} (𝑆 : Type ℓ₁) ℓ₂ : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂) where
  infix 4 _<_
  field
    _<_ : 𝑆  𝑆  Type ℓ₂
    trans : Transitive _<_
    irrefl : Irreflexive _<_

  asym : Asymmetric _<_
  asym x<y y<x = irrefl (trans x<y y<x)

  infix 4 _≮_ _>_ _≯_
  _≮_ _>_ _≯_ : 𝑆  𝑆  Type ℓ₂
  x  y = ¬ (x < y)
  x > y = y < x
  x  y = ¬ (y < x)

record StrictPartialOrder {ℓ₁} (𝑆 : Type ℓ₁) ℓ₂ : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂) where
  field strictPreorder : StrictPreorder 𝑆 ℓ₂
  open StrictPreorder strictPreorder public
  field conn : Connected _<_

record PartialOrder {ℓ₁} (𝑆 : Type ℓ₁) ℓ₂ : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂) where
  field preorder : Preorder 𝑆 ℓ₂
  open Preorder preorder public
  field antisym : Antisymmetric _≤_

data Tri (A : Type a) (B : Type b) (C : Type c) : Type (a ℓ⊔ b ℓ⊔ c) where
  lt : (x<y : A)  Tri A B C
  eq : (x≡y : B)  Tri A B C
  gt : (x>y : C)  Tri A B C

record TotalOrder {ℓ₁} (𝑆 : Type ℓ₁) ℓ₂ ℓ₃ : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂ ℓ⊔ ℓsuc ℓ₃) where
  field
    strictPartialOrder : StrictPartialOrder 𝑆 ℓ₂
    partialOrder : PartialOrder 𝑆 ℓ₃
  open PartialOrder partialOrder renaming (trans to ≤-trans) public
  open StrictPartialOrder strictPartialOrder renaming (trans to <-trans) public

  infix 4 _<?_
  field
    _<?_ : Decidable _<_

    ≰⇒> :  {x y}  x  y  x > y
    ≮⇒≥ :  {x y}  x  y  x  y

  <⇒≤ :  {x y}  x < y  x  y
  <⇒≤ = ≮⇒≥  asym

  _<ᵇ_ : 𝑆  𝑆  Bool
  x <ᵇ y = does (x <? y)

  <⇒≱ :  {x y}  x < y  x  y
  <⇒≱ {x} {y} x<y x≥y = irrefl (subst (_< _) (antisym (<⇒≤ x<y) x≥y) x<y)

  ≤⇒≯ :  {x y}  x  y  x  y
  ≤⇒≯ {x} {y} x≤y x>y = irrefl (subst (_< _) (antisym (≮⇒≥ (asym x>y)) x≤y) x>y)

  infix 4 _≤ᵇ_ _≤?_ _≤|≥_ _≟_

  _≤?_ : Decidable _≤_
  x ≤? y with y <? x
  ... | yes y<x = no  (<⇒≱ y<x)
  ... | no  y≮x = yes (≮⇒≥ y≮x)

  _≤ᵇ_ : 𝑆  𝑆  Bool
  x ≤ᵇ y = does (x ≤? y)

  _≤|≥_ : Total _≤_
  x ≤|≥ y with x <? y
  ... | yes x<y = inl (<⇒≤ x<y)
  ... | no  x≮y = inr (≮⇒≥ x≮y)

  _≟_ : Discrete 𝑆
  x  y with x <? y | y <? x
  ... | yes x<y | _ = no  x≡y  irrefl (subst (_< _) x≡y x<y))
  ... | _ | yes y<x = no  x≡y  irrefl (subst (_ <_) x≡y y<x))
  ... | no x≮y | no y≮x = yes (conn x≮y y≮x)

  Ordering : (x y : 𝑆)  Type (ℓ₁ ℓ⊔  ℓ₂)
  Ordering x y = Tri (x < y) (x  y) (x > y)

  compare :  x y  Ordering x y
  compare x y with x <? y | y <? x
  ... | yes x<y | _ = lt x<y
  ... | no  x≮y | yes y<x = gt y<x
  ... | no  x≮y | no  y≮x = eq (conn x≮y y≮x)

  total⇒isSet : isSet 𝑆
  total⇒isSet = Discrete→isSet _≟_

  data _≲_ (x y : 𝑆) : Type (ℓ₁ ℓ⊔ ℓ₂ ℓ⊔ ℓ₃) where
    <[_] : (x<y : x < y)  x  y
    ≤[_] : (x≤y : x  y)  x  y
    ≡[_] : (x≡y : x  y)  x  y

  Ordℓ :  {x y}  x  y  Level
  Ordℓ <[ _ ] = ℓ₂
  Ordℓ ≤[ _ ] = ℓ₃
  Ordℓ ≡[ _ ] = ℓ₁

  TheOrd :  {x y}  (x≲y : x  y)  Type (Ordℓ x≲y)
  TheOrd {x} {y} <[ _ ] = x < y
  TheOrd {x} {y} ≤[ _ ] = x  y
  TheOrd {x} {y} ≡[ _ ] = x  y

  ≲[_] :  {x y}  (x≲y : x  y)  TheOrd x≲y
  ≲[ <[ x<y ] ] = x<y
  ≲[ ≤[ x≤y ] ] = x≤y
  ≲[ ≡[ x≡y ] ] = x≡y

  ≱[_] :  {x y}  x  y  x  y
  ≱[ x≱y ] = <[ ≰⇒> x≱y ]

  ≯[_] :  {x y}  x  y  x  y
  ≯[ x≯y ] = ≤[ ≮⇒≥ x≯y ]

  infixr 2 _≲;_

  _≲;_ :  {x y z}  x  y  y  z  x  z
  <[ x≲y ] ≲; <[ y≲z ] = <[ <-trans x≲y y≲z ]
  <[ x≲y ] ≲; ≡[ y≲z ] = <[ subst (_ <_) y≲z x≲y ]
  ≡[ x≲y ] ≲; <[ y≲z ] = <[ subst (_< _) (≡.sym x≲y) y≲z ]
  ≡[ x≲y ] ≲; ≡[ y≲z ] = ≡[ x≲y ; y≲z ]
  ≡[ x≲y ] ≲; ≤[ y≲z ] = ≤[ subst (_≤ _) (≡.sym x≲y) y≲z ]
  ≤[ x≲y ] ≲; ≤[ y≲z ] = ≤[ ≤-trans x≲y y≲z ]
  ≤[ x≲y ] ≲; ≡[ y≲z ] = ≤[ subst (_ ≤_) y≲z x≲y ]
  ≤[ x≲y ] ≲; <[ y≲z ] = ≱[  z≤x  <⇒≱ y≲z (≤-trans z≤x x≲y)) ]
  <[ x≲y ] ≲; ≤[ y≲z ] = ≱[  z≤x  <⇒≱ x≲y (≤-trans y≲z z≤x)) ]

  module Reasoning where

    infixr 2 ≤⟨∙⟩-syntax <⟨∙⟩-syntax ≡⟨∙⟩-syntax ≡˘⟨∙⟩-syntax _≡⟨⟩_ ≱⟨∙⟩-syntax ≯⟨∙⟩-syntax

    ≤⟨∙⟩-syntax :  (x : 𝑆) {y z}  y  z  x  y  x  z
    ≤⟨∙⟩-syntax _ y≲z x≤y = ≤[ x≤y ] ≲; y≲z

    syntax ≤⟨∙⟩-syntax x y≲z x≤y = x ≤⟨ x≤y  y≲z

    ≱⟨∙⟩-syntax :  (x : 𝑆) {y z}  y  z  x  y  x  z
    ≱⟨∙⟩-syntax _ y≲z x≱y = ≱[ x≱y ] ≲; y≲z

    syntax ≱⟨∙⟩-syntax x y≲z x≱y = x ≱⟨ x≱y  y≲z

    <⟨∙⟩-syntax :  (x : 𝑆) {y z}  y  z  x < y  x  z
    <⟨∙⟩-syntax _ y≲z x<y = <[ x<y ] ≲; y≲z

    syntax <⟨∙⟩-syntax x y≲z x<y = x <⟨ x<y  y≲z

    ≯⟨∙⟩-syntax :  (x : 𝑆) {y z}  y  z  x  y  x  z
    ≯⟨∙⟩-syntax _ y≲z x≯y = ≯[ x≯y ] ≲; y≲z

    syntax ≯⟨∙⟩-syntax x y≲z x≯y = x ≯⟨ x≯y  y≲z

    ≡⟨∙⟩-syntax :  (x : 𝑆) {y z}  y  z  x  y  x  z
    ≡⟨∙⟩-syntax _ y≲z x≡y = ≡[ x≡y ] ≲; y≲z

    syntax ≡⟨∙⟩-syntax x y≲z x≡y = x ≡⟨ x≡y  y≲z

    ≡˘⟨∙⟩-syntax :  (x : 𝑆) {y z}  y  z  y  x  x  z
    ≡˘⟨∙⟩-syntax _ y≲z y≡x = ≡[ ≡.sym y≡x ] ≲; y≲z

    syntax ≡˘⟨∙⟩-syntax x y≲z y≡x = x ≡˘⟨ y≡x  y≲z

    _≡⟨⟩_ :  (x : 𝑆) {y}  x  y  x  y
    _ ≡⟨⟩ x≲y = x≲y

    infix 2.5 _∎
    _∎ :  x  x  x
    x  = ≡[ ≡.refl ]

    infixr 2 begin_
    begin_ = ≲[_]

    _ :  w x y z  w < x  x  y  y  z  w < z
    _ = λ w x y z w<x x≡y y≤z  begin
      w <⟨ w<x 
      x ≡⟨ x≡y 
      y ≤⟨ y≤z 
      z 

module FromPartialOrder {ℓ₁} {𝑆 : Type ℓ₁} {ℓ₂} (po : PartialOrder 𝑆 ℓ₂) (_≤|≥_ : Total (PartialOrder._≤_ po)) where
  open PartialOrder po

  partialOrder = po

  ≤-side : 𝑆  𝑆  Bool
  ≤-side x y = is-l (x ≤|≥ y)

  ≤-dec : Decidable _≤_
  ≤-dec x y with x ≤|≥ y | y ≤|≥ x | inspect (≤-side x) y | inspect (≤-side y) x
  ≤-dec x y | inl x≤y | _       | _ | _ = yes x≤y
  ≤-dec x y | inr x≥y | inr y≥x | _ | _ = yes y≥x
  ≤-dec x y | inr x≥y | inl y≤x |  x≥yᵇ  |  y≤xᵇ  = no (x≢y  flip antisym x≥y)
    where
    x≢y : x  y
    x≢y x≡y = false≢true (≡.sym x≥yᵇ ; cong₂ ≤-side x≡y (≡.sym x≡y) ; y≤xᵇ)

  ≮⇒≥ :  {x y}  Stable (x  y)
  ≮⇒≥ {x} {y} = Dec→Stable (≤-dec x y)

  strictPartialOrder : StrictPartialOrder 𝑆 ℓ₂
  strictPartialOrder .StrictPartialOrder.strictPreorder .StrictPreorder._<_ x y = ¬ (y  x)
  strictPartialOrder .StrictPartialOrder.conn x<y y<x = antisym (≮⇒≥ y<x) (≮⇒≥ x<y)
  strictPartialOrder .StrictPartialOrder.strictPreorder .StrictPreorder.irrefl y≰x = y≰x refl
  strictPartialOrder .StrictPartialOrder.strictPreorder .StrictPreorder.trans {x} {y} {z} y≰x z≰y z≤x with ≤-dec y z
  ... | yes y≤z = y≰x (trans y≤z z≤x)
  ... | no  y≰z = either z≰y y≰z (z ≤|≥ y)

  ≰⇒> = id

  _<?_ : Decidable _≱_
  _<?_ x y with ≤-dec y x
  ... | yes y≤x = no λ y≰x  y≰x y≤x
  ... | no  y≰x = yes y≰x

fromPartialOrder : (po : PartialOrder A b) (_≤|≥_ : Total (PartialOrder._≤_ po))  TotalOrder _ _ _
fromPartialOrder po tot = record { FromPartialOrder po tot }

module FromStrictPartialOrder {ℓ₁} {𝑆 : Type ℓ₁} {ℓ₂} (spo : StrictPartialOrder 𝑆 ℓ₂) (<-dec : Decidable (StrictPartialOrder._<_ spo)) where
  open StrictPartialOrder spo
  strictPartialOrder = spo
  _<?_ = <-dec

  partialOrder : PartialOrder _ _
  partialOrder .PartialOrder.preorder .Preorder._≤_ x y = ¬ (y < x)
  partialOrder .PartialOrder.preorder .Preorder.refl x<x = asym x<x x<x
  partialOrder .PartialOrder.preorder .Preorder.trans {x} {y} {z} y≮x z≮y z<x with x <? y
  ... | yes x<y = z≮y (trans z<x x<y)
  ... | no  x≮y = z≮y (subst (z <_) (conn x≮y y≮x) z<x)
  partialOrder .PartialOrder.antisym = flip conn

  ≰⇒> :  {x y}  Stable (x < y)
  ≰⇒> {x} {y} = Dec→Stable (x <? y)

  ≮⇒≥ = id

fromStrictPartialOrder : (spo : StrictPartialOrder A b) (_<?_ : Decidable (StrictPartialOrder._<_ spo))  TotalOrder _ _ _
fromStrictPartialOrder spo _<?_ = record { FromStrictPartialOrder spo _<?_ }

record Equivalence {ℓ₁} (𝑆 : Type ℓ₁) ℓ₂ : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂) where
  infix 4 _≋_
  field
    _≋_ : 𝑆  𝑆  Type ℓ₂
    sym   :  {x y}  x  y  y  x
    refl  :  {x}  x  x
    trans :  {x y z}  x  y  y  z  x  z

≡-equivalence :  {a} {A : Type a}  Equivalence A a
≡-equivalence = record
  { _≋_ = _≡_
  ; sym = ≡.sym
  ; refl = ≡.refl
  ; trans = _;_
  }