Lemma squash_map_epi {X S} (ip : isaset S) (g g' : ∥ X ∥ -> S) : g ∘ squash_element = g'∘ squash_element -> g = g'. Proof. intros e. apply funextsec. apply squash_map_uniqueness. exact ip. intro x. induction e. apply idpath. Qed.