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.Coalgebraic {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.Coalgebraic.Map
open import SOAS.Metatheory.Algebra {T} โ
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 Strength โ
:Str
module _ {๐ : Familyโ}(๐แต : Coalg ๐)(๐แต : MetaAlg ๐)
(open Semantics ๐แต)(open Coalg ๐แต)
(rแตโ : MetaAlgโ ๐แต (โกแต ๐แต) r) where
open MetaAlg ๐แต
open MetaAlgโ rแตโ
๐แดฎ : Coalgโ ๐
๐แดฎ = record { แต = ๐แต ; ฮท = ๐ฃ๐๐ ; rโฮท = cong (ฮป - โ - _) โจ๐ฃ๐๐โฉ }
๐ค๐๐โren : MapEqโ โแดฎ ๐๐๐ (ฮป t ฯ โ ๐ค๐๐ (๐ฃ๐๐ t ฯ))
(ฮป t ฯ โ r (๐ค๐๐ t) ฯ)
๐ค๐๐โren = record
{ ฯ = ๐ฃ๐๐
; ฯ = ๐๐ฃ๐๐
; fโจ๐ฃโฉ = trans (cong ๐ค๐๐ Renaming.๐ฅโจ๐งโฉ) โจ๐งโฉ
; fโจ๐โฉ = trans (cong ๐ค๐๐ Renaming.๐ฅโจ๐โฉ) โจ๐โฉ
; fโจ๐โฉ = ฮป{ {ฯ = ฯ}{t} โ begin
๐ค๐๐ (๐ฃ๐๐ (๐๐๐ t) ฯ)
โกโจ cong ๐ค๐๐ Renaming.๐ฅโจ๐โฉ โฉ
๐ค๐๐ (๐๐๐ (str โแดฎ ๐ (โ
โ ๐ฃ๐๐ t) ฯ))
โกโจ โจ๐โฉ โฉ
๐๐๐ (โ
โ ๐ค๐๐ (str โแดฎ ๐ (โ
โ ๐ฃ๐๐ t) ฯ))
โกหโจ cong ๐๐๐ (str-natโ ๐ค๐๐ (โ
โ ๐ฃ๐๐ t) ฯ) โฉ
๐๐๐ (str โแดฎ ๐ (โ
.Fโ (ฮป { hโฒ ฯ โ ๐ค๐๐ (hโฒ ฯ) }) (โ
โ ๐ฃ๐๐ t)) ฯ)
โกหโจ congr โ
.homomorphism (ฮป - โ ๐๐๐ (str โแดฎ ๐ - ฯ)) โฉ
๐๐๐ (str โแดฎ ๐ (โ
โ (ฮป{ t ฯ โ ๐ค๐๐ (๐ฃ๐๐ t ฯ)}) t) ฯ)
โ }
; gโจ๐ฃโฉ = trans (rโโ โจ๐งโฉ) (cong (ฮป - โ - _) โจ๐ฃ๐๐โฉ)
; gโจ๐โฉ = trans (rโโ โจ๐โฉ) (cong (ฮป - โ - _) โจ๐๐ฃ๐๐โฉ)
; gโจ๐โฉ = ฮป{ {ฯ = ฯ}{t} โ begin
r (๐ค๐๐ (๐๐๐ t)) ฯ
โกโจ rโโ โจ๐โฉ โฉ
r (๐๐๐ (โ
โ ๐ค๐๐ t)) ฯ
โกโจ cong (ฮป - โ - ฯ) โจ๐๐๐โฉ โฉ
๐๐๐ (str โแดฎ ๐ (โ
โ r (โ
โ ๐ค๐๐ t)) ฯ)
โกหโจ congr โ
.homomorphism (ฮป - โ ๐๐๐ (str โแดฎ ๐ - ฯ)) โฉ
๐๐๐ (str โแดฎ ๐ (โ
โ (ฮป{ t ฯ โ r (๐ค๐๐ t) ฯ}) t) ฯ)
โ }
} where open โก-Reasoning
๐ค๐๐แตโ : Coalgโ ๐แต ๐แต ๐ค๐๐
๐ค๐๐แตโ = record { โจrโฉ = ฮป{ {t = t} โ MapEqโ.โ ๐ค๐๐โren t } }
๐ค๐๐แดฎโ : Coalgโโ ๐แดฎ ๐แดฎ ๐ค๐๐
๐ค๐๐แดฎโ = record { แตโ = ๐ค๐๐แตโ ; โจฮทโฉ = โจ๐งโฉ }
module Travแถ {๐ซ ๐ : Familyโ}(๐ซแดฎ : Coalgโ ๐ซ)(๐๐๐ : โ
๐ โพฬฃ ๐)
(ฯ : ๐ซ โพฬฃ ๐)(ฯ : ๐ โพฬฃ ใ ๐ , ๐ ใ) where
open Coalgโ ๐ซแดฎ
open Traversal ๐ซแดฎ ๐๐๐ ฯ ฯ
๐ฅ๐ฃ๐๐งแตโ : Coalgโ ๐แต Travแต ๐ฅ๐ฃ๐๐ง
๐ฅ๐ฃ๐๐งแตโ = ๐ค๐๐แตโ Travแต Travแต record
{ โจ๐๐๐โฉ = ฮป{ {t = t} โ dextยฒ (ฮป ฯ ฯ โ cong ๐๐๐ (str-dist ๐ (jแถ ๐ซแดฎ) t ฯ ฯ)) }
; โจ๐ฃ๐๐โฉ = refl ; โจ๐๐ฃ๐๐โฉ = refl }
๐ฅ๐ฃ๐๐งแดฎโ : Coalgโโ ๐แดฎ Travแดฎ ๐ฅ๐ฃ๐๐ง
๐ฅ๐ฃ๐๐งแดฎโ = record { แตโ = ๐ฅ๐ฃ๐๐งแตโ ; โจฮทโฉ = โจ๐งโฉ }
module _ (๐แดฎ : Coalgโ ๐)(ฯแดฎ : Coalgโโ ๐ซแดฎ ๐แดฎ ฯ)
(๐rแต : MetaAlgโ ๐แต (โกแต ๐แต) (Coalgโ.r ๐แดฎ)) where
private module ๐แดฎ = Coalgโ ๐แดฎ
private module ฯแดฎ = Coalgโโ ฯแดฎ
private module ๐rแต = MetaAlgโ ๐rแต
rโ๐ฅ๐ฃ๐๐ง : MapEqโ ๐ซแดฎ โแดฎ ๐๐๐ (ฮป t ฯ ฯฑ โ ๐แดฎ.r (๐ฅ๐ฃ๐๐ง t ฯ) ฯฑ)
(ฮป t ฯ ฯฑ โ ๐ฅ๐ฃ๐๐ง t (ฮป v โ r (ฯ v) ฯฑ))
rโ๐ฅ๐ฃ๐๐ง = record
{ ฯ = ๐แดฎ.ฮท
; ฯ = ฮป v โ ๐แดฎ.r (ฯ v)
; ฯ = ฯ
; fโจ๐ฃโฉ = ๐แดฎ.rโโ ๐ฅโจ๐งโฉ
; fโจ๐โฉ = trans (๐แดฎ.rโโ ๐ฅโจ๐โฉ) (cong (ฮป - โ - _) ๐rแต.โจ๐๐ฃ๐๐โฉ)
; fโจ๐โฉ = ฮป{ {ฯ = ฯ}{ฯฑ}{t} โ begin
๐แดฎ.r (๐ฅ๐ฃ๐๐ง (๐๐๐ t) ฯ) ฯฑ
โกโจ ๐แดฎ.rโโ ๐ฅโจ๐โฉ โฉ
๐แดฎ.r (๐๐๐ (str ๐ซแดฎ ๐ (โ
โ ๐ฅ๐ฃ๐๐ง t) ฯ)) ฯฑ
โกโจ cong (ฮป - โ - ฯฑ) ๐rแต.โจ๐๐๐โฉ โฉ
๐๐๐ (str โแดฎ ๐ (โ
.Fโ ๐แดฎ.r (str ๐ซแดฎ ๐ (โ
.Fโ ๐ฅ๐ฃ๐๐ง t) ฯ)) ฯฑ)
โกหโจ congr (str-natโ ๐แดฎ.r (โ
.Fโ ๐ฅ๐ฃ๐๐ง t) ฯ) (ฮป - โ ๐๐๐ (str โแดฎ ๐ - ฯฑ)) โฉ
๐๐๐ (str โแดฎ ๐ (str ๐ซแดฎ (โก ๐) (โ
.Fโ (ฮป { h ฯ โ ๐แดฎ.r (h ฯ) }) (โ
.Fโ ๐ฅ๐ฃ๐๐ง t)) ฯ) ฯฑ)
โกหโจ congr โ
.homomorphism (ฮป - โ ๐๐๐ (str โแดฎ ๐ (str ๐ซแดฎ (โก ๐) - ฯ) ฯฑ)) โฉ
๐๐๐ (str โแดฎ ๐ (str ๐ซแดฎ (โก ๐) (โ
โ (ฮป{ t ฯ โ ๐แดฎ.r (๐ฅ๐ฃ๐๐ง t ฯ)}) t) ฯ) ฯฑ)
โ }
; gโจ๐ฃโฉ = trans ๐ฅโจ๐งโฉ ฯแดฎ.โจrโฉ
; gโจ๐โฉ = ๐ฅโจ๐โฉ
; gโจ๐โฉ = ฮป{ {ฯ = ฯ}{ฯฑ}{t} โ begin
๐ฅ๐ฃ๐๐ง (๐๐๐ t) (ฮป x โ r (ฯ x) ฯฑ)
โกโจ ๐ฅโจ๐โฉ โฉ
๐๐๐ (str ๐ซแดฎ ๐ (โ
โ ๐ฅ๐ฃ๐๐ง t) (ฮป x โ r (ฯ x) ฯฑ))
โกโจ cong ๐๐๐ (str-dist ๐ (rแถ ๐ซแดฎ) (โ
โ ๐ฅ๐ฃ๐๐ง t) ฯ ฯฑ) โฉ
๐๐๐ (str โแดฎ ๐ (str ๐ซแดฎ (โก ๐) (โ
.Fโ (precomp ๐ r) (โ
โ ๐ฅ๐ฃ๐๐ง t)) ฯ) ฯฑ)
โกหโจ congr โ
.homomorphism (ฮป - โ ๐๐๐ (str โแดฎ ๐ (str ๐ซแดฎ (โก ๐) - ฯ) ฯฑ)) โฉ
๐๐๐ (str โแดฎ ๐ (str ๐ซแดฎ (โก ๐) (โ
โ (ฮป{ t ฯ ฯฑ โ ๐ฅ๐ฃ๐๐ง t (ฮป v โ r (ฯ v) ฯฑ)}) t) ฯ) ฯฑ)
โ }
} where open โก-Reasoning
๐ฅ๐ฃ๐๐งแถ : Coalgebraic ๐แดฎ ๐ซแดฎ ๐แดฎ ๐ฅ๐ฃ๐๐ง
๐ฅ๐ฃ๐๐งแถ = record { rโf = ฮป{ {ฯ = ฯ}{ฯฑ}{t = t} โ MapEqโ.โ rโ๐ฅ๐ฃ๐๐ง t }
; fโr = ฮป{ {ฯ = ฯ}{ฯ}{t = t} โ cong (ฮป - โ - ฯ) (Coalgโ.โจrโฉ ๐ฅ๐ฃ๐๐งแตโ {ฯ = ฯ}{t = t}) }
; fโฮท = trans ๐ฅโจ๐งโฉ ฯแดฎ.โจฮทโฉ }