Definition h1map_vec {A: UU} {n: nat} {v: vec A n} {P: A → UU} {B: UU} (f: ∏ (a: A), P a → B) (h1v: hvec (vec_map P v)) : vec B n := h1lower (h1map f h1v).
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.