(Q : Type) (scct' : forall a (x : C a), Q) (sppt' : forall b (y : C (f b)), scct' (f b) y = scct' (g b) (D b y)) : sWtil -> Q. Proof. apply sig_ind. refine (Coeq_ind (fun w => P w -> Q) (fun a x => scct' a x) _). intros b. refine (dpath_arrow P (fun _ => Q) _ _ _ _). intros y. refine (transport_const _ _ @ _). refine (sppt' b _ @ ap _ _). refine ((transport_path_universe' P (cglue b) (D b) _ _)^). exact (Coeq_rec_beta_cglue _ _ _ _). Defined.
Require Import HoTT.Basics. Require Import Types.Paths Types.Forall Types.Sigma Types.Arrow Types.Universe. Require Import HoTT.Colimits.Coeq.