proposition: Lemma path_homomorphism_ap_operation (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: Proof. intros u a. by apply path_oppreserving_ap_operation. Defined.
imports: HoTT.Classes.interfaces.ua_setalgebra HoTT.Types HoTT.Tactics