diagonal_functor _ _ -| limit_functor := right_kan_extension_adjunction has_limits.
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.