{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 → (α x) end. Global Instance trunc_closed_under_op {n} `{∀ s x, IsTrunc n (P s x)} {w : SymbolType σ} (α : Operation A w) : IsTrunc n ( α). Proof. induction w; cbn; exact _. Qed.
Require Import Import algebra_notations ne_list.notations. Import subalgebra_notations.