∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] (F : CategoryTheory.Functor J MonCat) {j j' : J} (f : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp (F.map f) (MonCat.Colimits.coconeMorphism F j') =
    MonCat.Colimits.coconeMorphism F j