∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.shrinkYonedaMon.{w, v, u} =
    { obj := fun X => MonCat.shrinkFunctor.{w, v, v, u} (CategoryTheory.yonedaMon.obj X),
      map := fun {X Y} f => MonCat.shrinkFunctorMap (CategoryTheory.yonedaMon.map f), map_id := ⋯, map_comp := ⋯ }