{w : SymbolType σ} : Operation A w → Operation B w → Type := match w with | [:s:] => λ α β, f s α = β | s ::: y => λ α β, ∀ (x : A s), (α x) (β (f s x)) end. Global Instance trunc_oppreserving `{Funext} {n : trunc_index} `{!IsTruncAlgebra n.+1 B} {w : SymbolType σ} (α : Operation A w) (β : Operation B w) : IsTrunc n ( α β). Proof. induction w; exact _. Qed.
Require Import Import algebra_notations ne_list.notations.