Theorems · Definition · category theory
CategoryTheory.ComposableArrows.left
{C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {n : ℕ} → CategoryTheory.ComposableArrows C n → CThe leftmost object of F : ComposableArrows C n.
- Cited by
- 40 results in Mathlib
- Foundations
- Depth 53 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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.ComposableArrowsstatement and proof · cited by 627
- CategoryTheory.ComposableArrows.obj'proof · cited by 94
Cited by45
Results whose statement or proof uses this declaration.
- CategoryTheory.ComposableArrows.homstatement · cited by 28
- CategoryTheory.ComposableArrows.ext₁statement and proof · cited by 16
- CategoryTheory.ComposableArrows.Precomp.mapstatement and proof · cited by 13
- CategoryTheory.ComposableArrows.precompstatement and proof · cited by 6
- CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrowsstatement · cited by 5
- CategoryTheory.ComposableArrows.precomp_mapstatement and proof · cited by 4
- CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrowsstatement · cited by 3
- SSet.Truncated.HomotopyCategory.homToNerveMk_compproof · cited by 1
- CategoryTheory.ComposableArrows.mk₁_homstatement and proof · cited by 1
- CategoryTheory.ComposableArrows.mk₁_surjectiveproof · cited by 1
- CategoryTheory.nerve.mk₁_homEquiv_applystatement · cited by 1
- CategoryTheory.nerve.nonempty_compStruct_iffproof · cited by 1