IsSurjection f. 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.
Require Import Basics. Require Import Types. Require Import TruncType. Require Import ReflectiveSubuniverse. Require Import Colimits.Pushout Truncations.Core HIT.SetCone.