Theorem surjectionisepitosets {X Y Z : UU} (f : X -> Y) (g1 g2 : Y -> Z) (is1 : issurjective f) (is2 : isaset Z) (isf : ∏ x : X, g1 (f x) = g2 (f x)) : ∏ y : Y, g1 y = g2 y. Proof. intros. set (P1:= make_hProp (paths (g1 y) (g2 y)) (is2 (g1 y) (g2 y))). unfold issurjective in is1. assert (s1: (hfiber f y)-> paths (g1 y) (g2 y)). { intro X1. induction X1 as [t x ]. induction x. apply (isf t). } assert (s2: ishinh (paths (g1 y) (g2 y))) by apply (hinhfun s1 (is1 y)). set (is3 := is2 (g1 y) (g2 y)). simpl in is3. apply (@hinhuniv (paths (g1 y) (g2 y)) (make_hProp _ is3)). - intro X1. assumption. - assumption. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.