(P: Type) (l': B -> P) (r': C -> P) (pp': l' o f == r' o g) : PO f g -> P := Colimit_rec P (Build_span_cocone l' r' pp').
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.