-- Closed monoid in the skew-closed category of families
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) ς)

  -- Congruence in both arguments of the multiplication
  μ≈₁ : {t₁ t₂ : 𝒳 α Γ}{σ : Γ ~[ 𝒳 ]↝ Δ}
       t₁  t₂
       μ t₁ σ  μ t₂ σ
  μ≈₁ refl = refl

  μ≈₂ : {t : 𝒳 α Γ}{σ ς : Γ ~[ 𝒳 ]↝ Δ}
       ({τ : T}{v :  τ Γ}  σ v  ς v)
       μ t σ  μ t ς
  μ≈₂ {t = t} p = cong (μ t) (dext′ p)

  -- Monoids are pointed coalgebras
   : Coalg 𝒳
   = record { r = λ t ρ   μ t (η  ρ) ; counit = runit
    ; comult = λ { {t = t}  sym (trans assoc (μ≈₂ lunit)) } }

   : Coalgₚ 𝒳
   = record {  =  ; η = η ; r∘η = lunit }

  -- Single-variable substitution
  [_/] : 𝒳 α Γ  𝒳 β (α  Γ)  𝒳 β Γ
  [ s /] t = μ t (add 𝒳 s η)

  -- Substitution for second variable
  [_/]′ : 𝒳 α Γ  𝒳 γ (β  α  Γ)  𝒳 γ (β  Γ)
  [ s /]′ t = μ t (lift₁  (add 𝒳 s η))

  -- Substitution for top two variables
  [_,_/]₂ : 𝒳 α Γ  𝒳 β Γ  𝒳 γ (α  β  Γ)  𝒳 γ Γ
  [ s₁ , s₂ /]₂ t = μ t (add 𝒳 s₁ (add 𝒳 s₂ η))


  open Coalgₚ  public using (r ; r∘η)

  -- Multiplication is coalgebraic map
  μᶜ : Coalgebraic    μ
  μᶜ = record { r∘f = assoc ; f∘r = trans assoc (μ≈₂ lunit) ; f∘η = lunit }


-- Monoid homomorphisms
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 { ᵇ⇒ = ᵇ⇒ ; ⟨η⟩ = ⟨η⟩ }

  -- Preservation of multiplication and unit implies the semantic substitution
  -- lemma for single- and double-variable substitution
  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

-- Category of substitution monoids
𝕄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