{-# OPTIONS --postfix-projections --safe --without-K --no-exact-split #-}

open import Level
open import Algebra
open import Algebra.Ordered
open import Algebra.Ordered.Consequences
import Algebra.Ordered.Construction.LowerSet
open import Function using (Equivalence; const; flip)
open import Data.Product using (_×_; _,_; proj₁; proj₂; <_,_>; -,_; Σ-syntax; ; ∃-syntax)
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Unit as Unit using ()
open import Relation.Binary
open import Relation.Binary.Construct.Core.Symmetric as SymCore using (SymCore)
open import Relation.Binary.Lattice
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
import Relation.Binary.Construct.Flip.EqAndOrd as Flip
open import Relation.Unary using (Pred; _⊆_)
import Relation.Binary.Reasoning.PartialOrder as PosetReasoning
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

module Algebra.Ordered.Construction.Ideal {c ℓ₁ ℓ₂} (pomagma : Pomagma c ℓ₁ ℓ₂) where

private
  module C = Pomagma pomagma

open C 
  using
    ( Carrier
    ) 
  renaming
    ( _∙_ to _∨ᶜ_
    ; _≤_ to _≤ᶜ_
    ; _≈_ to _≈ᶜ_
    )

private
  module L = Algebra.Ordered.Construction.LowerSet C.poset

open L using (LowerSet)

private
  variable
    w x y z : Carrier
    ℓx ℓy ℓz : Level
    X : Pred Carrier ℓx
    Y : Pred Carrier ℓy
    Z : Pred Carrier ℓz
    F F₁ F₂ : LowerSet
    G G₁ G₂ : LowerSet
    H H₁ H₂ : LowerSet

record Ideal : Set (suc (c  ℓ₂)) where
  no-eta-equality
  field
    ICarrier : Carrier  Set (c  ℓ₂)
    ≤-closed : x ≤ᶜ y  ICarrier y  ICarrier x
    ∨-closed : ICarrier x  ICarrier y  ICarrier (x ∨ᶜ y)
open Ideal public

private
  variable
    I I₁ I₂ : Ideal
    J J₁ J₂ : Ideal
    K K₁ K₂ : Ideal

infix 4 _≤_

record _≤_ (I J : Ideal) : Set (c  ℓ₂) where
  no-eta-equality
  field
    *≤* : I .ICarrier  J .ICarrier
open _≤_ public

infix 4 _≈_

_≈_ : Ideal  Ideal  Set (c  ℓ₂)
_≈_ = SymCore _≤_

≤-refl : I  I
≤-refl .*≤* Ix = Ix

≤-trans : I  J  J  K  I  K
≤-trans I≤J J≤K .*≤* z = J≤K .*≤* (I≤J .*≤* z)

-- FIXME: get rid of the propositional equality here
≤-isPartialOrder : IsPartialOrder _≈_ _≤_
≤-isPartialOrder = SymCore.isPreorder⇒isPartialOrder _≤_ ≡-≤-isPreorder
  where
    ≡-≤-isPreorder : IsPreorder _≡_ _≤_
    ≡-≤-isPreorder = record
      { isEquivalence = PropEq.isEquivalence
      ; reflexive = λ { PropEq.refl  ≤-refl }
      ; trans = ≤-trans
      }

open IsPartialOrder ≤-isPartialOrder
  using
    ( module Eq
    )
  renaming
    ( ≤-respˡ-≈  to ≤-respˡ-≈
    ; reflexive  to ≤-reflexive
    ; isPreorder to ≤-isPreorder
    )
  public

≤-poset : Poset _ _ _
≤-poset = record
  { isPartialOrder = ≤-isPartialOrder
  }

≈-setoid : Setoid _ _
≈-setoid = record
  { isEquivalence = Poset.isEquivalence ≤-poset
  }

------------------------------------------------------------------------------
-- From ideals to lower sets
U : Ideal  LowerSet
U I .L.ICarrier = I .ICarrier
U I .L.≤-closed = I .≤-closed

U-mono : I  J  U I L.≤ U J
U-mono I≤J .L.*≤* = I≤J .*≤*

U-cong : I  J  U I L.≈ U J
U-cong (J≤I , I≤J) = U-mono J≤I , U-mono I≤J

------------------------------------------------------------------------------
-- Turn a lower set into an ideal by closing under ∨

data `⋁ (F : LowerSet) : Set (c  ℓ₂) where
  leaf : (x : Carrier)  F .L.ICarrier x  `⋁ F
  node : `⋁ F  `⋁ F  `⋁ F

`⋁-eval : `⋁ F  Carrier
`⋁-eval (leaf x _) = x
`⋁-eval (node c d) = `⋁-eval c ∨ᶜ `⋁-eval d

`⋁-map : F L.≤ G  `⋁ F  `⋁ G
`⋁-map F≤G (leaf x Fx) = leaf x (F≤G .L.*≤* Fx)
`⋁-map F≤G (node c d)  = node (`⋁-map F≤G c) (`⋁-map F≤G d)

`⋁-map-eval : (F≤G : F L.≤ G) (c : `⋁ F)  `⋁-eval c ≤ᶜ `⋁-eval (`⋁-map F≤G c)
`⋁-map-eval F≤G (leaf x Fx) = C.refl
`⋁-map-eval F≤G (node c d) = C.mono (`⋁-map-eval F≤G c) (`⋁-map-eval F≤G d)

α : LowerSet  Ideal
α F .ICarrier x = Σ[ t  `⋁ F ] (x ≤ᶜ `⋁-eval t)
α F .≤-closed x≤y (t , y≤t) = t , C.trans x≤y y≤t
α F .∨-closed (s , x≤s) (t , y≤t) = node s t , C.mono x≤s y≤t

α-mono : F L.≤ G  α F  α G
α-mono F≤G .*≤* (t , x≤t) = `⋁-map F≤G t , C.trans x≤t (`⋁-map-eval F≤G t)

α-cong :  {F G}  F L.≈ G  α F  α G
α-cong (G≤F , F≤G) = (α-mono G≤F , α-mono F≤G)

------------------------------------------------------------------------------
η : Carrier  Ideal
η x = α (L.η x)

η-mono : x ≤ᶜ y  η x  η y
η-mono x≤y = α-mono (L.η-mono x≤y)

------------------------------------------------------------------------------
-- U and α form a Galois connection

`⋁-closed : (t : `⋁ (U I))  I .ICarrier (`⋁-eval t)
`⋁-closed {I} (leaf x ϕ) = ϕ
`⋁-closed {I} (node c d) = I .∨-closed (`⋁-closed c) (`⋁-closed d)

counit : α (U I)  I
counit {I} .*≤* (t , x≤t) = I .≤-closed x≤t (`⋁-closed t)

counit⁻¹ : I  α (U I)
counit⁻¹ .*≤* Ix = leaf _ Ix , C.refl

counit-≈ : I  α (U I)
counit-≈ = counit⁻¹ , counit

unit : F L.≤ U (α F)
unit .L.*≤* Fx = leaf _ Fx , C.refl

------------------------------------------------------------------------------
-- Binary meets

_∧_ : Ideal  Ideal  Ideal
(I  J) .ICarrier x = I .ICarrier x × J .ICarrier x
(I  J) .≤-closed x≤y (Iy , Jy) = I .≤-closed x≤y Iy , J .≤-closed x≤y Jy
(I  J) .∨-closed (Ix , Jx) (Iy , Jy) = (I .∨-closed Ix Iy) , (J .∨-closed Jx Jy)

x∧y≤x : (I  J)  I
x∧y≤x .*≤* = proj₁

x∧y≤y : (I  J)  J
x∧y≤y .*≤* = proj₂

∧-greatest : I  J  I  K  I  (J  K)
∧-greatest K≤I K≤J .*≤* = < K≤I .*≤* , K≤J .*≤* >

∧-infimum : Infimum _≤_ _∧_
∧-infimum I J = (x∧y≤x ,  x∧y≤y , λ K  ∧-greatest)

∧-isMeetSemilattice : IsMeetSemilattice _≈_ _≤_ _∧_
∧-isMeetSemilattice = record
  { isPartialOrder = ≤-isPartialOrder
  ; infimum        = ∧-infimum
  }

-- FIXME: under what conditions does α preserve meets?

 : Ideal
 .ICarrier x = Lift _ Unit.⊤
 .≤-closed x≤y (lift Unit.tt) = lift Unit.tt
 .∨-closed _ _ = lift Unit.tt

⊤-maximum : Maximum _≤_ 
⊤-maximum x .*≤* _ = lift Unit.tt

∧-⊤-isBoundedMeetSemilattice : IsBoundedMeetSemilattice _≈_ _≤_ _∧_ 
∧-⊤-isBoundedMeetSemilattice = record
  { isMeetSemilattice = ∧-isMeetSemilattice
  ; maximum = ⊤-maximum
  }

------------------------------------------------------------------------------
-- Binary joins

_∨_ : Ideal  Ideal  Ideal
I  J = α (U I L.∨ U J)

 : Ideal
 = α L.⊥

x≤x∨y : I  (I  J)
x≤x∨y = ≤-trans counit⁻¹ (α-mono L.x≤x∨y)

y≤x∨y : J  (I  J)
y≤x∨y = ≤-trans counit⁻¹ (α-mono L.y≤x∨y)

∨-least : I  K  J  K  (I  J)  K
∨-least {I} {K} {J} I≤K J≤K .*≤* (t , x≤t) =
  K .≤-closed (C.trans x≤t (`⋁-map-eval _ t)) (`⋁-closed (`⋁-map (L.∨-least (U-mono I≤K) (U-mono J≤K)) t))

∨-supremum : Supremum _≤_ _∨_
∨-supremum I J = (x≤x∨y , y≤x∨y , λ K  ∨-least)

∨-isJoinSemilattice : IsJoinSemilattice _≈_ _≤_ _∨_
∨-isJoinSemilattice = record
  { isPartialOrder = ≤-isPartialOrder
  ; supremum       = ∨-supremum
  }

⊥-minimum : Minimum _≤_ 
⊥-minimum x = ≤-trans (α-mono (L.⊥-minimum (U x))) counit

∨-⊥-isBoundedJoinSemilattice : IsBoundedJoinSemilattice _≈_ _≤_ _∨_ 
∨-⊥-isBoundedJoinSemilattice = record
  { isJoinSemilattice = ∨-isJoinSemilattice
  ; minimum = ⊥-minimum
  }

private
  helper : (c : `⋁ (L.η (x ∨ᶜ y)))  Σ[ d  `⋁ (U (α (L.η x)  α (L.η y))) ] (`⋁-eval c ≤ᶜ `⋁-eval d)
  helper {x}{y} (leaf z (lift z≤x∨y)) =
    (node (leaf x (x≤x∨y .*≤* ((leaf x (lift C.refl)) , C.refl)))
          (leaf y (y≤x∨y .*≤* ((leaf y (lift C.refl)) , C.refl)))) ,
    z≤x∨y
  helper (node c₁ c₂) =
    let (d₁ , c₁≤d₁) , (d₂ , c₂≤d₂) = helper c₁ , helper c₂
    in node d₁ d₂ , C.mono c₁≤d₁ c₂≤d₂

η-preserve-∨ : α (L.η (x ∨ᶜ y))  α (L.η x)  α (L.η y)
η-preserve-∨ {x}{y} .*≤* {z} (c , z≤c) =
  let d , c≤d = helper c in 
    Ideal.≤-closed (α (L.η x)  α (L.η y)) 
      (C.trans z≤c c≤d) (`⋁-closed d)


------------------------------------------------------------------------------
module DayEntropic
    {_∙ᶜ_}
    {εᶜ}
    (isPomonoid : IsPomonoid _≈ᶜ_ _≤ᶜ_ _∙ᶜ_ εᶜ)
    (∨-entropy : Entropy _≤ᶜ_ _∨ᶜ_ _∙ᶜ_)
    (∨-tidy    : εᶜ ∨ᶜ εᶜ ≤ᶜ εᶜ)
    where

  private
    module LMon = L.Day isPomonoid

  _◁_ : Ideal  Ideal  Ideal
  (I  J) .ICarrier x =
    ∃[ y ] ∃[ z ] (x ≤ᶜ (y ∙ᶜ z) × I .ICarrier y × J .ICarrier z)
  (I  J) .≤-closed x≤w (y , z , w≤yz , Iy , Jz) =
    (-, -, C.trans x≤w w≤yz , Iy , Jz)
  (I  J) .∨-closed (y₁ , z₁ , x₁≤y₁z₁ , ϕ₁ , ψ₁) (y₂ , z₂ , x₂≤y₂z₂ , ϕ₂ , ψ₂) =
    y₁ ∨ᶜ y₂ , z₁ ∨ᶜ z₂ ,
    C.trans (C.mono x₁≤y₁z₁ x₂≤y₂z₂) (∨-entropy _ _ _ _) ,
    I .∨-closed ϕ₁ ϕ₂ ,
    J .∨-closed ψ₁ ψ₂

  ι : Ideal
  ι .ICarrier x = Lift c (x ≤ᶜ εᶜ)
  ι .≤-closed x≤y (lift y≤ε) = lift (C.trans x≤y y≤ε)
  ι .∨-closed (lift x≤ε) (lift y≤ε) = lift (C.trans (C.mono x≤ε y≤ε) ∨-tidy)

  ◁-mono : Monotonic₂ _≤_ _≤_ _≤_ _◁_
  ◁-mono I₁≤J₁ I₂≤J₂ .*≤* = LMon.∙-mono (U-mono I₁≤J₁) (U-mono I₂≤J₂) .L.*≤*

  ◁-assoc : Associative _≈_ _◁_
  ◁-assoc I J K .proj₁ .*≤* = LMon.∙-assoc (U I) (U J) (U K) .proj₁ .L.*≤*
  ◁-assoc I J K .proj₂ .*≤* = LMon.∙-assoc (U I) (U J) (U K) .proj₂ .L.*≤*

  ◁-identityˡ : LeftIdentity _≈_ ι _◁_
  ◁-identityˡ I .proj₁ .*≤* = LMon.∙-identityˡ (U I) .proj₁ .L.*≤*
  ◁-identityˡ I .proj₂ .*≤* = LMon.∙-identityˡ (U I) .proj₂ .L.*≤*

  ◁-identityʳ : RightIdentity _≈_ ι _◁_
  ◁-identityʳ I .proj₁ .*≤* = LMon.∙-identityʳ (U I) .proj₁ .L.*≤*
  ◁-identityʳ I .proj₂ .*≤* = LMon.∙-identityʳ (U I) .proj₂ .L.*≤*

  ◁-identity : Identity _≈_ ι _◁_
  ◁-identity = (◁-identityˡ , ◁-identityʳ)

  ◁-isPomonoid : IsPomonoid _≈_ _≤_ _◁_ ι
  ◁-isPomonoid = record
    { isPosemigroup = record
      { isPomagma = record
        { isPartialOrder = ≤-isPartialOrder
        ; mono = ◁-mono
        }
      ; assoc = ◁-assoc
      }
    ; identity = ◁-identity
    }

  U-monoidal : U (I  J) L.≈ (U I LMon.∙ U J)
  U-monoidal .proj₁ .L.*≤* Ix = Ix
  U-monoidal .proj₂ .L.*≤* Ix = Ix

  U-monoidal-ι : U ι L.≈ LMon.ε
  U-monoidal-ι .proj₁ .L.*≤* x≤ε = x≤ε
  U-monoidal-ι .proj₂ .L.*≤* x≤ε = x≤ε

  η-preserve-◁ : η (x ∙ᶜ y)  η x  η y
  η-preserve-◁ {x} {y} .*≤* {z} (c , z≤c) =
    Ideal.≤-closed
      (α (L.η x)  α (L.η y))
        (C.trans z≤c (`⋁-map-eval _ c))
          (`⋁-closed {α (L.η x)  α (L.η y)} 
            (`⋁-map 
              (L.≤-trans LMon.η-preserve-∙ 
                (L.≤-trans (LMon.∙-mono unit unit) (U-monoidal .proj₂))) c))

{-
  -- FIXME: this doesn't work
  module _ (idem : ∀ {x} → x ∨ᶜ x ≤ᶜ x) where

    open IsPomonoid isPomonoid using (mono)

    -- FIXME: this is the same combination function as below
    _∙ᶜ'_ : `⋁ F → `⋁ G → `⋁ (F LMon.∙ G)
    leaf x Fx  ∙ᶜ' leaf y Gy  = leaf (x ∙ᶜ y) (x , y , C.refl , Fx , Gy)
    leaf x Fx  ∙ᶜ' node d₁ d₂ = node (leaf x Fx ∙ᶜ' d₁) (leaf x Fx ∙ᶜ' d₂)
    node c₁ c₂ ∙ᶜ' d          = node (c₁ ∙ᶜ' d) (c₂ ∙ᶜ' d)

    `⋁-∙-eval : (c : `⋁ F)(d : `⋁ G) → eval (c ∙ᶜ' d) ≤ᶜ eval c ∙ᶜ eval d
    `⋁-∙-eval (leaf x Fx)  (leaf y Gy)  = C.refl
    `⋁-∙-eval (leaf x Fx)  (node d₁ d₂) =
       C.trans (C.mono (`⋁-∙-eval (leaf x Fx) d₁) (`⋁-∙-eval (leaf x Fx) d₂))
      (C.trans (∨-entropy _ _ _ _)
               (mono idem C.refl))
    `⋁-∙-eval (node c₁ c₂) d =
      C.trans (C.mono (`⋁-∙-eval c₁ d) (`⋁-∙-eval c₂ d))
      (C.trans (∨-entropy _ _ _ _)
      (mono C.refl idem))

    η-preserve-◁⁻¹ : α (η x) ◁ α (η y) ≤ α (η (x ∙ᶜ y))
    η-preserve-◁⁻¹ {x}{y} .*≤* {z} (z₁ , z₂ , z≤z₁z₂ , (c₁ , z₁≤c) , (c₂ , z₂≤c)) =
      `⋁-map η-preserve-∙⁻¹ (c₁ ∙ᶜ' c₂) ,
      C.trans z≤z₁z₂ {!!}
-}

module DayCommutative
    {_∙ᶜ_}
    {εᶜ}
    (isCommutativePomonoid : IsCommutativePomonoid _≈ᶜ_ _≤ᶜ_ _∙ᶜ_ εᶜ)
    (distrib : _DistributesOver_ _≤ᶜ_ _∙ᶜ_ _∨ᶜ_)
  where

  private
    module Mon = IsCommutativePomonoid isCommutativePomonoid
    module LMon = L.DayCommutative isCommutativePomonoid

  distribˡ = distrib .proj₁
  distribʳ = distrib .proj₂

  _∙_ : Ideal  Ideal  Ideal
  I  J = α (U I LMon.∙ U J)

  ε : Ideal
  ε = α LMon.ε

  _`⋁-∙_ : `⋁ F  `⋁ G  `⋁ (F LMon.∙ G)
  leaf x Fx  `⋁-∙ leaf y Gy  = leaf (x ∙ᶜ y) (x , y , C.refl , Fx , Gy)
  leaf x Fx  `⋁-∙ node d₁ d₂ = node (leaf x Fx `⋁-∙ d₁) (leaf x Fx `⋁-∙ d₂)
  node c₁ c₂ `⋁-∙ d          = node (c₁ `⋁-∙ d) (c₂ `⋁-∙ d)

  `⋁-∙-eval : (c : `⋁ F)(d : `⋁ G)  `⋁-eval c ∙ᶜ `⋁-eval d ≤ᶜ `⋁-eval (c `⋁-∙ d)
  `⋁-∙-eval (leaf x Fx)  (leaf y Gy)  = C.refl
  `⋁-∙-eval (leaf x Fx)  (node d₁ d₂) = C.trans (distribˡ _ _ _) (C.mono (`⋁-∙-eval (leaf x Fx) d₁) (`⋁-∙-eval (leaf x Fx) d₂))
  `⋁-∙-eval (node c₁ c₂) d            = C.trans (distribʳ _ _ _) (C.mono (`⋁-∙-eval c₁ d) (`⋁-∙-eval c₂ d))

  α-helper : (c : `⋁ (U (α F) LMon.∙ U (α G)))  x ≤ᶜ `⋁-eval c  Σ[ d  `⋁ (F LMon.∙ G) ] (x ≤ᶜ `⋁-eval d)
  α-helper (leaf y (y₁ , y₂ , y≤y₁y₂ , (c , y₁≤c) , (d , y₂≤d))) x≤y =
    (c `⋁-∙ d) , C.trans x≤y (C.trans y≤y₁y₂ (C.trans (Mon.mono y₁≤c y₂≤d) (`⋁-∙-eval c d)))
  α-helper (node c d) x≤cd =
    let (c' , c≤c') , (d' , d≤d') = α-helper c C.refl , α-helper d C.refl
    in (node c' d') , (C.trans x≤cd (C.mono c≤c' d≤d'))

  α-monoidal : (α F  α G)  α (F LMon.∙ G)
  α-monoidal .proj₁ .*≤* (c , x≤c)  = α-helper c x≤c
  α-monoidal .proj₂ = α-mono (LMon.∙-mono unit unit)

  ∙-mono : Monotonic₂ _≤_ _≤_ _≤_ _∙_
  ∙-mono I₁≤I₂ J₁≤J₂ = α-mono (LMon.∙-mono (U-mono I₁≤I₂) (U-mono J₁≤J₂))

  η-preserve-∙ : η (x ∙ᶜ y)  η x  η y
  η-preserve-∙ = α-mono (L.≤-trans LMon.η-preserve-∙ (LMon.∙-mono unit unit))

  η-preserve-∙⁻¹ : η x  η y  η (x ∙ᶜ y)
  η-preserve-∙⁻¹ = ≤-trans (α-monoidal .proj₁) (α-mono LMon.η-preserve-∙⁻¹)

  ∙-assoc : Associative _≈_ _∙_
  ∙-assoc I J K =
    begin
      (I  J)  K
    ≡⟨⟩
      α (U (α (U I LMon.∙ U J)) LMon.∙ U K)
    ≈⟨ α-cong (LMon.∙-congˡ (U-cong counit-≈)) 
      α (U (α (U I LMon.∙ U J)) LMon.∙ U (α (U K)))
    ≈⟨ α-monoidal 
      α ((U I LMon.∙ U J) LMon.∙ U K)
    ≈⟨ α-cong (LMon.∙-assoc (U I) (U J) (U K)) 
      α (U I LMon.∙ (U J LMon.∙ U K))
    ≈⟨ α-monoidal 
      α (U (α (U I)) LMon.∙ U (α (U J LMon.∙ U K)))
    ≈⟨ α-cong (LMon.∙-congʳ (U-cong counit-≈)) 
      α (U I LMon.∙ U (α (U J LMon.∙ U K)))
    ≡⟨⟩
      I  (J  K)
    
    where open SetoidReasoning ≈-setoid

  ∙-identityˡ : LeftIdentity _≈_ ε _∙_
  ∙-identityˡ I =
    begin
      ε  I
    ≡⟨⟩
      α (U (α LMon.ε) LMon.∙ U I)
    ≈⟨ α-cong (LMon.∙-congˡ (U-cong counit-≈)) 
      α (U (α LMon.ε) LMon.∙ U (α (U I)))
    ≈⟨ α-monoidal 
      α (LMon.ε LMon.∙ U I)
    ≈⟨ α-cong (LMon.∙-identityˡ (U I)) 
      α (U I)
    ≈⟨ counit-≈ 
      I
    
    where open SetoidReasoning ≈-setoid

  ∙-identityʳ : RightIdentity _≈_ ε _∙_
  ∙-identityʳ I =
    begin
      I  ε
    ≡⟨⟩
      α (U I LMon.∙ U (α LMon.ε))
    ≈⟨ α-cong (LMon.∙-congʳ (U-cong counit-≈)) 
      α (U (α (U I)) LMon.∙ U (α LMon.ε))
    ≈⟨ α-monoidal 
      α (U I LMon.∙ LMon.ε)
    ≈⟨ α-cong (LMon.∙-identityʳ (U I)) 
      α (U I)
    ≈⟨ counit-≈ 
      I
    
    where open SetoidReasoning ≈-setoid

  ∙-comm : Commutative _≈_ _∙_
  ∙-comm I J = α-cong (LMon.∙-comm (U I) (U J))

  ∙-isCommutativePomonoid : IsCommutativePomonoid _≈_ _≤_ _∙_ ε
  ∙-isCommutativePomonoid = record
    { isPomonoid = record
      { isPosemigroup = record
        { isPomagma = record
          { isPartialOrder = ≤-isPartialOrder
          ; mono = ∙-mono
          }
        ; assoc = ∙-assoc
        }
      ; identity = ∙-identityˡ , ∙-identityʳ
      }
      ; comm = ∙-comm
    }

  commutativePomonoid : CommutativePomonoid (suc (c  ℓ₂)) (c  ℓ₂) (c  ℓ₂)
  commutativePomonoid = record
    { isCommutativePomonoid = ∙-isCommutativePomonoid }

  ------------------------------------------------------------------------------
  -- Residuals

  _⊸_ : Ideal  Ideal  Ideal
  (I  J) .ICarrier x =  {y}  I .ICarrier y  J .ICarrier (x ∙ᶜ y)
  (I  J) .≤-closed x≤z f Iy = J .≤-closed (Mon.monoˡ x≤z) (f Iy)
  (I  J) .∨-closed I⊸Jx I⊸Jy {z} Iz =
    J .≤-closed (distribʳ _ _ _) (J .∨-closed (I⊸Jx Iz) (I⊸Jy Iz))

  U⊸ : U (I  J) L.≤ (U I LMon.⊸ U J)
  U⊸ .L.*≤* f = f

  U⊸⁻¹ : (U I LMon.⊸ U J) L.≤ U (I  J)
  U⊸⁻¹ .L.*≤* f = f

  U⊸-≈ : U (I  J) L.≈ (U I LMon.⊸ U J)
  U⊸-≈ = (U⊸ , U⊸⁻¹)

  ⊸-residual-to : (I  J)  K  J  (I  K)
  ⊸-residual-to IJ≤K =
    ≤-trans counit⁻¹
   (≤-trans (α-mono (LMon.⊸-residual-to (L.≤-trans unit (U-mono IJ≤K))))
   (≤-trans (α-mono U⊸⁻¹)
             counit))

  ⊸-residual-from : J  (I  K)  (I  J)  K
  ⊸-residual-from {J} {I} {K} J≤I⊸K =
    begin
      I  J
    ≡⟨⟩
      α (U I LMon.∙ U J)
    ≤⟨ α-mono (LMon.⊸-residual-from (L.≤-trans (U-mono J≤I⊸K) U⊸)) 
      α (U K)
    ≈⟨ counit-≈ 
      K
    
    where open PosetReasoning ≤-poset

  ⊸-residual : RightResidual _≤_ _∙_ _⊸_
  ⊸-residual .Equivalence.to        = ⊸-residual-to
  ⊸-residual .Equivalence.from      = ⊸-residual-from
  ⊸-residual .Equivalence.to-cong   = λ { PropEq.refl  PropEq.refl }
  ⊸-residual .Equivalence.from-cong = λ { PropEq.refl  PropEq.refl }

  ⊸-∙-isResiduatedCommutativePomonoid : IsResiduatedCommutativePomonoid _≈_ _≤_ _∙_ _⊸_ ε
  ⊸-∙-isResiduatedCommutativePomonoid = record
    { isCommutativePomonoid = ∙-isCommutativePomonoid
    ; residuated = comm∧residual⇒residuated ≤-isPreorder ∙-comm ⊸-residual
    }

module DayDuoidal
    {_∙ᶜ_} 
    {_◁ᶜ_} 
    {εᶜ}
    {ιᶜ}
    (isCommutativeDuoidal : IsCommutativeDuoidal _≈ᶜ_ _≤ᶜ_ _∙ᶜ_ _◁ᶜ_ εᶜ ιᶜ)
    (distrib : _DistributesOver_ _≤ᶜ_ _∙ᶜ_ _∨ᶜ_)
    (∨ᶜ-entropy : Entropy _≤ᶜ_ _∨ᶜ_ _◁ᶜ_)
    (∨ᶜ-tidy : ιᶜ ∨ᶜ ιᶜ ≤ᶜ ιᶜ)
  where

  private
    module Duo = IsCommutativeDuoidal isCommutativeDuoidal
    module LDuo = L.DayDuoidal Duo.isDuoidal

  open DayCommutative Duo.∙-isCommutativePomonoid distrib
  open DayEntropic Duo.◁-isPomonoid ∨ᶜ-entropy ∨ᶜ-tidy

  ∙-◁-entropy : Entropy _≤_ _∙_ _◁_
  ∙-◁-entropy I₁ J₁ I₂ J₂ =
    begin
      (I₁  J₁)  (I₂  J₂)
    ≡⟨⟩
      α (U (I₁  J₁) LDuo.∙ U (I₂  J₂))
    ≈⟨ α-cong (LDuo.∙-cong U-monoidal U-monoidal) 
      α ((U I₁ LDuo.◁ U J₁) LDuo.∙ (U I₂ LDuo.◁ U J₂))
    ≤⟨ α-mono (LDuo.∙-◁-entropy (U I₁) (U J₁) (U I₂) (U J₂)) 
      α ((U I₁ LDuo.∙ U I₂) LDuo.◁ (U J₁ LDuo.∙ U J₂))
    ≤⟨ α-mono (LDuo.◁-mono unit unit) 
      α (U (α (U I₁ LDuo.∙ U I₂)) LDuo.◁ U (α (U J₁ LDuo.∙ U J₂)))
    ≈⟨ α-cong U-monoidal 
      α (U (α (U I₁ LDuo.∙ U I₂)  α (U J₁ LDuo.∙ U J₂)))
    ≈⟨ counit-≈ 
      α (U I₁ LDuo.∙ U I₂)  α (U J₁ LDuo.∙ U J₂)
    ≡⟨⟩
      (I₁  I₂)  (J₁  J₂)
    
    where open PosetReasoning ≤-poset

  tidy : (c : `⋁ LDuo.ι)  `⋁-eval c ≤ᶜ ιᶜ
  tidy (leaf x (lift x≤ι)) = x≤ι
  tidy (node c d) = C.trans (C.mono (tidy c) (tidy d)) ∨ᶜ-tidy

  ε≤ι : ε  ι
  ε≤ι .*≤* (t , x≤t) = lift (C.trans x≤t (C.trans (`⋁-map-eval LDuo.ε≤ι t) (tidy (`⋁-map LDuo.ε≤ι t))))

  ∙-◁-isDuoidal : IsDuoidal _≈_ _≤_ _∙_ _◁_ ε ι
  ∙-◁-isDuoidal = record
    { ∙-isPomonoid = IsCommutativePomonoid.isPomonoid ∙-isCommutativePomonoid
    ; ◁-isPomonoid = ◁-isPomonoid
    ; ∙-◁-entropy = ∙-◁-entropy
    ; ∙-idem-ι = ≤-trans (α-mono (LDuo.∙-mono (U-monoidal-ι .proj₁) (U-monoidal-ι .proj₁)))
                (≤-trans (α-mono LDuo.∙-idem-ι)
                (≤-trans (α-mono (U-monoidal-ι .proj₂))
                          counit))
    ; ◁-idem-ε = ≤-trans (α-mono LDuo.◁-idem-ε)
                (≤-trans (α-mono (LDuo.◁-mono unit unit))
                (≤-trans (α-mono (U-monoidal .proj₂))
                counit))
    ; ε≲ι = ε≤ι
    }