(P: Type) (l': B -> P) (r': C -> P) (pp': l' o f == r' o g) : forall x, ap (PO_rec P l' r' pp') (popp x) = pp' x. Proof. intro x. unfold popp. refine (ap_pp _ _ _ @ _ @ concat_p1 _). refine (_ @@ _). 1: exact (Colimit_rec_beta_colimp P (Build_span_cocone l' r' pp') (inl tt) (inr true) tt x). lhs nrapply ap_V. apply (inverse2 (q:=1)). exact (Colimit_rec_beta_colimp P (Build_span_cocone l' r' pp') (inl tt) (inr false) tt 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.