Definition vec_zip {A B: UU} {n: nat} (v1: vec A n) (v2: vec B n): vec (A × B) n. Proof. induction n. - exact [()]. - induction v1 as [x1 xs1]. induction v2 as [x2 xs2]. exact ((x1 ,, x2) ::: IHn xs1 xs2). Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.