(P : PO f g -> Type) (l' : forall b, P (pol b)) (r' : forall c, P (por c)) (pp' : forall a, popp a # l' (f a) = r' (g a)) : forall (i j : span_graph) (e : span_graph i j) (ar : span f g i), transport P (colimp i j e ar) (PO_ind_obj P l' r' j (((span f g) _f e) ar)) = PO_ind_obj P l' r' i ar. Proof. intros [u|b] [u'|b'] []; cbn. destruct b'; cbn. 1: reflexivity. unfold popp in pp'. intro a. apply moveR_transport_p. rhs_V nrapply transport_pp. destruct u. symmetry; apply pp'. 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.