open import SOAS.Common
open import SOAS.Families.Core
open import Categories.Object.Initial
open import SOAS.Coalgebraic.Strength
import SOAS.Metatheory.MetaAlgebra
module SOAS.Metatheory.Substitution {T : Set}
(โ
F : Functor ๐ฝamiliesโ ๐ฝamiliesโ) (โ
:Str : Strength โ
F)
(๐ : Familyโ) (open SOAS.Metatheory.MetaAlgebra โ
F ๐)
(๐:Init : Initial ๐etaAlgebras)
where
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Abstract.Hom
import SOAS.Abstract.Coalgebra as โโก ; open โโก.Sorted
import SOAS.Abstract.Box as โก ; open โก.Sorted
open import SOAS.Abstract.Monoid
open import SOAS.Coalgebraic.Map
open import SOAS.Coalgebraic.Monoid
open import SOAS.Metatheory.Algebra โ
F
open import SOAS.Metatheory.Semantics โ
F โ
:Str ๐ ๐:Init
open import SOAS.Metatheory.Traversal โ
F โ
:Str ๐ ๐:Init
open import SOAS.Metatheory.Renaming โ
F โ
:Str ๐ ๐:Init
open import SOAS.Metatheory.Coalgebraic โ
F โ
:Str ๐ ๐:Init
open Strength โ
:Str
private
variable
ฮ ฮ : Ctx
ฮฑ : T
module Substitution = Traversal ๐แดฎ ๐๐๐ id ๐๐ง๐๐ฃ
๐ค๐ฆ๐ : ๐ โพฬฃ ใ ๐ , ๐ ใ
๐ค๐ฆ๐ = Substitution.๐ฅ๐ฃ๐๐ง
๐ค๐ฆ๐แถ : Coalgebraic ๐แดฎ ๐แดฎ ๐แดฎ ๐ค๐ฆ๐
๐ค๐ฆ๐แถ = Travแถ.๐ฅ๐ฃ๐๐งแถ ๐แดฎ ๐๐๐ id ๐๐ง๐๐ฃ ๐แดฎ idแดฎโ Renaming.๐ค๐๐แตโ
module ๐ค๐ฆ๐แถ = Coalgebraic ๐ค๐ฆ๐แถ
compat : {ฯ : ฮ โ ฮ} (t : ๐ ฮฑ ฮ) โ ๐ฃ๐๐ t ฯ โก ๐ค๐ฆ๐ t (๐ง๐๐ฃ โ ฯ)
compat {ฯ = ฯ} t = begin ๐ฃ๐๐ t ฯ โกหโจ ๐ฅ๐ฃ๐๐ง-ฮทโid ๐แดฎ id refl โฉ
๐ค๐ฆ๐ (๐ฃ๐๐ t ฯ) ๐ง๐๐ฃ โกโจ ๐ค๐ฆ๐แถ.fโr โฉ
๐ค๐ฆ๐ t (๐ง๐๐ฃ โ ฯ) โ where open โก-Reasoning
๐ค๐ฆ๐-comp : MapEqโ ๐แดฎ ๐แดฎ ๐๐๐ (ฮป t ฯ ฯ โ ๐ค๐ฆ๐ (๐ค๐ฆ๐ t ฯ) ฯ)
(ฮป t ฯ ฯ โ ๐ค๐ฆ๐ t (ฮป v โ ๐ค๐ฆ๐ (ฯ v) ฯ))
๐ค๐ฆ๐-comp = record
{ ฯ = id
; ฯ = ๐ค๐ฆ๐
; ฯ = ๐๐ง๐๐ฃ
; fโจ๐ฃโฉ = ๐ฅโโ ๐ฅโจ๐งโฉ
; fโจ๐โฉ = trans (๐ฅโโ ๐ฅโจ๐โฉ) ๐ฅโจ๐โฉ
; fโจ๐โฉ = ฮป{ {ฯ = ฯ}{ฯ}{t} โ begin
๐ค๐ฆ๐ (๐ค๐ฆ๐ (๐๐๐ t) ฯ) ฯ
โกโจ ๐ฅโโ ๐ฅโจ๐โฉ โฉ
๐ค๐ฆ๐ (๐๐๐ (str ๐แดฎ ๐ (โ
โ ๐ค๐ฆ๐ t) ฯ)) ฯ
โกโจ ๐ฅโจ๐โฉ โฉ
๐๐๐ (str ๐แดฎ ๐ (โ
โ ๐ค๐ฆ๐ (str ๐แดฎ ๐ (โ
โ ๐ค๐ฆ๐ t) ฯ)) ฯ)
โกหโจ congr (str-natโ ๐ค๐ฆ๐ (โ
โ ๐ค๐ฆ๐ t) ฯ) (ฮป - โ ๐๐๐ (str ๐แดฎ ๐ - ฯ)) โฉ
๐๐๐ (str ๐แดฎ ๐ (str ๐แดฎ ใ ๐ , ๐ ใ (โ
.Fโ (ฮป { h ฯ โ ๐ค๐ฆ๐ (h ฯ) }) (โ
โ ๐ค๐ฆ๐ t)) ฯ) ฯ)
โกหโจ congr โ
.homomorphism (ฮป - โ ๐๐๐ (str ๐แดฎ ๐ (str ๐แดฎ ใ ๐ , ๐ ใ - ฯ) ฯ)) โฉ
๐๐๐ (str ๐แดฎ ๐ (str ๐แดฎ ใ ๐ , ๐ ใ (โ
โ (ฮป{ t ฯ โ ๐ค๐ฆ๐ (๐ค๐ฆ๐ t ฯ)}) t) ฯ) ฯ)
โ }
; gโจ๐ฃโฉ = ๐ฅโจ๐งโฉ
; gโจ๐โฉ = ๐ฅโจ๐โฉ
; gโจ๐โฉ = ฮป{ {ฯ = ฯ}{ฯ}{t} โ begin
๐ค๐ฆ๐ (๐๐๐ t) (ฮป v โ ๐ค๐ฆ๐ (ฯ v) ฯ)
โกโจ ๐ฅโจ๐โฉ โฉ
๐๐๐ (str ๐แดฎ ๐ (โ
โ ๐ค๐ฆ๐ t) (ฮป v โ ๐ค๐ฆ๐ (ฯ v) ฯ))
โกโจ cong ๐๐๐ (str-dist ๐ ๐ค๐ฆ๐แถ (โ
โ ๐ค๐ฆ๐ t) (ฮป {ฯ} z โ ฯ z) ฯ) โฉ
๐๐๐ (str ๐แดฎ ๐ (str ๐แดฎ ใ ๐ , ๐ ใ (โ
.Fโ (precomp ๐ ๐ค๐ฆ๐) (โ
โ ๐ค๐ฆ๐ t)) ฯ) ฯ)
โกหโจ congr โ
.homomorphism (ฮป - โ ๐๐๐ (str ๐แดฎ ๐ (str ๐แดฎ ใ ๐ , ๐ ใ - ฯ) ฯ)) โฉ
๐๐๐ (str ๐แดฎ ๐ (str ๐แดฎ ใ ๐ , ๐ ใ (โ
โ (ฮป{ t ฯ ฯ โ ๐ค๐ฆ๐ t (ฮป v โ ๐ค๐ฆ๐ (ฯ v) ฯ)}) t) ฯ) ฯ)
โ }
} where open โก-Reasoning ; open Substitution
๐แต : Mon ๐
๐แต = record
{ ฮท = ๐ง๐๐ฃ
; ฮผ = ๐ค๐ฆ๐
; lunit = Substitution.๐ฅโจ๐งโฉ
; runit = ฮป{ {t = t} โ trans (๐ฅ๐ฃ๐๐ง-ฮทโ๐ค๐๐ ๐แดฎ ๐แต id refl) ๐ค๐๐-id }
; assoc = ฮป{ {t = t} โ MapEqโ.โ ๐ค๐ฆ๐-comp t }
}
open Mon ๐แต using ([_/] ; [_,_/]โ ; lunit ; runit ; assoc) public
๐แดน : CoalgMon ๐
๐แดน = record { แดฎ = ๐แดฎ ; แต = ๐แต ; ฮท-compat = refl ; ฮผ-compat = ฮป{ {t = t} โ compat t } }