proposition: Theorem isapropisofhlevel (n : nat) (X : UU) : isaprop (isofhlevel n X).
proof: Proof. revert X. induction n as [ | n IHn ]. - apply isapropiscontr. - intro X. apply impred. intros t. apply impred. intros t0. apply IHn. Defined.
imports: UniMath.Foundations.PartC