English
The morphism coming from compULiftYonedaIsoULiftYonedaCompLan is the left Kan extension of the relevant functor along yoneda.
Русский
Морфизм, полученный из compULiftYonedaIsoULiftYonedaCompLan, является левым Kan-расширением соответствующего функторa вдоль yoneda.
LaTeX
$$$$ \text{IsLeftKanExtension}( (F.op.lan).hom ) $$$$
Lean4
/-- Given a functor `F : C ⥤ D`, `F.op.lan : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁` is the
left Kan extension of `F ⋙ yoneda : C ⥤ Dᵒᵖ ⥤ Type v₁` along `yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁`. -/
instance : F.op.lan.IsLeftKanExtension (compULiftYonedaIsoULiftYonedaCompLan.{w} F).hom :=
⟨⟨Limits.IsInitial.ofUnique _⟩⟩
