∀ {J : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} J] (F : CategoryTheory.Functor J MonCat)
  (q : Quotient (MonCat.Colimits.colimitSetoid F)) (b c : MonCat.Colimits.ColimitType F), q * b * c = q * (b * c)