Theorems · Definition · category theory
HomotopicalAlgebra.RightHomotopyClass
{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 right homotopies.
- Cited by
- 16 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.RightHomotopyRelproof · cited by 22
Cited by21
Results whose statement or proof uses this declaration.
- HomotopicalAlgebra.RightHomotopyClass.mkstatement · cited by 17
- HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iffstatement · cited by 5
- HomotopicalAlgebra.RightHomotopyClass.precompstatement and proof · cited by 5
- HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClassstatement · cited by 4
- HomotopicalAlgebra.RightHomotopyClass.mk_surjectivestatement · cited by 4
- HomotopicalAlgebra.rightHomotopyClassToHomstatement · cited by 4
- HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalencestatement and proof · cited by 4
- HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRightstatement · cited by 4
- HomotopicalAlgebra.bijective_rightHomotopyClassToHomstatement and proof · cited by 2
- HomotopicalAlgebra.RightHomotopyClass.whiteheadproof · cited by 2
- HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_weakEquivalencestatement and proof · cited by 1