Definition helh2map {A: UU} {n: nat} {v: vec A n} {P: A → UU} {h1v: hvec (vec_map P v)} {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 R h1v i)) (f _ _ (eqweqmap (hel_h1map_vec Q h1v i) (hel h2v i)))). Proof. revert n v f h1v h2v i. refine (vec_ind _ _ _ ). - intros f h1v h2v i. use fromstn0. exact i. - intros x n v X f h1v h2v i. induction i as [j jlt]. induction j as [| k]. * apply idpath. * use X. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.