`(D : Diagram G) : Cone (Limit D) D. Proof. srapply Build_Cone. + intros i x. apply (lim x i). + intros i j g x. apply limp. Defined.
Require Import Basics. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cone. Require Import Diagrams.ConstantDiagram.