{D: Diagram G} `(f: Q <~> Q') : IsColimit D Q -> IsColimit D Q'. Proof. intros HQ. srapply (Build_IsColimit (cocone_postcompose HQ f) _). apply cocone_postcompose_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.