Definition h1const_vec_h1const {A: UU} {n: nat} {B: A} {P: A → UU} (hv: hvec (vec_map P (vec_fill B n)) ) : vec_to_h1const (h1const_to_vec hv) = hv. Proof. induction n. - induction hv. apply idpath. - simpl in hv. simpl. change hv with (pr1 hv ::: pr2 hv)%hvec. apply maponpaths. 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.