Lemma funcalg_alg_funcalg (a: algebra σ) : functoralgebra_to_algebra (algebra_to_functoralgebra a) = a. Proof. use total2_paths2_b. - apply eta_unit'. - apply funextsec. intro nm. apply funextfun. intro x. simpl. rewrite make_vec_el. rewrite h1const_to_vec_eta_unit'. rewrite h1const_vec_h1const. rewrite transportb_sec_constant. rewrite transportb_fun. rewrite (transportb_eta_unit'(P:=(λ x0 : unit → UU, x0 (sort nm)))). apply idpath. Defined.
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.