Limits in categories of condensed objects

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

instance instHasLimitsCondensedSetInstCategoryCondensedTypeTypes : CategoryTheory.Limits.HasLimits CondensedSet

Equations

• instHasLimitsCondensedSetInstCategoryCondensedTypeTypes = ⋯

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

Equations

• instHasLimitsOfSizeCondensedSetInstCategoryCondensedTypeTypes = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯