{G : Graph} {D : Diagram G} (P : Type) (C : Cocone D P) (i j : G) (g: G i j) (x: D i) : ap (Colimit_rec P C) (colimp i j g x) = legs_comm C i j g x. Proof. rapply (cancelL (transport_const (colimp i j g x) _)). srapply ((apD_const (Colimit_ind (fun _ => P) C _) (colimp i j g x))^ @ _). srapply (Colimit_ind_beta_colimp (fun _ => P) C _ i j g x). 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.