proposition: Lemma squash_map_uniqueness {X S} (ip : isaset S) (g g' : ∥ X ∥ -> S) : g ∘ squash_element ~ g' ∘ squash_element -> g ~ g'.
proof: 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.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions