Lemma isofhlevelvec {n} (is1 : isofhlevel n A) k : isofhlevel n (vec A k). Proof. induction k as [|k IH]. - apply isofhlevelcontr, iscontrunit. - apply isofhleveldirprod. + apply is1. + apply IH. Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.