fact: Definition OpPreserving {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)).
imports: HoTT.Algebra.Universal.Algebra HoTT.WildCat.Core HoTT.Types