Definition h1const_is_vec {A: UU} {n: nat} (v: vec A n) (B: UU) : hvec (vec_map (λ _, B) v) = vec B n. Proof. induction n. - apply idpath. - simpl. apply maponpaths. apply IHn. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.