Definition squash_pairs_to_set {Y : UU} (F : Y -> UU) : (isaset Y) -> (∏ y y', F y -> F y' -> y = y') -> (∃ y, F y) -> Y. Proof. intros is e. set (P := ∑ y, ∥ F y ∥). assert (iP : isaprop P). { apply isapropsubtype. intros y y' f f'. apply (squash_to_prop f). apply is. clear f; intro f. apply (squash_to_prop f'). apply is. clear f'; intro f'. apply e. - assumption. - assumption. } intros w. assert (p : P). { apply (squash_to_prop w). exact iP. clear w; intro w. exact (pr1 w,,hinhpr (pr2 w)). } clear w. exact (pr1 p). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.