{w : SymbolType σ} (f : Operation A w) : Type := ∀ (a b : FamilyProd A (dom_symboltype w)), for_all_2_family_prod A A Φ a b -> Φ (cod_symboltype w) (ap_operation f a) (ap_operation f b). Class OpsCompatible : Type := ops_compatible : ∀ (u : Symbol σ), u.#A. Global Instance trunc_ops_compatible `{Funext} {n : trunc_index} `{!∀ s x y, IsTrunc n (Φ s x y)} : IsTrunc n OpsCompatible. Proof. apply istrunc_forall. Qed.
Require Import Import algebra_notations ne_list.notations.