proposition: Theorem isofhlevelsnweqfromhlevelsn (n : nat) (X Y : UU) (is : isofhlevel (S n) Y) : isofhlevel (S n) (Y ≃ X).
proof: Proof. intros. apply (isofhlevelweqf (S n) (weqinvweq X Y)). apply isofhlevelsnweqtohlevelsn. exact is. Defined.
imports: UniMath.Foundations.PartC