fact: Fixpoint op_prod_algebra (w : SymbolType σ) : (∀ i, Operation (A i) w) → Operation carriers_prod_algebra w := match w return (∀ i, Operation (A i) w) → Operation carriers_prod_algebra w with | [:_:] => idmap | _ ::: g => λ f p, op_prod_algebra g (λ i, f i (p i)) end.
imports: HoTT.Types.Bool HoTT.Types.Forall HoTT.Classes.theory.ua_homomorphism