Structures · Topology
HomotopicalAlgebra.ModelCategory
A model category is a category equipped with classes of morphisms named cofibrations, fibrations and weak equivalences which satisfy the axioms CM1/CM2/CM3/CM4/CM5 of (closed) model categories.
- Shape
- One type argument · adds categoryWithFibrations, categoryWithCofibrations, categoryWithWeakEquivalences, cm1a, cm1b, cm2, cm3a, cm3b, cm3c, cm4a, cm4b, cm5a, cm5b
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Concrete types that are instances2
- CategoryTheory.Over
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by313
- HomotopicalAlgebra.BifibrantObject.homRel
- HomotopicalAlgebra.BifibrantObject.HoCat
- HomotopicalAlgebra.CofibrantObject.homRel
- HomotopicalAlgebra.BifibrantObject.toHoCat
- HomotopicalAlgebra.CofibrantObject.HoCat
- HomotopicalAlgebra.CofibrantObject.toHoCat
- HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObj
- HomotopicalAlgebra.FibrantObject.homRel
- HomotopicalAlgebra.CofibrantObject.iBifibrantResolutionObj
- HomotopicalAlgebra.FibrantObject.HoCat
- HomotopicalAlgebra.FibrantObject.toHoCat
- HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj
- HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj
- HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap
- HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject
- HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj
- HomotopicalAlgebra.CofibrantBrownFactorization.toMapFactorizationData
- HomotopicalAlgebra.leftHomotopyClassToHom
- HomotopicalAlgebra.Cylinder.ofFactorizationData
- HomotopicalAlgebra.FibrantBrownFactorization.toMapFactorizationData
- HomotopicalAlgebra.PathObject.ofFactorizationData
- HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj
- HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution
- HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iff
- HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight
- HomotopicalAlgebra.rightHomotopyClassToHom
- HomotopicalAlgebra.CofibrantBrownFactorization.mk'
- HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence
- HomotopicalAlgebra.FibrantBrownFactorization.mk'
- HomotopicalAlgebra.FibrantBrownFactorization.r
- HomotopicalAlgebra.PathObject.trans
- HomotopicalAlgebra.CofibrantBrownFactorization.s
- HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass
- HomotopicalAlgebra.Cylinder.trans
- HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap
- HomotopicalAlgebra.LeftHomotopyRel.exists_good_cylinder
- HomotopicalAlgebra.RightHomotopyRel.exists_very_good_pathObject
- HomotopicalAlgebra.FibrantObject.HoCat.resolutionMap
- HomotopicalAlgebra.LeftHomotopyClass.mk_eq_mk_iff
- HomotopicalAlgebra.RightHomotopyRel.exists_good_pathObject
- HomotopicalAlgebra.LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence
- HomotopicalAlgebra.Cylinder.exists_very_good
- HomotopicalAlgebra.FibrantBrownFactorization.i_r
- HomotopicalAlgebra.FibrantObject.HoCat.resolution
- HomotopicalAlgebra.PathObject.exists_very_good
- HomotopicalAlgebra.CofibrantObject.HoCat.resolution
- HomotopicalAlgebra.FibrantObject.HoCat.resolutionMap_fac
- HomotopicalAlgebra.LeftHomotopyRel.rightHomotopyRel
- HomotopicalAlgebra.CofibrantObject.homRel_iff_rightHomotopyRel
- HomotopicalAlgebra.RightHomotopyRel.equivalence