{w : SymbolType σ} (α : Operation A w) (β : Operation B w) : Type := forall a : DomOperation A w, f (sort_cod w) (α a) = β (fun i => f (sorts_dom w i) (a i)). Global Instance hprop_oppreserving `{Funext} {w : SymbolType σ} (α : Operation A w) (β : Operation B w) : IsHProp ( α β). Proof. apply istrunc_forall. Qed.
Require Import