Theorems · Definition · category theory
CategoryTheory.Limits.HasCoproductsOfShape
Type v → (C : Type u_1) → [CategoryTheory.Category.{u_2, u_1} C] → PropAn abbreviation for HasColimitsOfShape (Discrete f).
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
- CategoryTheory.Discreteproof · cited by 2,447
- CategoryTheory.Limits.HasColimitsOfShapeproof · cited by 308
Cited by38
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.Sigma.functorstatement and proof · cited by 10
- CategoryTheory.Limits.Sigma.mapIsostatement and proof · cited by 8
- CategoryTheory.evaluationLeftAdjointstatement and proof · cited by 6
- CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColimstatement and proof · cited by 4
- CategoryTheory.Limits.Sigma.functorιstatement and proof · cited by 3
- CategoryTheory.Limits.Sigma.constCompSigmaIsoConststatement and proof · cited by 2
- CategoryTheory.Limits.hasCoproductsOfShape_of_oppositestatement · cited by 2
- CategoryTheory.Limits.hasProductsOfShape_of_oppositestatement and proof · cited by 2
- CategoryTheory.Limits.Sigma.ι_mapIso_homstatement and proof · cited by 2
- CategoryTheory.evaluationAdjunctionRightstatement and proof · cited by 2
- CategoryTheory.Limits.hasCoproductsOfShape_of_smallstatement · cited by 1
- CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim_comp_functorιstatement and proof · cited by 1