Theorems · Definition · category theory
CategoryTheory.Limits.HasBinaryCoproduct
{C : Type u} → [CategoryTheory.Category.{v, u} C] → C → C → PropAn abbreviation for HasColimit (pair X Y).
- Cited by
- 81 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
- 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 and proof · cited by 32,673
- CategoryTheory.Limits.pairproof · cited by 536
- CategoryTheory.Limits.HasColimitproof · cited by 307
Cited by110
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.coprodstatement and proof · cited by 252
- CategoryTheory.Limits.coprod.inlstatement and proof · cited by 137
- CategoryTheory.Limits.coprod.inrstatement and proof · cited by 132
- CategoryTheory.Limits.coprod.descstatement and proof · cited by 69
- CategoryTheory.Limits.coprod.mapstatement and proof · cited by 49
- CategoryTheory.Limits.coprodComparisonstatement and proof · cited by 22
- CategoryTheory.Limits.coprod.desc_compstatement and proof · cited by 22
- CategoryTheory.Limits.coprod.hom_extstatement and proof · cited by 21
- CategoryTheory.Limits.coprod.map_descstatement and proof · cited by 16
- HomotopicalAlgebra.Precylinder.istatement and proof · cited by 13
- CategoryTheory.Limits.codiagstatement and proof · cited by 13
- CategoryTheory.Limits.coprodIsCoprodstatement and proof · cited by 11