Theorems · Inductive type · category theory
CategoryTheory.Limits.MultispanIndex
CategoryTheory.Limits.MultispanShape →
(C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max (max (max u v) w) w')This is a structure encapsulating the data necessary to define a Multispan.
- Cited by
- 102 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
- CategoryTheory.Limits.MultispanShapestatement · cited by 102
Cited by162
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.MultispanIndex.multispanstatement and proof · cited by 139
- CategoryTheory.Limits.MultispanIndex.rightstatement and proof · cited by 117
- CategoryTheory.Limits.MultispanIndex.leftstatement and proof · cited by 85
- CategoryTheory.GlueData.diagramstatement · cited by 68
- CategoryTheory.Limits.Multicofork.πstatement and proof · cited by 50
- CategoryTheory.Limits.Multicoforkstatement and proof · cited by 43
- CategoryTheory.Limits.MultispanIndex.fststatement and proof · cited by 40
- CategoryTheory.Limits.MultispanIndex.sndstatement and proof · cited by 40
- CategoryTheory.Limits.HasMulticoequalizerstatement and proof · cited by 38
- CategoryTheory.Limits.MultispanIndex.fstSigmaMapOfIsColimitstatement and proof · cited by 29
- CategoryTheory.Limits.MultispanIndex.sndSigmaMapOfIsColimitstatement and proof · cited by 29
- CategoryTheory.Limits.Multicoequalizer.πstatement and proof · cited by 25