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