{G : Graph} {D : Diagram G} {C : Type} : (C -> Limit D) <~> DiagramMap (diagram_const C) D. Proof. srapply equiv_adjointify. { intro f. srapply Build_DiagramMap. { intros i c. apply lim, f, c. } intros i j g x. apply limp. } { intros [f p] c. srapply Build_Limit. { intro i. apply f, c. } intros i j g. apply p. } 1,2: intro; reflexivity. Defined.
Require Import Basics. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cone. Require Import Diagrams.ConstantDiagram.