proposition: Lemma squash_map_epi {X S} (ip : isaset S) (g g' : ∥ X ∥ -> S) : g ∘ squash_element = g'∘ squash_element -> g = g'.
proof: Proof. intros e. apply funextsec. apply squash_map_uniqueness. exact ip. intro x. induction e. apply idpath. Qed.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions