Definition functoralgebra_to_algebra (FAlg: algebra_ob F) : algebra σ. Proof. induction FAlg as [carrier ops]. simpl in ops. exists (λ _, carrier). intro nm. intro subterms. apply h1const_to_vec in subterms. exact (ops (nm ,, el subterms)). 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.