proposition: Theorem isapropisofhlevelf (n : nat) {X Y : UU} (f : X -> Y) : isaprop (isofhlevelf n f).
proof: Proof. intros. unfold isofhlevelf. apply impred. intro y. apply isapropisofhlevel. Defined.
imports: UniMath.Foundations.PartC