∀ {C : Type u_3} {D : Type u_4} {H : Type u_6} [inst : CategoryTheory.Category.{u_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] [inst_2 : CategoryTheory.Category.{u_5, u_6} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [inst_3 : L.HasPointwiseLeftKanExtension F] (Y : D)
  (g₁ g₂ : CategoryTheory.CostructuredArrow L Y) (φ : g₁ ⟶ g₂),
  CategoryTheory.CategoryStruct.comp (((CategoryTheory.CostructuredArrow.proj L Y).comp F).map φ)
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L Y).comp F)
        ((CategoryTheory.CostructuredArrow.map (CategoryTheory.CategoryStruct.id Y)).obj g₂)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L Y).comp F)
        ((CategoryTheory.CostructuredArrow.map (CategoryTheory.CategoryStruct.id Y)).obj g₁))
      (((CategoryTheory.Functor.const (CategoryTheory.CostructuredArrow L Y)).obj
            (CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.proj L Y).comp F))).map
        φ)