Lemma hvec_vec_fill {A: UU} {n: nat} : hvec (vec_fill A n) = vec A n. Proof. induction n. - apply idpath. - simpl. apply maponpaths. assumption. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.