(f : ∀ s, A s → B s) `{!IsHomomorphism f} : ∀ (u : Symbol σ) (a : FamilyProd A (dom_symboltype (σ u))), f (cod_symboltype (σ u)) (ap_operation u.#A a) = ap_operation u.#B (map_family_prod f a). Proof. intros u a. by apply path_oppreserving_ap_operation. Defined.
Require Import Import algebra_notations ne_list.notations.