Theorems · Definition · category theory
CategoryTheory.ComposableArrows
(C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → ℕ → Type (max v_1 u_1)ComposableArrows C n is the type of functors Fin (n + 1) ⥤ C.
- Cited by
- 627 results in Mathlib
- Foundations
- Depth 25 from the axioms, rests on 239 definitions · uses propext
- 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 and proof · cited by 32,673
- CategoryTheory.Functorproof · cited by 16,252
Cited by800
Results whose statement or proof uses this declaration.
- CategoryTheory.ComposableArrows.mk₁statement · cited by 350
- CategoryTheory.Abelian.SpectralObject.Hstatement · cited by 284
- CategoryTheory.ComposableArrows.map'statement and proof · cited by 133
- CategoryTheory.ComposableArrows.obj'statement and proof · cited by 94
- CategoryTheory.ComposableArrows.mk₂statement · cited by 79
- CategoryTheory.Abelian.SpectralObject.δstatement · cited by 77
- CategoryTheory.nerveproof · cited by 68
- CategoryTheory.ComposableArrows.Exactstatement · cited by 65
- CategoryTheory.ComposableArrows.mk₃statement · cited by 50
- CategoryTheory.ComposableArrows.twoδ₁Toδ₀statement · cited by 49
- CategoryTheory.ComposableArrows.twoδ₂Toδ₁statement · cited by 47
- CategoryTheory.Abelian.SpectralObject.pOpcyclesstatement · cited by 43
Showing the 200 most cited of 800.