Theorems · Definition · category theory
CategoryTheory.Limits.HasBinaryCoproducts
(C : Type u) → [CategoryTheory.Category.{v, u} C] → PropA category HasBinaryCoproducts if it has all colimit of shape Discrete WalkingPair,
i.e. if it has a coproduct for every pair of objects.
- Cited by
- 98 results in Mathlib
- Foundations
- Depth 11 from the axioms, rests on 61 definitions · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Discreteproof · cited by 2,447
- CategoryTheory.Limits.WalkingPairproof · cited by 1,319
- CategoryTheory.Limits.HasColimitsOfShapeproof · cited by 308
Cited by144
Results whose statement or proof uses this declaration.
- CategoryTheory.coprodMonadstatement and proof · cited by 15
- CategoryTheory.IsMonoidalLeftDistribstatement · cited by 13
- CategoryTheory.leftDistribstatement and proof · cited by 12
- CategoryTheory.monoidalOfHasFiniteCoproductsstatement and proof · cited by 11
- CategoryTheory.IsMonoidalRightDistribstatement · cited by 11
- CategoryTheory.rightDistribstatement and proof · cited by 11
- CategoryTheory.Limits.coprod.braidingstatement and proof · cited by 10
- CategoryTheory.Limits.coprod.functorstatement and proof · cited by 8
- CategoryTheory.underToAlgebrastatement and proof · cited by 6
- CategoryTheory.algebraToUnderstatement and proof · cited by 5
- CategoryTheory.Limits.coprod.associatorstatement and proof · cited by 5
- CategoryTheory.algebraEquivUnderstatement and proof · cited by 4