Limits in categories of condensed objects

This file adds some instances for limits in condensed sets and condensed modules.

instance instHasLimitsCondensedSet : CategoryTheory.Limits.HasLimits CondensedSet

instance instHasLimitsOfSizeCondensedSet : CategoryTheory.Limits.HasLimitsOfSize.{u, u + 1, u + 1, u + 2} CondensedSet

instance instHasLimitsCondensedMod (R : Type (u + 1)) [Ring R] : CategoryTheory.Limits.HasLimits (CondensedMod R)

instance instHasColimitsCondensedMod (R : Type (u + 1)) [Ring R] : CategoryTheory.Limits.HasColimits (CondensedMod R)

instance instHasLimitsOfSizeCondensedMod (R : Type (u + 1)) [Ring R] : CategoryTheory.Limits.HasLimitsOfSize.{u, u + 1, u + 1, u + 2} (CondensedMod R)

instance instHasColimitsOfShapeCondensedOfHasWeakSheafifyCompHausCoherentTopology {A : Type u_1} {J : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} J] [CategoryTheory.Limits.HasColimitsOfShape J A] [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) A] : CategoryTheory.Limits.HasColimitsOfShape J (Condensed A)

instance instHasLimitsOfShapeCondensed {A : Type u_1} {J : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} J] [CategoryTheory.Limits.HasLimitsOfShape J A] : CategoryTheory.Limits.HasLimitsOfShape J (Condensed A)

instance instHasFiniteLimitsCondensed {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Limits.HasFiniteLimits A] : CategoryTheory.Limits.HasFiniteLimits (Condensed A)

instance instHasFiniteColimitsCondensedOfHasWeakSheafifyCompHausCoherentTopology {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Limits.HasFiniteColimits A] [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) A] : CategoryTheory.Limits.HasFiniteColimits (Condensed A)