open import SOAS.Common
open import SOAS.Families.Core

-- Algebras for a signature endofunctor
module SOAS.Metatheory.Algebra {T : Set} (⅀F : Functor (𝔽amiliesₛ {T}) (𝔽amiliesₛ {T})) where


module ⅀ = Functor ⅀F

⅀ : Familyₛ → Familyₛ
⅀ = ⅀.₀

⅀₁ : {𝒳 𝒴 : Familyₛ} → 𝒳 ⇾̣ 𝒴 → ⅀ 𝒳 ⇾̣ ⅀ 𝒴
⅀₁ = Functor.₁ ⅀F