Lemma h1map_compose {A: UU} {n: nat} {v: vec A n} {P: A → UU} {Q: A → UU} {R: A → UU} (f: ∏ a: A, P a → Q a) (g: ∏ (a: A), Q a → R a) (h1v: hvec (vec_map P v)) : h1map g (h1map f h1v) = h1map (λ a: A, (g a) ∘ (f a)) h1v. Proof. revert n v h1v. refine (vec_ind _ _ _). - induction h1v. apply idpath. - simpl. intros x n xs IHxs h1v. apply maponpaths. apply (IHxs (pr2 h1v)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.