Definition alegbra_weq_functoralgebra: algebra σ ≃ algebra_ob F. Proof. apply (weq_iso algebra_to_functoralgebra functoralgebra_to_algebra). exact funcalg_alg_funcalg. exact alg_funcalg_alg. 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.