Theorems · Definition · category theory
CategoryTheory.Limits.BinaryBicone.toBiconeFunctor
{C : Type uC} →
[inst : CategoryTheory.Category.{uC', uC} C] →
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
{X Y : C} →
CategoryTheory.Functor (CategoryTheory.Limits.BinaryBicone X Y)
(CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y))Convert a BinaryBicone into a Bicone over a pair.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
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
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functorstatement · cited by 16,252
- CategoryTheory.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
- CategoryTheory.Limits.WalkingPairstatement and proof · cited by 1,319
- CategoryTheory.Limits.BinaryBiconestatement and proof · cited by 111
- CategoryTheory.Limits.BinaryBicone.ptproof · cited by 95
- CategoryTheory.Limits.Biconestatement · cited by 75
- CategoryTheory.Limits.WalkingPair.casesOnproof · cited by 59
- CategoryTheory.Limits.BinaryBicone.sndproof · cited by 48
- CategoryTheory.Limits.BinaryBicone.fstproof · cited by 48
- CategoryTheory.Limits.BinaryBicone.inlproof · cited by 47
Cited by5
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.BinaryBicone.toBiconeproof · cited by 1
- CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_map_homstatement and proof · cited by 0
- CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_obj_ptstatement and proof · cited by 0
- CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_obj_ιstatement and proof · cited by 0
- CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_obj_πstatement and proof · cited by 0