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