open import SOAS.Common
open import SOAS.Families.Core
open import Categories.Object.Initial
open import SOAS.Coalgebraic.Strength
import SOAS.Metatheory.MetaAlgebra

-- Substitution structure by initiality
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

-- Substitution is a ๐•‹-parametrised traversal into ๐•‹
module Substitution = Traversal ๐•‹แดฎ ๐•’๐•๐•˜ id ๐•ž๐•ง๐•’๐•ฃ

๐•ค๐•ฆ๐•“ : ๐•‹ โ‡พฬฃ ใ€– ๐•‹ , ๐•‹ ใ€—
๐•ค๐•ฆ๐•“ = Substitution.๐•ฅ๐•ฃ๐•’๐•ง

-- The renaming and algebra structures on ๐•‹ are compatible, so ๐•ค๐•ฆ๐•“ is coalgebraic
๐•ค๐•ฆ๐•“แถœ : Coalgebraic ๐•‹แดฎ ๐•‹แดฎ ๐•‹แดฎ ๐•ค๐•ฆ๐•“
๐•ค๐•ฆ๐•“แถœ = Travแถœ.๐•ฅ๐•ฃ๐•’๐•งแถœ ๐•‹แดฎ ๐•’๐•๐•˜ id ๐•ž๐•ง๐•’๐•ฃ ๐•‹แดฎ idแดฎโ‡’ Renaming.๐•ค๐•–๐•žแตƒโ‡’

module ๐•ค๐•ฆ๐•“แถœ = Coalgebraic ๐•ค๐•ฆ๐•“แถœ

-- Compatibility of renaming and substitution
compat : {ฯ : ฮ“ โ† ฮ”} (t : ๐•‹ ฮฑ ฮ“) โ†’ ๐•ฃ๐•–๐•Ÿ t ฯ โ‰ก ๐•ค๐•ฆ๐•“ t (๐•ง๐•’๐•ฃ โˆ˜ ฯ)
compat {ฯ = ฯ} t =  begin ๐•ฃ๐•–๐•Ÿ t ฯ           โ‰กห˜โŸจ ๐•ฅ๐•ฃ๐•’๐•ง-ฮทโ‰ˆid ๐•‹แดฎ id refl โŸฉ
                          ๐•ค๐•ฆ๐•“ (๐•ฃ๐•–๐•Ÿ t ฯ) ๐•ง๐•’๐•ฃ  โ‰กโŸจ ๐•ค๐•ฆ๐•“แถœ.fโˆ˜r โŸฉ
                          ๐•ค๐•ฆ๐•“ t (๐•ง๐•’๐•ฃ โˆ˜ ฯ)   โˆŽ where open โ‰ก-Reasoning

-- Substitution associativity law
๐•ค๐•ฆ๐•“-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

-- Coalgebraic monoid structure on ๐•‹
๐•‹แต : 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 } }