Lemma alg_funcalg_alg (a: algebra_ob F) : algebra_to_functoralgebra (functoralgebra_to_algebra a) = a. 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Induction.PolynomialFunctors. Require Import UniMath.Induction.W.Core. Require Import UniMath.Induction.W.Wtypes. Require Import UniMath.Induction.FunctorAlgebras_legacy. Require Import UniMath.Algebra.Universal.Signatures. Require Import UniMath.Algebra.Universal.Algebras. Require Import UniMath.Algebra.Universal.HVectors. Require Import UniMath.Algebra.Universal.Terms.