{D1 D2 : Diagram G} (m : D1 ~d~ D2) {Q : Type} : IsColimit D2 Q -> IsColimit D1 Q. Proof. intros HQ. srapply (Build_IsColimit (cocone_precompose m HQ) _). apply cocone_precompose_equiv_universality, HQ. 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.