equiv_isepi_isepi' {X Y} f : @isepi X Y f <~> @isepi' X Y f. Proof. unfold isepi, isepi'. apply (@equiv_functor_forall' _ _ _ _ _ (equiv_idmap _)); intro Z. apply (@equiv_functor_forall' _ _ _ _ _ (equiv_idmap _)); intro g. unfold equiv_idmap; simpl. refine (transitivity (@equiv_sig_ind _ (fun h : Y -> Z => g o f = h o f) (fun h => g = h.1)) _). apply equiv_iff_hprop. { intro hepi. nrapply (Build_Contr _ (g; idpath)). intro xy; specialize (hepi xy). apply path_sigma_uncurried. exists hepi. apply path_ishprop. } { intros hepi xy. exact (ap pr1 ((contr (g; 1))^ @ contr xy)). } Defined.
Require Import Basics. Require Import Types. Require Import TruncType. Require Import ReflectiveSubuniverse. Require Import Colimits.Pushout Truncations.Core HIT.SetCone.