{A B : Type} (f : A -> B) : DiagramMap (diagram_const A) (diagram_const B). Proof. srapply Build_DiagramMap. 1: intro i; exact f. reflexivity. Defined.
Require Import Basics. Require Import Cone. Require Import Cocone. Require Import Diagram. Require Import Graph.