Functor (C -> D) (C' -> D) := functor__of__initial_morphism has_left_kan_extensions.
Require Import Category.Core Functor.Core. Require Import KanExtensions.Core. Require Import Adjoint.UniversalMorphisms.Core. Require Import FunctorCategory.Core. Require Import Adjoint.Core.