Lemma h1map_path {A: UU} {n: nat} {v: vec A n} {P: A → UU} {Q: A → UU} (f: ∏ a: A, P a → Q a) (g: ∏ (a: A), P a → Q a) (h1v: hvec (vec_map P v)) (h2path: hvec (h1map_vec (λ a p, f a p = g a p) h1v)) : h1map f h1v = h1map g h1v. Proof. revert n v h1v h2path. refine (vec_ind _ _ _). - induction h1v. reflexivity. - simpl. intros x n xs IHxs h1v h2path. use map_on_two_paths. + exact (pr1 h2path). + exact (IHxs (pr2 h1v) (pr2 h2path)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.