Lemma squash_map_uniqueness {X S} (ip : isaset S) (g g' : ∥ X ∥ -> S) : g ∘ squash_element ~ g' ∘ squash_element -> g ~ g'. Proof. intros h. set ( Q := λ y, g y = g' y ). unfold homot. apply (@factor_dep_through_squash X). intros y. apply ip. intro x. apply h. Qed.