Definition squash_to_set {X Y : UU} (is : isaset Y) (f : X -> Y) : (∏ x x', f x = f x') -> ∥ X ∥ -> Y. Proof. intros e w. set (P := ∑ y, ∃ x, f x = y). assert (j : isaprop P). { apply isapropsubtype; intros y y' j j'. apply (squash_to_prop j). apply is. clear j; intros [j k]. apply (squash_to_prop j'). apply is. clear j'; intros [j' k']. intermediate_path (f j). exact (!k). intermediate_path (f j'). apply e. exact k'. } assert (p : P). { apply (squash_to_prop w). exact j. intro x0. exists (f x0). apply hinhpr. exists x0. apply idpath. } exact (pr1 p). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.