proposition: Corollary isweqhomot {X Y : UU} (f1 f2 : X -> Y) (h : f1 ~ f2) : isweq f1 -> isweq f2.
proof: Proof. intros x0. unfold isweq. intro y. apply (iscontrhfiberl2 f1 f2 h). apply x0. Defined.
imports: UniMath.Foundations.Preamble