proposition: Lemma isofhlevelhvec {m: nat} {n: nat} (v: vec UU n) (levels: hvec (vec_map (isofhlevel m) v)) : isofhlevel m (hvec v).
proof: Proof. revert n v levels. refine (vec_ind _ _ _). - intro. apply isofhlevelcontr. apply iscontrunit. - intros x n xs IHxs levels. simpl. apply isofhleveldirprod. + apply (pr1 levels). + apply (IHxs (pr2 levels)). Defined.
imports: UniMath.Foundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors