{σ} (A : Carriers σ) (w : SymbolType σ) : Type := match w with | [:s:] => A s | s ::: w' => A s → A w' end. Global Instance trunc_operation `{Funext} {σ : Signature} (A : Carriers σ) {n} `{!∀ s, IsTrunc n (A s)} (w : SymbolType σ) : IsTrunc n ( A w). Proof. induction w; exact _. Defined.
Require Import Import ne_list.notations.