∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Functor C D} {B : D}
  (F : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow K B)) (j : J),
  (CategoryTheory.CostructuredArrow.CreatesConnected.natTransInCostructuredArrow F).app j = (F.obj j).hom