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.Semantics {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.Construction.Structure as Structure
open import SOAS.Abstract.Hom
import SOAS.Abstract.Coalgebra as ββ‘ ; open ββ‘.Sorted
import SOAS.Abstract.Box as β‘ ; open β‘.Sorted
open import SOAS.Metatheory.Algebra β
F
open Strength β
:Str
private
variable
Ξ Ξ Ξ Ξ : Ctx
Ξ± Ξ² : T
π« π¬ π : Familyβ
open Initial π:Init
open Object β₯ public renaming (πΆ to π ; Λ’ to πα΅)
open MetaAlg πα΅ public renaming (πππ to πππ ; π£ππ to π§ππ£ ; ππ£ππ to ππ§ππ£ ;
πββ to πββ ; πββ to πββ)
module Semantics (πα΅ : MetaAlg π) where
open Morphism (! {π β πα΅}) public renaming (π to π€ππ ; Λ’β to π€ππα΅β)
open MetaAlgβ π€ππα΅β public renaming (β¨πππβ© to β¨πβ© ; β¨π£ππβ© to β¨π§β© ; β¨ππ£ππβ© to β¨πβ©)
open MetaAlg πα΅
module π = MetaAlg πα΅
eq : {g h : π βΎΜ£ π} (gα΅ : MetaAlgβ πα΅ πα΅ g) (hα΅ : MetaAlgβ πα΅ πα΅ h) (t : π Ξ± Ξ)
β g t β‘ h t
eq {g = g}{h} gα΅ hα΅ t = !-uniqueβ (g β gα΅) (h β hα΅) {x = t}
π€ππ! : {g : π βΎΜ£ π}(gα΅ : MetaAlgβ πα΅ πα΅ g)(t : π Ξ± Ξ) β π€ππ t β‘ g t
π€ππ! {g = g} gα΅ t = !-unique (g β gα΅) {x = t}
eq-id : {g : π βΎΜ£ π} (gα΅ : MetaAlgβ πα΅ πα΅ g) (t : π Ξ± Ξ) β
g t β‘ t
eq-id gα΅ t = Semantics.eq πα΅ gα΅ (idα΅ πα΅) t
π€ππ-id : {t : π Ξ± Ξ} β Semantics.π€ππ πα΅ t β‘ t
π€ππ-id {t = t} = eq-id (Semantics.π€ππα΅β πα΅) t