(P : PO f g -> Type) (l' : forall b, P (pol b)) (r' : forall c, P (por c)) : forall (i : span_graph) (x : obj (span f g) i), P (colim i x). Proof. intros [u|[]] x; cbn. - exact (@colimp _ (span f g) (inl u) (inr true) tt x # l' (f x)). - exact (l' x). - exact (r' x). 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.