{J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J MonCat) →
      [inst_1 : CategoryTheory.IsFiltered J] → (j : J) → F.obj j ⟶ MonCat.FilteredColimits.colimit F