Theorem isofhlevelsnweqfromhlevelsn (n : nat) (X Y : UU) (is : isofhlevel (S n) Y) : isofhlevel (S n) (Y ≃ X). Proof. intros. apply (isofhlevelweqf (S n) (weqinvweq X Y)). apply isofhlevelsnweqtohlevelsn. exact is. Defined.