open import SOAS.Common
import SOAS.Families.Core

-- Families with syntactic structure
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

-- A family with support for variables, metavariables, and β…€-algebra structure
record MetaAlg (π’œ : Familyβ‚›) : Set where

  field
    π‘Žπ‘™π‘”  : β…€ π’œ β‡ΎΜ£ π’œ
    π‘£π‘Žπ‘Ÿ  :   ℐ β‡ΎΜ£ π’œ
    π‘šπ‘£π‘Žπ‘Ÿ :   𝔛 β‡ΎΜ£ γ€– π’œ , π’œ γ€—

  -- Congruence in metavariable arguments
  π‘šβ‰ˆβ‚ : {π”ͺ₁ π”ͺβ‚‚ : 𝔛 Ξ± Ξ }{Οƒ : Ξ  ~[ π’œ ]↝ Ξ“}
      β†’ π”ͺ₁ ≑ π”ͺβ‚‚
      β†’ π‘šπ‘£π‘Žπ‘Ÿ π”ͺ₁ Οƒ ≑ π‘šπ‘£π‘Žπ‘Ÿ π”ͺβ‚‚ Οƒ
  π‘šβ‰ˆβ‚ refl = refl

  π‘šβ‰ˆβ‚‚ : {π”ͺ : 𝔛 Ξ± Ξ }{Οƒ Ο‚ : Ξ  ~[ π’œ ]↝ Ξ“}
      β†’ ({Ο„ : T}(v : ℐ Ο„ Ξ ) β†’ Οƒ v ≑ Ο‚ v)
      β†’ π‘šπ‘£π‘Žπ‘Ÿ π”ͺ Οƒ ≑ π‘šπ‘£π‘Žπ‘Ÿ π”ͺ Ο‚
  π‘šβ‰ˆβ‚‚ {π”ͺ = π”ͺ} p = cong (π‘šπ‘£π‘Žπ‘Ÿ π”ͺ) (dext p)

-- Meta-algebra homomorphism
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 ∘ Ξ΅)

-- Category of meta-algebras
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._β‡’_



-- Identity is a meta-algebra homomorphism
idᡃ : {π’œ : Familyβ‚›} β†’ (π’œα΅ƒ : MetaAlg π’œ) β†’ MetaAlgβ‡’ π’œα΅ƒ π’œα΅ƒ id
idᡃ π’œα΅ƒ = record { βŸ¨π‘Žπ‘™π‘”βŸ© = cong (MetaAlg.π‘Žπ‘™π‘” π’œα΅ƒ) (sym β…€.identity)
                ; βŸ¨π‘£π‘Žπ‘ŸβŸ© = refl ; βŸ¨π‘šπ‘£π‘Žπ‘ŸβŸ© = refl }