proposition: Lemma issurj_isepi {X Y} (f:X->Y): IsSurjection f -> isepi f.
proof: Proof. intros sur ? ? ? ep. apply path_forall. intro y. specialize (sur y). pose (center (merely (hfiber f y))). apply (Trunc_rec (n:=-1) (A:=(sig (fun x : X => f x = y)))); try assumption. intros [x p]. set (p0:=apD10 ep x). transitivity (g (f x)). - by apply ap. - transitivity (h (f x));auto with path_hints. by apply ap. Qed.
imports: Basics Types TruncType ReflectiveSubuniverse Colimits.Pushout Truncations.Core HIT.SetCone