{A : Type} : diagram_const_functor (idmap : A -> A) = diagram_idmap (diagram_const A). Proof. reflexivity. Defined.
Require Import Basics. Require Import Cone. Require Import Cocone. Require Import Diagram. Require Import Graph.