fact: Definition cocone_postcompose_inv `{D: Diagram G} {Q X} (H : IsColimit D Q) (C' : Cocone D X) : Q -> X := @equiv_inv _ _ _ (iscolimit_unicocone H X) C'.
imports: Basics Types Diagrams.Diagram Diagrams.Graph Diagrams.Cocone Diagrams.ConstantDiagram Colimits.Coeq