fact: Definition limit_functor : Functor (D -> C) (1 -> C) := right_kan_extension_functor has_limits.
imports: Category.Core Functor.Core KanExtensions.Functors Limits.Core FunctorCategory.Core Adjoint.Core NatCategory