Lemma h2lower_h1map_h1lift {A: UU} {n: nat} {v: vec A n} {P: A → UU} {Q: ∏ (a: A), UU} (f: ∏ (a: A), P a → Q a) (h1v: hvec (vec_map P v)) : h2lower (h2map (λ a p _, f a p) (h1lift h1v)) = h1map f h1v. Proof. revert n v h1v. refine (vec_ind _ _ _). - reflexivity. - intros x n xs IHxs h1v. simpl. apply maponpaths. exact (IHxs (pr2 h1v)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.