∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections],
  MonCat.HasLimits.limitConeIsLimit F =
    CategoryTheory.Limits.IsLimit.ofFaithful (CategoryTheory.forget MonCat)
      (CategoryTheory.Limits.Types.Small.limitConeIsLimit (F.comp (CategoryTheory.forget MonCat)))
      (fun s =>
        MonCat.ofHom
          {
            toFun := fun v =>
              EquivLike.coe (equivShrink ↑(F.comp (CategoryTheory.forget MonCat)).sections)
                ⟨fun j => ((CategoryTheory.forget MonCat).mapCone s).π.app j v, ⋯⟩,
            map_one' := ⋯, map_mul' := ⋯ })
      ⋯