(Q : sWtil -> Type) (scct' : forall a x, Q (scct a x)) (sppt' : forall b y, (sppt b y) # (scct' (f b) y) = scct' (g b) (D b y)) : forall w, Q w. Proof. apply sig_ind. refine (Coeq_ind (fun w => forall x:P w, Q (w;x)) (fun a x => scct' a x) _). intros b. apply (dpath_forall P (fun a b => Q (a;b)) _ _ (cglue b) (scct' (f b)) (scct' (g b))). intros y. set (q := transport_path_universe' P (cglue b) (D b) (Coeq_rec_beta_cglue Type C (fun b0 : B => path_universe (D b0)) b) y). rewrite transportD_is_transport. refine (_ @ apD (scct' (g b)) q^). refine (moveL_transport_V (fun x => Q (scct (g b) x)) q _ _ _). rewrite transport_compose, <- transport_pp. refine (_ @ sppt' b y). apply ap10, ap. refine (whiskerL _ (ap_exist P (coeq (g b)) _ _ q) @ _). exact ((path_sigma_p1_1p' _ _ _)^). Defined.
Require Import HoTT.Basics. Require Import Types.Paths Types.Forall Types.Sigma Types.Arrow Types.Universe. Require Import HoTT.Colimits.Coeq.