proposition: Theorem isofhlevelsnweqtohlevelsn (n : nat) (X Y : UU) (is : isofhlevel (S n) Y) : isofhlevel (S n) (X ≃ Y).
proof: Proof. intros. apply (isofhlevelsninclb n _ (isinclpr1weq _ _)). apply impred. intro. exact is. Defined.
imports: UniMath.Foundations.PartC