proposition: Lemma oppreserving_prod_algebra_mapin {w : SymbolType σ} (f : ∀ (i:I) s, C s → A i s) (α : ∀ (i:I), Operation (A i) w) (β : Operation C w) (P : ∀ (i:I), OpPreserving (f i) β (α i)) : OpPreserving (def_prod_algebra_mapin f) β (op_prod_algebra I A w (λ i, α i)).
proof: Proof. induction w. - funext i. apply P. - intro x. apply IHw. intro i. apply P. Defined.
imports: HoTT.Types.Bool HoTT.Types.Forall HoTT.Classes.theory.ua_homomorphism