{A B C : Type} (f : A -> B) (g : B -> C) : diagram_const_functor (g o f) = diagram_comp (diagram_const_functor g) (diagram_const_functor f). Proof. reflexivity. Defined.
Require Import Basics. Require Import Cone. Require Import Cocone. Require Import Diagram. Require Import Graph.