Theorems · Definition · category theory
HomotopicalAlgebra.PathObject.toPrepathObject
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
[inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
{A : C} → HomotopicalAlgebra.PathObject A → HomotopicalAlgebra.PrepathObject A- Cited by
- 24 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- HomotopicalAlgebra.CategoryWithWeakEquivalencesstatement and proof · cited by 77
- HomotopicalAlgebra.PrepathObjectstatement · cited by 56
- HomotopicalAlgebra.PathObjectstatement and proof · cited by 32
Cited by35
Results whose statement or proof uses this declaration.
- HomotopicalAlgebra.PathObject.RightHomotopyproof · cited by 14
- HomotopicalAlgebra.PathObject.symmproof · cited by 6
- HomotopicalAlgebra.PathObject.transproof · cited by 4
- HomotopicalAlgebra.RightHomotopyRel.exists_very_good_pathObjectproof · cited by 3
- HomotopicalAlgebra.PathObject.ofFactorizationData_p₀statement and proof · cited by 1
- HomotopicalAlgebra.PathObject.ofFactorizationData_p₁statement and proof · cited by 1
- HomotopicalAlgebra.PathObject.symm_pstatement and proof · cited by 1
- HomotopicalAlgebra.PathObject.RightHomotopy.exists_good_pathObjectproof · cited by 1
- HomotopicalAlgebra.PathObject.RightHomotopy.reflproof · cited by 1
- HomotopicalAlgebra.PathObject.RightHomotopy.transstatement and proof · cited by 1
- HomotopicalAlgebra.RightHomotopyRel.factorsThroughLocalizationproof · cited by 1