pol' {f : A -> B} {g : A -> C} {Z} (Co : Cocone (span f g) Z) : B -> Z := legs Co (inr true).
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.