module SOAS.Abstract.Monoid {T : Set} where
open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.ContextMaps.Combinators
open import SOAS.Construction.Structure as Structure
open import SOAS.Abstract.Hom {T}
open import SOAS.Abstract.Coalgebra using (module Sorted) ; open Sorted
open import SOAS.Families.Core {T}
open import Categories.Category.Equivalence using (StrongEquivalence)
open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)
open import SOAS.Coalgebraic.Map {T}
open import SOAS.Coalgebraic.Lift {T}
private
variable
Γ Δ Θ : Ctx
α β γ : T
record Mon (𝒳 : Familyₛ) : Set where
field
η : ℐ ⇾̣ 𝒳
μ : 𝒳 ⇾̣ 〖 𝒳 , 𝒳 〗
lunit : {σ : Γ ~[ 𝒳 ]↝ Δ}{v : ℐ α Γ}
→ μ (η v) σ ≡ σ v
runit : {t : 𝒳 α Γ} → μ t η ≡ t
assoc : {σ : Γ ~[ 𝒳 ]↝ Δ}{ς : Δ ~[ 𝒳 ]↝ Θ} {t : 𝒳 α Γ}
→ μ (μ t σ) ς ≡ μ t (λ v → μ (σ v) ς)
μ≈₁ : {t₁ t₂ : 𝒳 α Γ}{σ : Γ ~[ 𝒳 ]↝ Δ}
→ t₁ ≡ t₂
→ μ t₁ σ ≡ μ t₂ σ
μ≈₁ refl = refl
μ≈₂ : {t : 𝒳 α Γ}{σ ς : Γ ~[ 𝒳 ]↝ Δ}
→ ({τ : T}{v : ℐ τ Γ} → σ v ≡ ς v)
→ μ t σ ≡ μ t ς
μ≈₂ {t = t} p = cong (μ t) (dext′ p)
ᵇ : Coalg 𝒳
ᵇ = record { r = λ t ρ → μ t (η ∘ ρ) ; counit = runit
; comult = λ { {t = t} → sym (trans assoc (μ≈₂ lunit)) } }
ᴮ : Coalgₚ 𝒳
ᴮ = record { ᵇ = ᵇ ; η = η ; r∘η = lunit }
[_/] : 𝒳 α Γ → 𝒳 β (α ∙ Γ) → 𝒳 β Γ
[ s /] t = μ t (add 𝒳 s η)
[_/]′ : 𝒳 α Γ → 𝒳 γ (β ∙ α ∙ Γ) → 𝒳 γ (β ∙ Γ)
[ s /]′ t = μ t (lift₁ ᴮ (add 𝒳 s η))
[_,_/]₂ : 𝒳 α Γ → 𝒳 β Γ → 𝒳 γ (α ∙ β ∙ Γ) → 𝒳 γ Γ
[ s₁ , s₂ /]₂ t = μ t (add 𝒳 s₁ (add 𝒳 s₂ η))
open Coalgₚ ᴮ public using (r ; r∘η)
μᶜ : Coalgebraic ᴮ ᴮ ᴮ μ
μᶜ = record { r∘f = assoc ; f∘r = trans assoc (μ≈₂ lunit) ; f∘η = lunit }
record Mon⇒ {𝒳 𝒴 : Familyₛ}(𝒳ᵐ : Mon 𝒳)(𝒴ᵐ : Mon 𝒴)
(f : 𝒳 ⇾̣ 𝒴) : Set where
private module 𝒳 = Mon 𝒳ᵐ
private module 𝒴 = Mon 𝒴ᵐ
field
⟨η⟩ : {v : ℐ α Γ} → f (𝒳.η v) ≡ 𝒴.η v
⟨μ⟩ : {σ : Γ ~[ 𝒳 ]↝ Δ}{t : 𝒳 α Γ}
→ f (𝒳.μ t σ) ≡ 𝒴.μ (f t) (f ∘ σ)
ᵇ⇒ : Coalg⇒ 𝒳.ᵇ 𝒴.ᵇ f
ᵇ⇒ = record { ⟨r⟩ = trans ⟨μ⟩ (𝒴.μ≈₂ ⟨η⟩) }
ᴮ⇒ : Coalgₚ⇒ 𝒳.ᴮ 𝒴.ᴮ f
ᴮ⇒ = record { ᵇ⇒ = ᵇ⇒ ; ⟨η⟩ = ⟨η⟩ }
sub-lemma : (s : 𝒳 α Γ)(t : 𝒳 β (α ∙ Γ)) →
f (𝒳.[ s /] t) ≡ 𝒴.[ f s /] (f t)
sub-lemma s t = trans ⟨μ⟩ (cong (𝒴.μ (f t))
(dext λ{ new → refl ; (old y) → ⟨η⟩}))
sub-lemma₂ : (s₁ : 𝒳 α Γ)(s₂ : 𝒳 β Γ)(t : 𝒳 γ (α ∙ β ∙ Γ)) →
f (𝒳.[ s₁ , s₂ /]₂ t) ≡ 𝒴.[ f s₁ , f s₂ /]₂ (f t)
sub-lemma₂ s₁ s₂ t = trans ⟨μ⟩ (cong (𝒴.μ (f t))
(dext λ{ new → refl ; (old new) → refl
; (old (old y)) → ⟨η⟩}))
module MonoidStructure = Structure 𝔽amiliesₛ Mon
𝕄onoids : Category 1ℓ 0ℓ 0ℓ
𝕄onoids = MonoidStructure.StructCat record
{ IsHomomorphism = Mon⇒
; id-hom = record { ⟨η⟩ = refl ; ⟨μ⟩ = refl }
; comp-hom = λ g f gᵐ⇒ fᵐ⇒ → record
{ ⟨η⟩ = trans (cong g (⟨η⟩ fᵐ⇒)) (⟨η⟩ gᵐ⇒)
; ⟨μ⟩ = trans (cong g (⟨μ⟩ fᵐ⇒)) (⟨μ⟩ gᵐ⇒)
}
} where open Mon⇒
module 𝕄on = Category 𝕄onoids
Monoid : Set₁
Monoid = 𝕄on.Obj
Monoid⇒ : Monoid → Monoid → Set
Monoid⇒ = 𝕄on._⇒_
module AsMonoid (ℳᵐ : Monoid) where
open Object ℳᵐ renaming (𝐶 to ℳ; ˢ to ᵐ) public
open Mon ᵐ public
module AsMonoid⇒ {ℳᵐ 𝒩ᵐ : Monoid} (fᵐ⇒ : Monoid⇒ ℳᵐ 𝒩ᵐ) where
open Morphism fᵐ⇒ renaming (𝑓 to f ; ˢ⇒ to ᵐ⇒) public
open Mon⇒ ᵐ⇒ public