Lemma isweqcontrprop (X Y : UU) (f : X → Y) : iscontr X → isaprop Y → isweq f. Proof. intros HX HY. apply isweqimplimpl. - intros. apply HX. - apply isapropifcontr. apply HX. - apply HY. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.PartB.