(f : A -> B) (g : A -> C) : Diagram span_graph. Proof. srapply Build_Diagram. - intros [i|i]. + exact A. + exact (if i then B else C). - intros [i|i] [j|j] u; cbn; try contradiction. destruct j. + exact f. + exact g. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Graph. Require Import Diagrams.Diagram.