{X Y} (f:X->Y): isepi f -> issurj f. Proof. intros epif y. set (g :=fun _:Y => Unit_hp). set (h:=(fun y:Y => (hp (hexists (fun _ : Unit => {x:X & y = (f x)})) _ ))). assert (X1: g o f = h o f ). - apply path_forall. intro x. apply path_equiv_biimp_rec;[|done]. intros _ . apply min1. exists tt. by (exists x). - specialize (epif _ g h). specialize (epif X1). clear X1. set (p:=apD10 epif y). apply (@minus1Trunc_map (sig (fun _ : Unit => sig (fun x : X => y = f x)))). + intros [ _ [x eq]]. exists x. by symmetry. + apply (transport hproptype p tt). Defined.
Require Import Basics. Require Import Types. Require Import TruncType. Require Import ReflectiveSubuniverse. Require Import Colimits.Pushout Truncations.Core HIT.SetCone.