Definition helh2map_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)) (i:⟦ n ⟧) : hel (h2map f h2v) 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. revert n h1v h2v i. use hvec_ind_fixedv. - intros h1v h2v i. use fromstn0. exact i. - intros n IH h1v h2v i. induction i as [j jlt]. induction j as [| k]. * apply idpath. * use IH. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.