fact: Definition Pushout_Limit {C : Category} (F : Span C) := Colimit F.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor Category.Structure.Cone Category.Structure.Limit Category.Structure.Span Category.Structure.Pullback Category.Construction.Opposite Category.Functor.Opposite Category.Instance.Roof