proposition: Lemma path_oppreserving_ap_operation (f : ∀ s, A s → B s) {w : SymbolType σ} (a : FamilyProd A (dom_symboltype w)) (α : Operation A w) (β : Operation B w) (P : OpPreserving f α β) : f (cod_symboltype w) (ap_operation α a) = ap_operation β (map_family_prod f a).
proof: Proof. induction w. - assumption. - destruct a as [x a]. apply IHw. apply P. Defined.
imports: HoTT.Classes.interfaces.ua_setalgebra HoTT.Types HoTT.Tactics