`{Funext} {A B : HSet} (f : A -> B) : isepi' f -> Contr (setcone f). Proof. intros hepi. apply (Build_Contr _ (setcone_point _)). pose (alpha1 := @pglue A B Unit f (const_tt _)). pose (tot:= { h : B -> setcone f & tr o push o inl o f = h o f }). transparent assert (l : tot). { simple refine (tr o _ o inl; _). { refine push. } { refine idpath. } } pose (r := (@const B (setcone f) (setcone_point _); (ap (fun f => @tr 0 _ o f) (path_forall _ _ alpha1))) : tot). subst tot. assert (X : l = r). { let lem := constr:(fun X push' => hepi (Build_HSet (setcone f)) (tr o push' o @inl _ X)) in pose (lem _ push). refine (path_contr l r). } subst l r. pose (I0 b := ap10 (X ..1) b). refine (Trunc_ind _ _). pose (fun a : B + Unit => (match a as a return setcone_point _ = tr (push a) with | inl a' => (I0 a')^ | inr tt => idpath end)) as I0f. refine (Pushout_ind _ (fun a' => I0f (inl a')) (fun u => (I0f (inr u))) _). simpl. subst alpha1. intros. unfold setcone_point. subst I0. simpl. pose (X..2) as p. simpl in p. rewrite (transport_precompose f _ _ X..1) in p. assert (H':=concat (ap (fun x => ap10 x a) p) (ap10_ap_postcompose tr (path_arrow (pushl o f) (pushr o const_tt _) pglue) _)). rewrite ap10_path_arrow in H'. clear p. pose (concat (ap10_ap_precompose f (X ..1) a)^ H') as p. clearbody p. simpl in p. rewrite p. rewrite transport_paths_Fr. apply concat_Vp. Qed.
Require Import Basics. Require Import Types. Require Import TruncType. Require Import ReflectiveSubuniverse. Require Import Colimits.Pushout Truncations.Core HIT.SetCone.