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 = (_ : CategoryTheory.Limits.HasLimits (CategoryTheory.Sheaf (CategoryTheory.coherentTopology CompHaus) (Type (u + 1))))

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

Equations

• instHasLimitsOfSizeCondensedSetInstCategoryCondensedTypeTypes = (_ : CategoryTheory.Limits.HasLimitsOfSize.{u, u + 1, u + 1, u + 2} CondensedSet)

instance instHasLimitsCondensedAbInstCategoryCondensedAddCommGroupCatInstAddCommGroupCatLargeCategory : CategoryTheory.Limits.HasLimits CondensedAb

Equations

• One or more equations did not get rendered due to their size.

instance instHasLimitsOfSizeCondensedAbInstCategoryCondensedAddCommGroupCatInstAddCommGroupCatLargeCategory : CategoryTheory.Limits.HasLimitsOfSize.{u, u + 1, u + 1, u + 2} CondensedAb

Equations

• One or more equations did not get rendered due to their size.