Corollary UniqueConstruction_to_weq {X Y:UU} (f:X->Y) : UniqueConstruction f -> isweq f. Proof. intros bij. assert (sur := pr1 bij). assert (inj := pr2 bij). use (isweq_iso f). - intros y. exact (pr1 (sur y)). - intros. simpl. simpl in inj. apply inj. exact (pr2 (sur (f x))). - intros. simpl. exact (pr2 (sur y)). Defined.