{X Y} (f:X->Y): IsSurjection f -> isepi f. 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.
Require Import Basics. Require Import Types. Require Import TruncType. Require Import ReflectiveSubuniverse. Require Import Colimits.Pushout Truncations.Core HIT.SetCone.