Theorems · Definition · category theory
HomotopicalAlgebra.LeftHomotopyClass
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] → C → C → [HomotopicalAlgebra.CategoryWithWeakEquivalences C] → Type vIn a category with weak equivalences, this is the quotient of the type
of morphisms X ⟶ Y by the equivalence relation generated by left homotopies.
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
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
- HomotopicalAlgebra.CategoryWithWeakEquivalencesstatement and proof · cited by 77
- HomotopicalAlgebra.LeftHomotopyRelproof · cited by 22
Cited by20
Results whose statement or proof uses this declaration.
- HomotopicalAlgebra.LeftHomotopyClass.mkstatement · cited by 14
- HomotopicalAlgebra.leftHomotopyClassToHomstatement · cited by 6
- HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClassstatement · cited by 4
- HomotopicalAlgebra.LeftHomotopyClass.mk_surjectivestatement · cited by 4
- HomotopicalAlgebra.LeftHomotopyClass.postcompstatement and proof · cited by 4
- HomotopicalAlgebra.LeftHomotopyClass.mk_eq_mk_iffstatement · cited by 3
- HomotopicalAlgebra.LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalencestatement and proof · cited by 3
- HomotopicalAlgebra.bijective_leftHomotopyClassToHomstatement · cited by 2
- HomotopicalAlgebra.bijective_rightHomotopyClassToHomproof · cited by 2
- HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeftstatement · cited by 1
- HomotopicalAlgebra.bijective_leftHomotopyClassToHom_iff_bijective_rightHomotopyClassToHomstatement and proof · cited by 1
- HomotopicalAlgebra.leftHomotopyClassToHom.congr_simpstatement and proof · cited by 0