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