Definition h2map_makehvec_basevecfill {A: UU} {n: nat} {a: A} {P: A → UU} {h1v: hvec (vec_map P (vec_fill a n))} {Q: ∏ (a: A) (p: P a), UU} {R: ∏ (a: A) (p: P a), UU} (f: ∏ (a: A) (p: P a), Q a p → R a p) (h2v: hvec (h1map_vec Q h1v)) : h2map f h2v = make_hvec (λ i, invweq (eqweqmap (hel_h1map_vec_vec_fill R h1v i)) (f _ _ (eqweqmap (hel_h1map_vec_vec_fill Q h1v i) (hel h2v i)))). Proof. use (invmaponpathsweq helf_weq). simpl. use funextsec. intro i. etrans. { apply helh2map_basevecfill. } use pathsinv0. use hel_make_hvec. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.