Definition vec_fill {A: UU} (a: A): ∏ n: nat, vec A n := nat_rect (λ n: nat, vec A n) [()] (λ (n: nat) (v: vec A n), a ::: v).
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.