proposition: Corollary isofhlevelweqb (n : nat) {X Y : UU} (f : X ≃ Y) : isofhlevel n Y -> isofhlevel n X.
proof: Proof. intros X0. apply (hlevelretract n (invmap f) f (homotinvweqweq f)). assumption. Defined.
imports: UniMath.Foundations.PartA