proposition: Lemma funcalg_alg_funcalg (a: algebra σ) : functoralgebra_to_algebra (algebra_to_functoralgebra a) = a.
proof: 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.
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