proposition: Corollary isweqhomot_iff {X Y : UU} (f1 f2 : X -> Y) (h : f1 ~ f2) : isweq f1 <-> isweq f2.
proof: Proof. intros. split. - apply isweqhomot; assumption. - apply isweqhomot, invhomot; assumption. Defined.
imports: UniMath.Foundations.Preamble