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

Equations

• instHasLimitsCondensedSet = ⋯

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

Equations

• instHasLimitsOfSizeCondensedSet = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯