open import SOAS.Common
import SOAS.Families.Core
module SOAS.Metatheory.MetaAlgebra {T : Set}
(open SOAS.Families.Core {T})
(β
F : Functor π½amiliesβ π½amiliesβ)
(π : Familyβ) where
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
open import SOAS.Metatheory.Algebra β
F
private
variable
Ξ Ξ Ξ : Ctx
Ξ± : T
record MetaAlg (π : Familyβ) : Set where
field
πππ : β
π βΎΜ£ π
π£ππ : β βΎΜ£ π
ππ£ππ : π βΎΜ£ γ π , π γ
πββ : {πͺβ πͺβ : π Ξ± Ξ }{Ο : Ξ ~[ π ]β Ξ}
β πͺβ β‘ πͺβ
β ππ£ππ πͺβ Ο β‘ ππ£ππ πͺβ Ο
πββ refl = refl
πββ : {πͺ : π Ξ± Ξ }{Ο Ο : Ξ ~[ π ]β Ξ}
β ({Ο : T}(v : β Ο Ξ ) β Ο v β‘ Ο v)
β ππ£ππ πͺ Ο β‘ ππ£ππ πͺ Ο
πββ {πͺ = πͺ} p = cong (ππ£ππ πͺ) (dext p)
record MetaAlgβ {π β¬ : Familyβ}(πα΅ : MetaAlg π)(β¬α΅ : MetaAlg β¬)
(f : π βΎΜ£ β¬) : Set where
private module π = MetaAlg πα΅
private module β¬ = MetaAlg β¬α΅
field
β¨πππβ© : {t : β
π Ξ± Ξ} β f (π.πππ t) β‘ β¬.πππ (β
β f t)
β¨π£ππβ© : {v : β Ξ± Ξ} β f (π.π£ππ v) β‘ β¬.π£ππ v
β¨ππ£ππβ© : {πͺ : π Ξ± Ξ }{Ξ΅ : Ξ ~[ π ]β Ξ} β f (π.ππ£ππ πͺ Ξ΅) β‘ β¬.ππ£ππ πͺ (f β Ξ΅)
module MetaAlgebraStructure = Structure π½amiliesβ MetaAlg
MetaAlgebraCatProps : MetaAlgebraStructure.CategoryProps
MetaAlgebraCatProps = record
{ IsHomomorphism = MetaAlgβ
; id-hom = Ξ» {π}{πα΅} β record
{ β¨πππβ© = cong (πππ πα΅) (sym β
.identity)
; β¨π£ππβ© = refl
; β¨ππ£ππβ© = refl }
; comp-hom = Ξ»{ {πΆΛ’ = πα΅}{β¬α΅}{πα΅} g f gα΅β fα΅β β record
{ β¨πππβ© = trans (cong g (β¨πππβ© fα΅β))
(trans (β¨πππβ© gα΅β)
(cong (πππ πα΅) (sym β
.homomorphism)))
; β¨π£ππβ© = trans (cong g (β¨π£ππβ© fα΅β)) (β¨π£ππβ© gα΅β)
; β¨ππ£ππβ© = trans (cong g (β¨ππ£ππβ© fα΅β)) (β¨ππ£ππβ© gα΅β) }
}} where open MetaAlg ; open MetaAlgβ
module MetaAlgProps = MetaAlgebraStructure.CategoryProps MetaAlgebraCatProps
πetaAlgebras : Category 1β 0β 0β
πetaAlgebras = MetaAlgebraStructure.StructCat MetaAlgebraCatProps
module πetaAlg = Category πetaAlgebras
MetaAlgebra : Setβ
MetaAlgebra = πetaAlg.Obj
MetaAlgebraβ : MetaAlgebra β MetaAlgebra β Set
MetaAlgebraβ = πetaAlg._β_
idα΅ : {π : Familyβ} β (πα΅ : MetaAlg π) β MetaAlgβ πα΅ πα΅ id
idα΅ πα΅ = record { β¨πππβ© = cong (MetaAlg.πππ πα΅) (sym β
.identity)
; β¨π£ππβ© = refl ; β¨ππ£ππβ© = refl }