open import SOAS.Metatheory.Syntax
module SOAS.Metatheory.FreeMonoid {T : Set} (Syn : Syntax {T}) where
open Syntax Syn
open import SOAS.Common
open import SOAS.Families.Core {T}
open import SOAS.Context {T}
open import SOAS.Variable {T}
open import SOAS.Construction.Structure as Structure
open import SOAS.Abstract.Hom {T}
import SOAS.Abstract.Coalgebra {T} as โโก ; open โโก.Sorted
import SOAS.Abstract.Box {T} as โก ; open โก.Sorted
open import Categories.Monad
open import SOAS.Abstract.Monoid
open import SOAS.Coalgebraic.Map
open import SOAS.Coalgebraic.Monoid
open import SOAS.Coalgebraic.Strength
open import SOAS.Metatheory Syn
private
variable
ฮฑ ฮฒ : T
ฮ ฮ : Ctx
module _ (๐ : Familyโ) where
open Theory ๐
ฮฃ๐แต : ฮฃMon ๐
ฮฃ๐แต = record
{ แต = ๐แต
; ๐๐๐ = ๐๐๐
; ฮผโจ๐๐๐โฉ = ฮป{ {ฯ = ฯ} t โ begin
๐ค๐ฆ๐ (๐๐๐ t) ฯ
โกโจ Substitution.๐ฅโจ๐โฉ โฉ
๐๐๐ (str ๐แดฎ ๐ (โ
โ ๐ค๐ฆ๐ t) ฯ)
โกโจ cong ๐๐๐ (CoalgMon.str-eq ๐แดน ๐ โ
:Str (โ
โ ๐ค๐ฆ๐ t) ฯ) โฉ
๐๐๐ (str (Mon.แดฎ ๐แต) ๐ (โ
โ ๐ค๐ฆ๐ t) ฯ)
โ }
} where open โก-Reasoning
module FฮฃM {โณ : Familyโ}(ฮฃโณแต : ฮฃMon โณ) (ฯ : ๐ โพฬฃ โณ) where
open ฮฃMon ฮฃโณแต renaming (๐๐๐ to โณ๐๐๐ ; แดฎ to โณแดฎ ; แต to โณแต) public
private module โณ = ฮฃMon ฮฃโณแต
ฯ : ๐ โพฬฃ ใ โณ , โณ ใ
ฯ ๐ช ฮต = ฮผ (ฯ ๐ช) ฮต
โณแต : MetaAlg โณ
โณแต = record { ๐๐๐ = โณ.๐๐๐ ; ๐ฃ๐๐ = ฮท ; ๐๐ฃ๐๐ = ฯ }
open Semantics โณแต public renaming (๐ค๐๐ to ๐๐ฉ๐ฅ)
open MetaAlg โณแต
open Coalgebraic ฮผแถ
๐๐ฉ๐ฅแตโ : Coalgโ ๐แต โณ.แต ๐๐ฉ๐ฅ
๐๐ฉ๐ฅแตโ = ๐ค๐๐แตโ โณ.แต โณแต record
{ โจ๐๐๐โฉ = ฮป{ {t = t} โ dext (ฮป ฯ โ begin
ฮผ (๐๐๐ t) (ฮท โ ฯ)
โกโจ ฮผโจ๐๐๐โฉ t โฉ
๐๐๐ (str โณ.แดฎ โณ (โ
โ ฮผ t) (ฮท โ ฯ))
โกโจ cong ๐๐๐ (str-natโ (ฮทแดฎโ โณแดฎ) (โ
โ โณ.ฮผ t) ฯ) โฉ
๐๐๐ (str โแดฎ โณ (โ
.Fโ (ฮป { h ฯ โ h (ฮป v โ ฮท (ฯ v)) }) (โ
โ โณ.ฮผ t)) ฯ)
โกหโจ congr โ
.homomorphism (ฮป - โ ๐๐๐ (str โแดฎ โณ - ฯ)) โฉ
๐๐๐ (str โแดฎ โณ (โ
.Fโ (ฮป{ t ฯ โ ฮผ t (ฮท โ ฯ)}) t) ฯ)
โ) }
; โจ๐ฃ๐๐โฉ = dextโฒ โณ.lunit
; โจ๐๐ฃ๐๐โฉ = dextโฒ โณ.assoc
} where open โก-Reasoning
๐๐ฉ๐ฅแดฎโ : Coalgโโ ๐แดฎ โณ.แดฎ ๐๐ฉ๐ฅ
๐๐ฉ๐ฅแดฎโ = record { แตโ = ๐๐ฉ๐ฅแตโ ; โจฮทโฉ = โจ๐งโฉ }
ฮผโ๐๐ฉ๐ฅ : MapEqโ ๐แดฎ โณ.๐๐๐ (ฮป t ฯ โ ๐๐ฉ๐ฅ (๐ค๐ฆ๐ t ฯ))
(ฮป t ฯ โ ฮผ (๐๐ฉ๐ฅ t) (๐๐ฉ๐ฅ โ ฯ))
ฮผโ๐๐ฉ๐ฅ = record
{ ฯ = ๐๐ฉ๐ฅ
; ฯ = ฯ
; fโจ๐ฃโฉ = cong ๐๐ฉ๐ฅ Substitution.๐ฅโจ๐งโฉ
; fโจ๐โฉ = trans (cong ๐๐ฉ๐ฅ Substitution.๐ฅโจ๐โฉ) โจ๐โฉ
; fโจ๐โฉ = ฮป{ {ฯ = ฯ}{t} โ begin
๐๐ฉ๐ฅ (๐ค๐ฆ๐ (๐๐๐ t) ฯ)
โกโจ cong ๐๐ฉ๐ฅ Substitution.๐ฅโจ๐โฉ โฉ
๐๐ฉ๐ฅ (๐๐๐ (str ๐แดฎ ๐ (โ
โ ๐ค๐ฆ๐ t) ฯ))
โกโจ โจ๐โฉ โฉ
๐๐๐ (โ
โ ๐๐ฉ๐ฅ (str ๐แดฎ ๐ (โ
โ ๐ค๐ฆ๐ t) ฯ))
โกหโจ cong ๐๐๐ (str-natโ ๐๐ฉ๐ฅ (โ
โ ๐ค๐ฆ๐ t) ฯ) โฉ
๐๐๐ (str ๐แดฎ โณ (โ
.Fโ (ฮป { h ฯ โ ๐๐ฉ๐ฅ (h ฯ) }) (โ
โ ๐ค๐ฆ๐ t)) ฯ)
โกหโจ congr โ
.homomorphism (ฮป - โ ๐๐๐ (str ๐แดฎ โณ - ฯ)) โฉ
๐๐๐ (str ๐แดฎ โณ (โ
โ (ฮป{ t ฯ โ ๐๐ฉ๐ฅ (๐ค๐ฆ๐ t ฯ)}) t) ฯ)
โ }
; gโจ๐ฃโฉ = trans (ฮผโโ โจ๐งโฉ) (Mon.lunit โณ.แต)
; gโจ๐โฉ = trans (ฮผโโ โจ๐โฉ) (Mon.assoc โณ.แต)
; gโจ๐โฉ = ฮป{ {ฯ = ฯ}{t} โ begin
ฮผ (๐๐ฉ๐ฅ (๐๐๐ t)) (๐๐ฉ๐ฅ โ ฯ)
โกโจ ฮผโโ โจ๐โฉ โฉ
ฮผ (๐๐๐ (โ
โ ๐๐ฉ๐ฅ t)) (๐๐ฉ๐ฅ โ ฯ)
โกโจ ฮผโจ๐๐๐โฉ _ โฉ
๐๐๐ (str โณแดฎ โณ (โ
โ ฮผ (โ
โ ๐๐ฉ๐ฅ t)) (๐๐ฉ๐ฅ โ ฯ))
โกหโจ congr โ
.homomorphism (ฮป - โ ๐๐๐ (str โณแดฎ โณ - (๐๐ฉ๐ฅ โ ฯ))) โฉ
๐๐๐ (str โณแดฎ โณ (โ
โ (ฮผ โ ๐๐ฉ๐ฅ) t) (๐๐ฉ๐ฅ โ ฯ))
โกโจ cong ๐๐๐ (str-natโ ๐๐ฉ๐ฅแดฎโ ((โ
โ (ฮผ โ ๐๐ฉ๐ฅ) t)) ฯ) โฉ
๐๐๐ (str ๐แดฎ โณ (โ
.Fโ (ฮป { hโฒ ฯ โ hโฒ (๐๐ฉ๐ฅ โ ฯ) }) (โ
โ (ฮผ โ ๐๐ฉ๐ฅ) t)) ฯ)
โกหโจ congr โ
.homomorphism (ฮป - โ โณ๐๐๐ (str ๐แดฎ โณ - ฯ)) โฉ
๐๐๐ (str ๐แดฎ โณ (โ
โ (ฮป{ t ฯ โ ฮผ (๐๐ฉ๐ฅ t) (๐๐ฉ๐ฅ โ ฯ)}) t) ฯ)
โ }
} where open โก-Reasoning
๐๐ฉ๐ฅแตโ : ฮฃMonโ ฮฃ๐แต ฮฃโณแต ๐๐ฉ๐ฅ
๐๐ฉ๐ฅแตโ = record { แตโ = record
{ โจฮทโฉ = โจ๐งโฉ
; โจฮผโฉ = ฮป{ {t = t} โ MapEqโ.โ ฮผโ๐๐ฉ๐ฅ t } }
; โจ๐๐๐โฉ = โจ๐โฉ }
module ๐๐ฉ๐ฅแตโ = ฮฃMonโ ๐๐ฉ๐ฅแตโ
module _ {g : ๐ โพฬฃ โณ}
(gแตโ : ฮฃMonโ ฮฃ๐แต ฮฃโณแต g)
(p : โ{ฮฑ ฮ }{๐ช : ๐ ฮฑ ฮ } โ g (๐๐ง๐๐ฃ ๐ช ๐ง๐๐ฃ) โก ฯ ๐ช) where
open ฮฃMonโ gแตโ renaming (โจ๐๐๐โฉ to gโจ๐๐๐โฉ)
gแตโ : MetaAlgโ ๐แต โณแต g
gแตโ = record
{ โจ๐๐๐โฉ = gโจ๐๐๐โฉ
; โจ๐ฃ๐๐โฉ = โจฮทโฉ
; โจ๐๐ฃ๐๐โฉ = ฮป{ {๐ช = ๐ช}{ฮต} โ begin
g (๐๐ง๐๐ฃ ๐ช ฮต) โกหโจ cong g (cong (๐๐ง๐๐ฃ ๐ช) (dextโฒ Substitution.๐ฅโจ๐งโฉ)) โฉ
g (๐๐ง๐๐ฃ ๐ช (ฮป v โ ๐ค๐ฆ๐ (๐ง๐๐ฃ v) ฮต)) โกหโจ cong g Substitution.๐ฅโจ๐โฉ โฉ
g (๐ค๐ฆ๐ (๐๐ง๐๐ฃ ๐ช ๐ง๐๐ฃ) ฮต) โกโจ โจฮผโฉ โฉ
ฮผ (g (๐๐ง๐๐ฃ ๐ช ๐ง๐๐ฃ)) (g โ ฮต) โกโจ ฮผโโ p โฉ
ฮผ (ฯ ๐ช) (ฮป x โ g (ฮต x)) โ }
} where open โก-Reasoning
๐๐ฉ๐ฅแต! : {ฮฑ : T}{ฮ : Ctx}(t : ๐ ฮฑ ฮ) โ ๐๐ฉ๐ฅ t โก g t
๐๐ฉ๐ฅแต! = ๐ค๐๐! gแตโ
FamโโฮฃMon : Familyโ โ ฮฃMonoid
FamโโฮฃMon ๐ = Theory.๐ ๐ โ (ฮฃ๐แต ๐)
open ฮฃMonoidStructure.Free
Free-ฮฃMon-Mapping : FreeฮฃMonoid.FreeMapping FamโโฮฃMon
Free-ฮฃMon-Mapping = record
{ embed = ฮป {๐} ๐ช โ let open Theory ๐ in ๐๐ง๐๐ฃ ๐ช ๐ง๐๐ฃ
; univ = ฮป{ ๐ (โณ โ ฮฃโณแต) ฯ โ let open FฮฃM ๐ ฮฃโณแต ฯ in record
{ extend = ๐๐ฉ๐ฅ โ ๐๐ฉ๐ฅแตโ
; factor = trans โจ๐โฉ (trans (ฮผโโ โจ๐งโฉ) runit)
; unique = ฮป{ (g โ gแตโ) p {x = t} โ sym (๐๐ฉ๐ฅแต! gแตโ p t) } }}
}
Free:๐ฝamโโถฮฃ๐on : Functor ๐ฝamiliesโ ฮฃ๐onoids
Free:๐ฝamโโถฮฃ๐on = FreeฮฃMonoid.FreeMapping.Free Free-ฮฃMon-Mapping
ฮฃMon:Monad : Monad ๐ฝamiliesโ
ฮฃMon:Monad = FreeฮฃMonoid.FreeMapping.FreeMonad Free-ฮฃMon-Mapping
๐F : Functor ๐ฝamiliesโ ๐ฝamiliesโ
๐F = Monad.F ฮฃMon:Monad
open Theory
open Monad ฮฃMon:Monad
๐โ : {๐ ๐ : Familyโ} โ (๐ โพฬฃ ๐) โ ๐ ๐ โพฬฃ ๐ ๐
๐โ f t = Functor.โ ๐F f t
๐โโ๐ง๐๐ฃ : {๐ ๐ : Familyโ}(f : ๐ โพฬฃ ๐)(v : โ ฮฑ ฮ)
โ ๐โ f (๐ง๐๐ฃ ๐ v) โก ๐ง๐๐ฃ ๐ v
๐โโ๐ง๐๐ฃ {๐ = ๐}{๐} f v = FฮฃM.โจ๐งโฉ ๐ (ฮฃ๐แต ๐) (ฮป ๐ช โ ๐๐ง๐๐ฃ ๐ (f ๐ช) (๐ง๐๐ฃ ๐))
๐โโ๐๐ง๐๐ฃ : {๐ ๐ : Familyโ}(f : ๐ โพฬฃ ๐)(๐ช : ๐ ฮฑ ฮ)(ฮต : ฮ ~[ ๐ ๐ ]โ ฮ)
โ ๐โ f (๐๐ง๐๐ฃ ๐ ๐ช ฮต) โก ๐๐ง๐๐ฃ ๐ (f ๐ช) (๐โ f โ ฮต)
๐โโ๐๐ง๐๐ฃ {๐ = ๐}{๐} f ๐ช ฮต = begin
๐โ f (๐๐ง๐๐ฃ ๐ ๐ช ฮต)
โกโจโฉ
FฮฃM.๐๐ฉ๐ฅ ๐ (ฮฃ๐แต ๐) (ฮป ๐ช โ ๐๐ง๐๐ฃ ๐ (f ๐ช) (๐ง๐๐ฃ ๐)) (๐๐ง๐๐ฃ ๐ ๐ช ฮต)
โกโจ FฮฃM.โจ๐โฉ ๐ (ฮฃ๐แต ๐) (ฮป ๐ช โ ๐๐ง๐๐ฃ ๐ (f ๐ช) (๐ง๐๐ฃ ๐)) โฉ
๐ค๐ฆ๐ ๐ (๐๐ง๐๐ฃ ๐ (f ๐ช) (๐ง๐๐ฃ ๐)) (๐โ f โ ฮต)
โกโจ Substitution.๐ฅโจ๐โฉ ๐ โฉ
๐๐ง๐๐ฃ ๐ (f ๐ช) (ฮป ๐ซ โ ๐ค๐ฆ๐ ๐ (๐ง๐๐ฃ ๐ ๐ซ) (๐โ f โ ฮต))
โกโจ cong (๐๐ง๐๐ฃ ๐ (f ๐ช)) (dext (ฮป ๐ซ โ lunit ๐)) โฉ
๐๐ง๐๐ฃ ๐ (f ๐ช) (๐โ f โ ฮต)
โ where open โก-Reasoning
๐โโ๐๐ง๐๐ฃ[๐ง๐๐ฃ] : {๐ ๐ : Familyโ}(f : ๐ โพฬฃ ๐)(๐ช : ๐ ฮฑ ฮ)(ฯ : ฮ โ ฮ)
โ ๐โ f (๐๐ง๐๐ฃ ๐ ๐ช (๐ง๐๐ฃ ๐ โ ฯ)) โก ๐๐ง๐๐ฃ ๐ (f ๐ช) (๐ง๐๐ฃ ๐ โ ฯ)
๐โโ๐๐ง๐๐ฃ[๐ง๐๐ฃ] {๐ = ๐}{๐} f ๐ช ฯ = begin
๐โ f (๐๐ง๐๐ฃ ๐ ๐ช (๐ง๐๐ฃ ๐ โ ฯ))
โกโจ ๐โโ๐๐ง๐๐ฃ f ๐ช (๐ง๐๐ฃ ๐ โ ฯ) โฉ
๐๐ง๐๐ฃ ๐ (f ๐ช) (๐โ f โ ๐ง๐๐ฃ ๐ โ ฯ)
โกโจ cong (๐๐ง๐๐ฃ ๐ (f ๐ช)) (dext ฮป v โ ๐โโ๐ง๐๐ฃ f (ฯ v)) โฉ
๐๐ง๐๐ฃ ๐ (f ๐ช) (๐ง๐๐ฃ ๐ โ ฯ)
โ where open โก-Reasoning