proposition: Theorem limit_adjoint {G : Graph} {D : Diagram G} {C : Type} : (C -> Limit D) <~> DiagramMap (diagram_const C) D.
proof: 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.
imports: Basics Diagrams.Diagram Diagrams.Graph Diagrams.Cone Diagrams.ConstantDiagram