fact: Definition limit_adjunction : diagonal_functor _ _ -| limit_functor := right_kan_extension_adjunction has_limits.
imports: Category.Core Functor.Core KanExtensions.Functors Limits.Core FunctorCategory.Core Adjoint.Core NatCategory