proposition: Theorem isapropisweq {X Y : UU} (f : X -> Y) : isaprop (isweq f).
proof: Proof. intros. unfold isweq. apply (impred (S O) (λ y : Y, iscontr (hfiber f y)) (λ y : Y, isapropiscontr (hfiber f y))). Defined.
imports: UniMath.Foundations.PartC