free (finEqSig σ) = Fin ∘ σ .snd
module _ {f a e n : Level} (σ : Sig f a) (τ : EqSig e n) where
-- TODO: refactor as (Tree σ Unit -> Tree σ X) × (Tree σ Unit -> Tree σ X) ?
seq : Type (ℓ-max (ℓ-max (ℓ-max f a) e) n)
seq = (e : τ .name) -> Tree σ (τ .free e) × Tree σ (τ .free e)
module _ {f a e n s : Level} {σ : Sig f a} {τ : EqSig e n} where
-- type of structure satisfying equations
-- TODO: refactor as a coequaliser
infix 30 _⊨_
_⊨_ : struct s σ -> (ε : seq σ τ) -> Type (ℓ-max s (ℓ-max e n))
𝔛 ⊨ ε = (eqn : τ .name) (ρ : τ .free eqn -> 𝔛 .carrier)
-> sharp σ 𝔛 ρ (ε eqn .fst) ≡ sharp σ 𝔛 ρ (ε eqn .snd)
https://api.github.com/pufferffish/agda-symmetries/blob/0ff92bdb19aba58e89e9690583a23f811cdcca95/Cubical/Structures/Eq.agda#L41