proposition: Corollary isofhlevelfromfun (n : nat) (X : UU) : isofhlevelf n (λ x : X, tt) -> isofhlevel n X.
proof: Proof. intros is. apply (isofhlevelweqf n (weqhfibertounit X) (is tt)). Defined.
imports: UniMath.Foundations.PartA