Lemma epiissurjectiontosets {A B : UU} (p : A -> B) (isB:isaset B) (epip : ∏ (C:hSet) (g1 g2:B->C), (∏ x : A, g1 (p x) = g2 (p x)) -> (∏ y : B, g1 y = g2 y)) : issurjective p. Proof. intros. assert(pred_set : isaset (B -> hProp)). { apply (isaset_set_fun_space _ (make_hSet _ isasethProp)). } specialize (epip (make_hSet _ pred_set) (λ b x, ∥ ∑ y : hfiber p b, x = p (pr1 y) ∥ ) (λ b x, make_hProp (x = b) (isB x b)) ). lapply epip. - intro h. intro y. specialize (h y). apply toforallpaths in h. specialize (h y). cbn in h. match type of h with _ = ?type_witn => set (typ:= type_witn) in h end. assert (witness:typ ). { apply idpath. } revert witness. rewrite <- h. apply hinhfun. intro h'. exact (pr1 h'). - intro b. apply funextfun. intro x; cbn. apply weqtopathshProp. apply logeqweq. + apply hinhuniv. intros [y eqx]. rewrite eqx. apply (hfiberpr2 _ _ y). + intro eqx. apply hinhpr. use tpair. * exists b. apply idpath. * exact eqx. Qed.
Require Import UniMath.Foundations.UnivalenceAxiom.