Pushout f g <~> PO f g. Proof. srapply colimit_unicity. 3: eapply is_PO_pushout. eapply iscolimit_colimit. 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.