∀ {J : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} J] (F : CategoryTheory.Functor J CommMonCat)
  [inst_1 : Small.{u_2, max u_2 u_3} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections]
  (x : CategoryTheory.Limits.Cone F),
  (CategoryTheory.forget₂ CommMonCat MonCat).map
      {
        hom' :=
          {
            toFun := fun v =>
              EquivLike.coe
                (equivShrink
                  ↑((F.comp (CategoryTheory.forget₂ CommMonCat MonCat)).comp (CategoryTheory.forget MonCat)).sections)
                ⟨fun j =>
                  ((CategoryTheory.forget MonCat).mapCone ((CategoryTheory.forget₂ CommMonCat MonCat).mapCone x)).π.app
                    j v,
                  ⋯⟩,
            map_one' := ⋯, map_mul' := ⋯ } } =
    (CategoryTheory.forget₂ CommMonCat MonCat).map
      {
        hom' :=
          {
            toFun := fun v =>
              EquivLike.coe
                (equivShrink
                  ↑((F.comp (CategoryTheory.forget₂ CommMonCat MonCat)).comp (CategoryTheory.forget MonCat)).sections)
                ⟨fun j =>
                  ((CategoryTheory.forget MonCat).mapCone ((CategoryTheory.forget₂ CommMonCat MonCat).mapCone x)).π.app
                    j v,
                  ⋯⟩,
            map_one' := ⋯, map_mul' := ⋯ } }