Structures · Category theory
CategoryTheory.Limits.HasCountableProducts
A category has countable products if it has all products indexed by countable types.
- Shape
- One type argument · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by21
- CategoryTheory.Limits.SequentialProduct.functorMap
- CategoryTheory.Limits.SequentialProduct.functorObj
- CategoryTheory.Limits.SequentialProduct.cone
- CategoryTheory.Limits.SequentialProduct.functorMap_commSq_aux
- CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_pos
- CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_neg
- CategoryTheory.CountableAB4Star.of_hasExactLimitsOfShape_nat_and_finite
- CategoryTheory.Limits.SequentialProduct.functorMap_commSq_succ
- CategoryTheory.Limits.SequentialProduct.cone_π_app
- CategoryTheory.CountableAB4Star.of_hasExactLimitsOfShape_nat
- CategoryTheory.Limits.instHasProductsOfShapeOfHasCountableProductsOfCountable
- CategoryTheory.CountableAB4Star.of_countableAB5Star
- CategoryTheory.Limits.SequentialProduct.functorObjProj_neg
- CategoryTheory.Limits.SequentialProduct.functorMap_epi
- CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_neg_assoc
- CategoryTheory.Limits.HasCountableProducts.out
- CategoryTheory.Limits.hasFiniteProducts_of_hasCountableProducts
- CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_pos_assoc
- CategoryTheory.Limits.SequentialProduct.isLimit
- CategoryTheory.Limits.SequentialProduct.functorObjProj_pos
- CategoryTheory.Limits.SequentialProduct.functorMap_commSq
Ancestors0
No ancestors.