{-# 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)
≤-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
}
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
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)
`⋁-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
_∧_ : 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
}
⊤ : 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
}
_∨_ : 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))
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 }
_⊸_ : 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))
; ε≲ι = ε≤ι
}