Functor (D -> C) (1 -> C) := right_kan_extension_functor 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.