Corollary set_bijection_to_weq {X Y : UU} (f : X -> Y) : UniqueConstruction f -> isaset Y -> isweq f. Proof. intros bij i y. set (sur := pr1 bij); set (inj := pr2 bij). use tpair. - exists (pr1 (sur y)). exact (pr2 (sur y)). - intro w. use total2_paths_f. + simpl. apply inj. intermediate_path y. * exact (pr2 w). * exact (! pr2 (sur y)). + induction w as [x e]; simpl. induction e. apply i. Defined.