{G : Graph} (D : Diagram G) : Graph. Proof. srapply Build_Graph. + exact {i : G & D i}. + intros i j. exact {g : G i.1 j.1 & D _f g i.2 = j.2}. Defined.
Require Import Basics. Require Import Diagrams.Graph. Require Import Diagrams.Diagram.