Definition vec (A : UU) (n : nat) : UU. Proof. induction n as [|n IHn]. - apply unit. - apply (A × IHn). Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.