Theorems · Theorem · category theory
HomotopicalAlgebra.Precylinder.inl_i
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A)
[inst_1 : CategoryTheory.Limits.HasBinaryCoproduct A A],
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl P.i = P.i₀- Cited by
- 5 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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.Homstatement · cited by 32,603
- CategoryTheory.CategoryStruct.compstatement · cited by 17,999
- CategoryTheory.Limits.coprodstatement · cited by 252
- CategoryTheory.Limits.colimit.ι_descproof · cited by 170
- CategoryTheory.Limits.coprod.inlstatement · cited by 137
- CategoryTheory.Limits.BinaryCofan.mkproof · cited by 83
- CategoryTheory.Limits.HasBinaryCoproductstatement and proof · cited by 81
- HomotopicalAlgebra.Precylinder.Istatement · cited by 75
- HomotopicalAlgebra.Precylinderstatement and proof · cited by 56
- HomotopicalAlgebra.Precylinder.i₀statement and proof · cited by 40
- HomotopicalAlgebra.Precylinder.i₁proof · cited by 40
Cited by5
Results whose statement or proof uses this declaration.
- HomotopicalAlgebra.Precylinder.inl_i_assocproof · cited by 4
- HomotopicalAlgebra.LeftHomotopyRel.exists_very_good_cylinderproof · cited by 2
- HomotopicalAlgebra.Precylinder.symm_iproof · cited by 2
- HomotopicalAlgebra.Cylinder.LeftHomotopy.exists_good_cylinderproof · cited by 1
- HomotopicalAlgebra.Cylinder.ofFactorizationData_iproof · cited by 0