fact: Fixpoint ClosedUnderOp {w : SymbolType σ} : Operation A w → Type := match w with | [:s:] => P s | s ::: w' => λ (α : A s → Operation A w'), ∀ (x : A s), P s x → ClosedUnderOp (α x) end.
imports: HoTT.HProp HoTT.Types HoTT.Classes.theory.ua_homomorphism