fact: Definition OpCompatible {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).
imports: HoTT.HProp HoTT.Classes.interfaces.canonical_names HoTT.Classes.interfaces.ua_algebra