{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. Proof. srapply Build_Cocone. - intros [|[]]; [ exact (inr' o g) | exact inl' | exact inr' ]. - intros [u|b] [u'|b'] []; cbn. destruct b'. + exact pp'. + reflexivity. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Graph. Require Import Diagrams.Diagram. Require Import Diagrams.Span. Require Import Diagrams.Cocone. Require Import Colimits.Colimit. Import Colimits.Pushout.