Limits in categories of light condensed objects

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

instance instHasLimitsOfSizeLightCondSet : CategoryTheory.Limits.HasLimitsOfSize.{u, u, u + 1, u + 1} LightCondSet

Equations

• instHasLimitsOfSizeLightCondSet = ⋯

instance instHasFiniteLimitsLightCondSet : CategoryTheory.Limits.HasFiniteLimits LightCondSet

Equations

• instHasFiniteLimitsLightCondSet = ⋯

instance instHasLimitsOfSizeLightCondMod (R : Type u) [Ring R] : CategoryTheory.Limits.HasLimitsOfSize.{u, u, u + 1, u + 1} (LightCondMod R)

Equations

• ⋯ = ⋯

instance instHasFiniteLimitsLightCondMod (R : Type u) [Ring R] : CategoryTheory.Limits.HasFiniteLimits (LightCondMod R)

Equations

• ⋯ = ⋯