fact: Definition Build_span_cocone {f : A -> B} {g : A -> C} {Z : Type} (inl' : B -> Z) (inr' : C -> Z) (pp' : inl' o f == inr' o g) : Cocone (span f g) Z.
imports: Basics Types Diagrams.Graph Diagrams.Diagram Diagrams.Span Diagrams.Cocone Colimits.Colimit