fact: Definition PO_rec_beta_pp (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.
imports: Basics Types Diagrams.Graph Diagrams.Diagram Diagrams.Span Diagrams.Cocone Colimits.Colimit