Lemma h1const_to_vec_eta_unit' {f: sUU unit} {n: nat} {hv: hvec (vec_map (λ _ : unit, f tt) (vec_fill tt n))} : h1const_to_vec hv = h1const_to_vec (transportf (λ X, hvec (vec_map X (vec_fill tt n))) (eta_unit' f) hv). Proof. induction n. - apply idpath. - simpl. rewrite transportf_dirprod'. use total2_paths2. + simpl. rewrite (transportf_eta_unit'(P:=λ a: unit → UU, a tt)). apply idpath. + apply (IHn (pr2 hv)). 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.