fact: Definition popp' {f : A -> B} {g : A -> C} {Z} (Co : Cocone (span f g) Z) : pol' Co o f == por' Co o g := fun x => legs_comm Co (inl tt) (inr true) tt x @ (legs_comm Co (inl tt) (inr false) tt x)^.
imports: Basics Types Diagrams.Graph Diagrams.Diagram Diagrams.Span Diagrams.Cocone Colimits.Colimit