Definition hvec {n: nat} (v: vec UU n): UU. Proof. revert n v. exact (vec_ind (λ _ _, UU) unit (λ x _ _ IHv, x × IHv)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.