Theorems · Definition · category theory
CategoryTheory.Limits.HasCoequalizers
(C : Type u) → [CategoryTheory.Category.{v, u} C] → PropA category HasCoequalizers if it has all colimits of shape WalkingParallelPair, i.e. if it
has a coequalizer for every parallel pair of morphisms.
- Cited by
- 60 results in Mathlib
- Foundations
- Depth 14 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 and proof · cited by 32,673
- CategoryTheory.Limits.WalkingParallelPairproof · cited by 781
- CategoryTheory.Limits.HasColimitsOfShapeproof · cited by 308
Cited by82
Results whose statement or proof uses this declaration.
- Bimod.TensorBimod.Xstatement and proof · cited by 32
- Bimod.tensorBimodstatement and proof · cited by 25
- Bimod.TensorBimod.actLeftstatement and proof · cited by 15
- Bimod.TensorBimod.actRightstatement and proof · cited by 14
- π_tensor_id_preserves_coequalizer_inv_descstatement and proof · cited by 9
- Bimod.AssociatorBimod.homstatement and proof · cited by 9
- Bimod.whiskerLeftstatement and proof · cited by 9
- Bimod.whiskerRightstatement and proof · cited by 9
- Bimod.AssociatorBimod.invstatement and proof · cited by 7
- Bimod.LeftUnitorBimod.homstatement and proof · cited by 6
- Bimod.RightUnitorBimod.homstatement and proof · cited by 6
- Bimod.associatorBimodstatement and proof · cited by 5