PO f g -> Type. Proof. simple refine (PO_rec Type B0 C0 _). cbn; intro x. eapply path_universe_uncurried. etransitivity. - symmetry. apply f0. - apply g0. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Diagram. Require Import Diagrams.DDiagram. Require Import Diagrams.Span. Require Import Diagrams.Cocone. Require Import Colimits.Colimit. Require Import Colimits.Colimit_Pushout. Require Import Colimits.Colimit_Flattening.