Definition vec_map {A B : UU} (f : A → B) {n} (v : vec A n) : vec B n. Proof. induction n as [|m h]. - exact vnil. - eapply vcons. + exact (f (hd v)). + exact (h (tl v)). Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.