proposition: Lemma ishprop_surjective_factor_aux : forall b, IsHProp (exists c : C, forall a, g a = b -> f a = c).
proof: Proof. intros. apply Sigma.ishprop_sigma_disjoint. intros c1 c2 E1 E2. generalize (@center _ (Esurj b)); apply (Trunc_ind _). intros [a p];destruct p. path_via (f a). Qed.
imports: HoTT.Types HoTT.Basics HoTT.Truncations.Core Modalities.Modality