proposition: Lemma alg_funcalg_alg (a: algebra_ob F) : algebra_to_functoralgebra (functoralgebra_to_algebra a) = a.
proof: Proof. use total2_paths2_f. - apply idpath. - rewrite idpath_transportf. apply funextfun. intro X. simpl. rewrite vec_h1const_vec. rewrite el_make_vec_fun. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Induction.PolynomialFunctors UniMath.Induction.W.Core UniMath.Induction.W.Wtypes UniMath.Induction.FunctorAlgebras_legacy UniMath.Algebra.Universal.Signatures UniMath.Algebra.Universal.Algebras UniMath.Algebra.Universal.HVectors UniMath.Algebra.Universal.Terms