fact: Definition popp (a : A) : pol (f a) = por (g a) := colimp (D:=span f g) (inl tt) (inr true) tt a @ (colimp (D:=span f g) (inl tt) (inr false) tt a)^.
imports: Basics Types Diagrams.Graph Diagrams.Diagram Diagrams.Span Diagrams.Cocone Colimits.Colimit