Definition gtweq_sec (x:A) : (gterm σ)⋆ (arity x) ≃ (B x → U). Proof. unfold star. use (weqcomp helf_weq). use weqonsecfibers. intro i. use eqweqmap. use el_vec_map_vec_fill. 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.