Theorems · Definition · category theory
CategoryTheory.Limits.BinaryBicone.toCone
{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.Cone (CategoryTheory.Limits.pair P Q)Extract the cone from a binary bicone.
- Cited by
- 18 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.Conestatement · cited by 710
- CategoryTheory.Limits.pairstatement · cited by 536
- CategoryTheory.Limits.BinaryFan.mkproof · cited by 112
- CategoryTheory.Limits.BinaryBiconestatement and proof · cited by 111
- CategoryTheory.Limits.BinaryBicone.sndproof · cited by 48
- CategoryTheory.Limits.BinaryBicone.fstproof · cited by 48
Cited by36
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.biprod.mapproof · cited by 27
- CategoryTheory.Limits.BinaryBiproduct.isLimitstatement · cited by 14
- CategoryTheory.Limits.BinaryBicone.IsBilimit.isLimitstatement · cited by 7
- CategoryTheory.Limits.biprod.map_fstproof · cited by 6
- CategoryTheory.Limits.biprod.map_sndproof · cited by 5
- CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBinaryProductproof · cited by 2
- 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.isBinaryBilimitOfIsLimitstatement and proof · cited by 1
- CategoryTheory.Limits.isBinaryBilimitOfTotalproof · cited by 1