Lemma isofhlevelhvec {m: nat} {n: nat} (v: vec UU n) (levels: hvec (vec_map (isofhlevel m) v)) : isofhlevel m (hvec v). 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.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.