proposition: Lemma polynomial_alg_uncurried_equiv : polynomial_alg_uncurried ≃ (algebra_ob polynomial_functor).
proof: Proof. apply (weq_iso (λ p, (pr1 p,, uncurry (pr2 p))) (λ p, (pr1 p,, curry (pr2 p)))); try reflexivity. Defined.
imports: UniMath.Foundations.Preamble UniMath.Foundations.PartA UniMath.Foundations.UnivalenceAxiom UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.Induction.FunctorAlgebras_legacy UniMath.Induction.FunctorCoalgebras_legacy UniMath.CategoryTheory.Categories.Type.Core