{G : Graph} {D : Diagram G} (E : DDiagram D) : Diagram G. Proof. srapply Build_Diagram. - intro i. exact {x : D i & E (i; x)}. - intros i j g x. simpl in *. exists (D _f g x.1). exact (@arr _ E (i; x.1) (j; D _f g x.1) (g; idpath) x.2). Defined.
Require Import Basics. Require Import Diagrams.Graph. Require Import Diagrams.Diagram.