Lemma vec_map_comp {A B C: UU} (f: A → B) (g: B → C) {n: nat} (v: vec A n) : vec_map (funcomp f g) v = (funcomp (vec_map f) (vec_map g)) v. Proof. revert n v. refine (vec_ind _ _ _). - apply idpath. - intros x n xs HPxs. apply vecS_eq. + reflexivity. + apply HPxs. Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.