Theorems · Definition · category theory
CategoryTheory.Limits.BinaryBicone.toCocone
{C : Type uC} →
[inst : CategoryTheory.Category.{uC', uC} C] →
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
{P Q : C} → CategoryTheory.Limits.BinaryBicone P Q → CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair P Q)Extract the cocone from a binary bicone.
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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.HasZeroMorphismsstatement and proof · cited by 3,275
- CategoryTheory.Discretestatement · cited by 2,447
- CategoryTheory.Limits.WalkingPairstatement · cited by 1,319
- CategoryTheory.Limits.Coconestatement · cited by 746
- CategoryTheory.Limits.pairstatement · cited by 536
- CategoryTheory.Limits.BinaryBiconestatement and proof · cited by 111
- CategoryTheory.Limits.BinaryCofan.mkproof · cited by 83
- CategoryTheory.Limits.BinaryBicone.inlproof · cited by 47
- CategoryTheory.Limits.BinaryBicone.inrproof · cited by 47
Cited by34
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.BinaryBiproduct.isColimitstatement · cited by 8
- CategoryTheory.Limits.BinaryBicone.IsBilimit.isColimitstatement · cited by 5
- CategoryTheory.Limits.biprod.inl_mapproof · cited by 3
- CategoryTheory.Limits.biprod.inr_mapproof · cited by 3
- CategoryTheory.Limits.pointwiseBinaryBicone.isBilimitproof · cited by 2
- CategoryTheory.Limits.biprod.map_eq_map'proof · cited by 2
- CategoryTheory.Limits.BinaryBicone.IsBilimit.mk.injstatement and proof · cited by 1
- CategoryTheory.Limits.BinaryBicone.IsBilimit.mk.noConfusionstatement and proof · cited by 1
- CategoryTheory.Limits.isBinaryBilimitOfIsColimitstatement and proof · cited by 1
- CategoryTheory.Limits.isBinaryBilimitOfTotalproof · cited by 1
- CategoryTheory.Limits.biprod.map'proof · cited by 1