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