Definition algebra_to_functoralgebra (a: algebra σ) : algebra_ob F. Proof. induction a as [carrier ops]. unfold algebra_ob. exists (carrier tt). simpl. intro X. induction X as [nm subterms]. refine (ops nm _). apply vec_to_h1const. exact (make_vec 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.