colimit_functor -| diagonal_functor _ _ := left_kan_extension_adjunction has_colimits.
Require Import Category.Core Functor.Core. Require Import KanExtensions.Functors. Require Import Limits.Core. Require Import FunctorCategory.Core. Require Import Adjoint.Core. Require Import NatCategory.