(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 x, apD (PO_ind P l' r' pp') (popp x) = pp' x. Proof. intro x. lhs nrapply apD_pp. rewrite (Colimit_ind_beta_colimp P _ _ (inl tt) (inr true) tt x). rewrite concat_p1, apD_V. rewrite (Colimit_ind_beta_colimp P _ _ (inl tt) (inr false) tt x). rewrite moveR_transport_p_V, moveR_moveL_transport_p. rewrite inv_pp, inv_V. apply concat_p_Vp. 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.