{w : SymbolType σ} (f : Operation A w) : Type := forall (a b : DomOperation A w), (forall i : Arity w, Φ (sorts_dom w i) (a i) (b i)) -> Φ (sort_cod w) (f a) (f b). Class OpsCompatible : Type := ops_compatible : forall (u : Symbol σ), u.#A. Global Instance trunc_ops_compatible `{Funext} {n : trunc_index} `{!forall s x y, IsTrunc n (Φ s x y)} : IsTrunc n OpsCompatible. Proof. apply istrunc_forall. Defined.
Require Import