module SOAS.Coalgebraic.Monoid {T : Set} where
open import SOAS.Common
open import SOAS.Context {T}
open import SOAS.Variable
open import SOAS.Families.Core {T}
import SOAS.Families.Delta {T} as δ; open δ.Sorted
open import SOAS.Abstract.Hom {T}
import SOAS.Abstract.Box {T} as □ ; open □.Sorted
open import SOAS.Abstract.Monoid {T}
import SOAS.Abstract.Coalgebra {T} as →□ ; open →□.Sorted
open import SOAS.Coalgebraic.Map
open import SOAS.Coalgebraic.Strength
open import SOAS.Coalgebraic.Lift
private
variable
Γ Δ : Ctx
α β : T
record CoalgMon (𝒳 : Familyₛ) : Set where
field
ᴮ : Coalgₚ 𝒳
ᵐ : Mon 𝒳
open Coalgₚ ᴮ public renaming (η to ηᴮ)
open Mon ᵐ public hiding (ᵇ ; ᴮ ; r ; r∘η ; μᶜ) renaming (η to ηᵐ)
field
η-compat : {v : ℐ α Γ} → ηᴮ v ≡ ηᵐ v
μ-compat : {ρ : Γ ↝ Δ}{t : 𝒳 α Γ} → r t ρ ≡ μ t (ηᵐ ∘ ρ)
open Coalgₚ ᴮ using (r∘η) public
μᶜ : Coalgebraic ᴮ ᴮ ᴮ μ
μᶜ = record
{ r∘f = λ{ {σ = σ}{ϱ}{t} → begin
r (μ t σ) ϱ ≡⟨ μ-compat ⟩
μ (μ t σ) (ηᵐ ∘ ϱ) ≡⟨ assoc ⟩
μ t (λ v → μ (σ v) (ηᵐ ∘ ϱ)) ≡˘⟨ cong (μ t) (dext (λ _ → μ-compat)) ⟩
μ t (λ v → r (σ v) ϱ) ∎ }
; f∘r = λ{ {ρ = ρ}{ς}{t} → begin
μ (r t ρ) ς ≡⟨ cong (λ - → μ - ς) μ-compat ⟩
μ (μ t (ηᵐ ∘ ρ)) ς ≡⟨ assoc ⟩
μ t (λ v → μ (ηᵐ (ρ v)) ς) ≡⟨ cong (μ t) (dext (λ _ → lunit)) ⟩
μ t (ς ∘ ρ) ∎ }
; f∘η = trans (μ≈₂ η-compat) runit
} where open ≡-Reasoning
str-eq : (𝒴 : Familyₛ){F : Functor 𝔽amiliesₛ 𝔽amiliesₛ}(F:Str : Strength F)
(open Functor F)(open Strength F:Str)
(h : F₀ 〖 𝒳 , 𝒴 〗 α Γ)(σ : Γ ~[ 𝒳 ]↝ Δ)
→ str ᴮ 𝒴 h σ ≡ str (Mon.ᴮ ᵐ) 𝒴 h σ
str-eq 𝒴 {F} F:Str h σ = begin
str ᴮ 𝒴 h σ
≡⟨ str-nat₁ {f = id} (record { ᵇ⇒ = record { ⟨r⟩ = sym μ-compat }
; ⟨η⟩ = sym η-compat }) h σ ⟩
str (Mon.ᴮ ᵐ) 𝒴 (F₁ id h) σ
≡⟨ congr identity (λ - → str (Mon.ᴮ ᵐ) 𝒴 - σ) ⟩
str (Mon.ᴮ ᵐ) 𝒴 h σ
∎
where
open Functor F
open Strength F:Str
open ≡-Reasoning
lift-eq : {Ξ : Ctx}(t : 𝒳 β (Ξ ∔ Γ))(σ : Γ ~[ 𝒳 ]↝ Δ) →
μ t (lift ᴮ Ξ σ) ≡ μ t (lift (Mon.ᴮ ᵐ) Ξ σ)
lift-eq {Ξ = Ξ} t σ = str-eq 𝒳 (δ:Strength Ξ) (μ t) σ