(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)^.
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.