{G : Graph} {D : Diagram G} (P : Colimit D -> Type) (q : forall i x, P (colim i x)) (pp_q : forall (i j : G) (g: G i j) (x : D i), (@colimp G D i j g x) # (q j (D _f g x)) = q i x) : forall w, P w. Proof. srapply Coeq_ind. - intros [x i]. exact (q x i). - intros [[i x] [j f]]. cbn in f; cbn. apply moveR_transport_p. symmetry. exact (pp_q _ _ _ _). Defined.
Require Import Basics Types. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cocone. Require Import Diagrams.ConstantDiagram. Require Import Colimits.Coeq.