Limits in Grp C

We show that Grp C has limits.

instance CategoryTheory.instPreservesLimitsOfShapeMonFunctorOppositeMonCatShrinkYonedaMon {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {J : Type w} [Category.{u_2, w} J] [Limits.HasLimitsOfShape J C] : Limits.PreservesLimitsOfShape J shrinkYonedaMon.{max w v, v, u_1}

noncomputable def CategoryTheory.Grp.limitAux {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {J : Type w} [Category.{u_2, w} J] [Limits.HasLimitsOfShape J C] (F : Functor J (Grp C)) : Grp C

An auxiliary construction in order to prove that Grp.forget₂Mon creates limits.

@[implicit_reducible]

noncomputable instance CategoryTheory.instCreatesLimitsOfShapeGrpMonForget₂Mon {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {J : Type w} [Category.{u_2, w} J] [Limits.HasLimitsOfShape J C] : CreatesLimitsOfShape J (Grp.forget₂Mon C)

@[implicit_reducible]

noncomputable instance CategoryTheory.instCreatesLimitsOfShapeGrpForget {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {J : Type w} [Category.{u_2, w} J] [Limits.HasLimitsOfShape J C] : CreatesLimitsOfShape J (Grp.forget C)

instance CategoryTheory.instHasLimitsOfShapeGrp {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {J : Type w} [Category.{u_2, w} J] [Limits.HasLimitsOfShape J C] : Limits.HasLimitsOfShape J (Grp C)