proposition: Lemma isepi_issurj : IsSurjection f.
proof: Proof. intros y. pose (i := isepi'_contr_cone _ epif). assert (X0 : forall x : setcone f, fam x = fam (setcone_point f)). { intros. apply contr_dom_equiv. apply i. } specialize (X0 (tr (push (inl y)))). simpl in X0. unfold IsConnected. refine (transport (fun A => Contr A) (ap trunctype_type X0)^ _); exact _. Defined.
imports: Basics Types TruncType ReflectiveSubuniverse Colimits.Pushout Truncations.Core HIT.SetCone