proposition: Lemma hlevel_total2 n {A : UU} {B : A → UU} : isofhlevel n (∑ (x :A), B x) → isofhlevel (S n) A → ∏ (x : A), isofhlevel n (B x).
proof: Proof. intros ic ia x. exact (isofhlevelweqf _ (invweq (ezweqpr1 _ _)) (isofhlevelffromXY _ _ ic ia _)). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics