CategoryWithCofibrations

📁 Source: Mathlib/AlgebraicTopology/ModelCategory/CategoryWithCofibrations.lean

Statistics

Metric	Count
Definitions CategoryWithCofibrations, cofibrations, fibrations, CategoryWithWeakEquivalences, weakEquivalences, Cofibration, WeakEquivalence, cofibrations, fibrations, instCategoryWithCofibrationsOpposite, instCategoryWithFibrationsOpposite, instCategoryWithWeakEquivalencesFullSubcategory, instCategoryWithWeakEquivalencesOpposite, trivialCofibrations, trivialFibrations, weakEquivalences	16
Theorems mem, mem, mem, cofibration_iff, cofibration_op_iff, cofibration_unop_iff, cofibrations_eq_unop, cofibrations_op, fibration_iff, fibration_op_iff, fibration_unop_iff, fibrations_eq_unop, fibrations_op, instCofibrationOppositeOpOfFibration, instCofibrationUnopOfFibrationOpposite, instFibrationOppositeOpOfCofibration, instFibrationUnopOfCofibrationOpposite, instHasTwoOutOfThreePropertyFullSubcategoryWeakEquivalences, instIsMultiplicativeFullSubcategoryWeakEquivalences, instWeakEquivalenceHomFullSubcategory, instWeakEquivalenceMapFullSubcategoryι, instWeakEquivalenceOppositeOp, instWeakEquivalenceUnopOfOpposite, mem_cofibrations, mem_fibrations, mem_trivialCofibrations, mem_trivialCofibrations_iff, mem_trivialFibrations, mem_trivialFibrations_iff, mem_weakEquivalences, trivialCofibrations_eq_unop, trivialCofibrations_op, trivialCofibrations_sub_cofibrations, trivialCofibrations_sub_weakEquivalences, trivialFibrations_eq_unop, trivialFibrations_op, trivialFibrations_sub_fibrations, trivialFibrations_sub_weakEquivalences, weakEquivalence_iff, weakEquivalence_iff_of_objectProperty, weakEquivalences_eq_unop, weakEquivalences_op, weakEquivalences_op_iff, weakEquivalences_unop_iff	44
Total	60

HomotopicalAlgebra

Definitions

Name	Category	Theorems
CategoryWithCofibrations 📖	CompData	—
CategoryWithWeakEquivalences 📖	CompData	—
Cofibration 📖	CompData	32 math math: fibration_op_iff, instCofibrationOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsIso, Cylinder.instCofibrationI₁, mem_trivialCofibrations_iff, cofibration_op_iff, instCofibrationInrOfIsCofibrant, instCofibrationMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations_1, cofibrations_over_iff, instCofibrationInrOfIsStableUnderCobaseChangeCofibrations, instCofibrationLeftDiscretePUnitOfOver, PathObject.IsVeryGood.cofibration_ι, SSet.modelCategoryQuillen.cofibration_of_mono, FibrantObject.HoCat.exists_resolution, instCofibrationITrivialCofibrationsFibrations, SSet.modelCategoryQuillen.cofibration_iff, FibrantObject.instCofibrationIResolutionObj, instCofibrationInlOfIsStableUnderCobaseChangeCofibrations, Cylinder.IsGood.cofibration_i, CofibrantBrownFactorization.cofibration_s, instCofibrationCompOfIsStableUnderCompositionCofibrations, isCofibrant_iff, instCofibrationOppositeOpOfFibration, Cylinder.instCofibrationI₀, fibration_unop_iff, instCofibrationUnopOfFibrationOpposite, instCofibrationICofibrationsTrivialFibrations, cofibration_unop_iff, instCofibrationInlOfIsCofibrant, CofibrantObject.exists_bifibrant, isCofibrant_iff_of_isInitial, cofibration_iff, CofibrantObject.instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj
WeakEquivalence 📖	CompData	60 math math: BifibrantObject.weakEquivalence_homMk_iff, PathObject.weakEquivalence_ι, instWeakEquivalenceOppositeOp, weakEquivalence_iff_of_objectProperty, mem_trivialCofibrations_iff, instWeakEquivalenceCompOfIsStableUnderCompositionWeakEquivalences, CofibrantObject.instWeakEquivalenceBifibrantObjectBifibrantResolutionMap, instWeakEquivalenceIdOfContainsIdentitiesWeakEquivalences, instWeakEquivalenceOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsWeakEquivalencesOfIsIso, FibrantObject.weakEquivalence_toHoCat_map_iff, FibrantBrownFactorization.instWeakEquivalenceR, CofibrantBrownFactorization.instWeakEquivalenceICofibrationsTrivialFibrations, instWeakEquivalenceUnopOfOpposite, FibrantBrownFactorization.instWeakEquivalencePTrivialCofibrationsFibrations, instWeakEquivalenceITrivialCofibrationsFibrations, weakEquivalences_op_iff, CofibrantObject.HoCat.weakEquivalence_resolutionMap_iff, FibrantObject.instWeakEquivalenceIResolutionObj, weakEquivalence_iff, FibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans, weakEquivalence_of_postcomp, instWeakEquivalenceInrOfIsStableUnderCobaseChangeTrivialCofibrationsOfCofibration, FibrantObject.HoCat.exists_resolution, instWeakEquivalenceMapFullSubcategoryι, weakEquivalences_unop_iff, FibrantObject.HoCat.weakEquivalence_resolutionMap_iff, FibrantObject.weakEquivalence_homMk_iff, weakEquivalence_of_postcomp_of_fac, instWeakEquivalenceFstOfIsStableUnderBaseChangeTrivialFibrationsOfFibration, weakEquivalence_of_precomp, CofibrantObject.instWeakEquivalenceIBifibrantResolutionObj, Cylinder.LeftHomotopy.weakEquivalence_iff, CofibrantObject.instWeakEquivalenceWWeakEquivalences, FibrantObject.instWeakEquivalenceWWeakEquivalences, instWeakEquivalenceInlOfIsStableUnderCobaseChangeTrivialCofibrationsOfCofibration, CofibrantObject.instWeakEquivalencePResolutionObj, instWeakEquivalencePCofibrationsTrivialFibrations, CofibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans, CofibrantObject.instWeakEquivalenceHoCatAppAdjUnit, instWeakEquivalenceSndOfIsStableUnderBaseChangeTrivialFibrationsOfFibration, mem_trivialFibrations_iff, Cylinder.instWeakEquivalenceI₀, PathObject.instWeakEquivalenceP₁, CofibrantObject.exists_bifibrant, CofibrantObject.HoCat.exists_resolution, CofibrantObject.instWeakEquivalenceHoCatAppUnitHoCatAdj, weakEquivalences_over_iff, CofibrantObject.weakEquivalence_toHoCat_map_iff, instWeakEquivalenceLeftDiscretePUnitOfOver, CofibrantObject.instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, CofibrantBrownFactorization.instWeakEquivalenceS, PathObject.instWeakEquivalenceP₀, Cylinder.instWeakEquivalenceI₁, CofibrantObject.weakEquivalence_homMk_iff, PathObject.RightHomotopy.weakEquivalence_iff, weakEquivalence_precomp_iff, instWeakEquivalenceHomFullSubcategory, weakEquivalence_postcomp_iff, Cylinder.weakEquivalence_π, weakEquivalence_of_precomp_of_fac
cofibrations 📖	CompOp	39 math math: Cylinder.ofFactorizationData_i₀, SSet.modelCategoryQuillen.cofibrations_eq, Cylinder.ofFactorizationData_i₁, trivialCofibrations_sub_cofibrations, CofibrantBrownFactorization.instWeakEquivalenceICofibrationsTrivialFibrations, instFibrationPCofibrationsTrivialFibrations, instHasFactorizationOppositeCofibrationsTrivialFibrationsOfTrivialCofibrationsFibrations, Cylinder.ofFactorizationData_I, cofibrations_op, mem_cofibrations, ModelCategory.cm3c, instIsStableUnderRetractsOverCofibrations, fibrations_eq_unop, Cylinder.ofFactorizationData_i, CofibrantBrownFactorization.s_p, trivialFibrations_llp, cofibrations_eq_unop, instIsStableUnderCobaseChangeCofibrations, CofibrantBrownFactorization.cofibration_s, Cylinder.ofFactorizationData_π, cofibrations_over_def, CofibrantBrownFactorization.mk'_s, ModelCategory.cm5b, CofibrantBrownFactorization.mk'_p, CofibrantBrownFactorization.s_p_assoc, fibrations_op, cofibrations_rlp, instWeakEquivalencePCofibrationsTrivialFibrations, CofibrantBrownFactorization.mk'_Z, instCofibrationICofibrationsTrivialFibrations, instIsMultiplicativeCofibrations, Cofibration.mem, instIsStableUnderRetractsOppositeCofibrationsOfFibrations, instHasFactorizationOverCofibrationsTrivialFibrations, CofibrantBrownFactorization.instWeakEquivalenceS, isStableUnderCoproductsOfShape_cofibrations, cofibration_iff, ModelCategory.instIsWeakFactorizationSystemCofibrationsTrivialFibrations, CofibrantBrownFactorization.mk'_i
fibrations 📖	CompOp	39 math math: FibrantBrownFactorization.i_r_assoc, mem_fibrations, fibration_iff, SSet.modelCategoryQuillen.fibrations_eq, instIsStableUnderRetractsOverFibrations, FibrantBrownFactorization.instWeakEquivalenceR, FibrantBrownFactorization.mk'_i, FibrantBrownFactorization.instWeakEquivalencePTrivialCofibrationsFibrations, instWeakEquivalenceITrivialCofibrationsFibrations, FibrantBrownFactorization.mk'_Z, trivialFibrations_sub_fibrations, cofibrations_op, instIsMultiplicativeFibrations, ModelCategory.cm3b, instHasFactorizationOppositeTrivialCofibrationsFibrationsOfCofibrationsTrivialFibrations, PathObject.ofFactorizationData_p, isStableUnderProductsOfShape_fibrations, fibrations_eq_unop, ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations, PathObject.ofFactorizationData_p₁, Fibration.mem, instCofibrationITrivialCofibrationsFibrations, FibrantBrownFactorization.fibration_r, fibrations_llp, PathObject.ofFactorizationData_P, cofibrations_eq_unop, fibrations_over_def, instFibrationPTrivialCofibrationsFibrations, instIsStableUnderBaseChangeFibrations, trivialCofibrations_rlp, ModelCategory.cm5a, instHasFactorizationOverTrivialCofibrationsFibrations, fibrations_op, FibrantBrownFactorization.mk'_r, instIsStableUnderRetractsOppositeFibrationsOfCofibrations, PathObject.ofFactorizationData_p₀, FibrantBrownFactorization.mk'_p, PathObject.ofFactorizationData_ι, FibrantBrownFactorization.i_r
instCategoryWithCofibrationsOpposite 📖	CompOp	10 math math: cofibration_op_iff, instHasFactorizationOppositeCofibrationsTrivialFibrationsOfTrivialCofibrationsFibrations, cofibrations_op, instHasFactorizationOppositeTrivialCofibrationsFibrationsOfCofibrationsTrivialFibrations, fibrations_eq_unop, trivialCofibrations_op, trivialFibrations_eq_unop, instCofibrationOppositeOpOfFibration, fibration_unop_iff, instIsStableUnderRetractsOppositeCofibrationsOfFibrations
instCategoryWithFibrationsOpposite 📖	CompOp	10 math math: fibration_op_iff, instFibrationOppositeOpOfCofibration, instHasFactorizationOppositeCofibrationsTrivialFibrationsOfTrivialCofibrationsFibrations, instHasFactorizationOppositeTrivialCofibrationsFibrationsOfCofibrationsTrivialFibrations, cofibrations_eq_unop, fibrations_op, trivialCofibrations_eq_unop, instIsStableUnderRetractsOppositeFibrationsOfCofibrations, cofibration_unop_iff, trivialFibrations_op
instCategoryWithWeakEquivalencesFullSubcategory 📖	CompOp	36 math math: BifibrantObject.weakEquivalence_homMk_iff, BifibrantObject.inverts_iff_factors, weakEquivalence_iff_of_objectProperty, CofibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, CofibrantObject.instWeakEquivalenceBifibrantObjectBifibrantResolutionMap, FibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, FibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, FibrantObject.weakEquivalence_toHoCat_map_iff, FibrantObject.instHasRightResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, CofibrantObject.instHasLeftResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, instIsMultiplicativeFullSubcategoryWeakEquivalences, FibrantObject.localizerMorphism_functor, BifibrantObject.instIsLocalizationHoCatToHoCatWeakEquivalences, FibrantObject.instIsLocalizationCompιWeakEquivalences, CofibrantObject.instIsCofibrantObjFunctorWeakEquivalencesLocalizerMorphism, CofibrantObject.instIsConnectedLeftResolutionWeakEquivalencesLocalizerMorphism, instHasTwoOutOfThreePropertyFullSubcategoryWeakEquivalences, FibrantObject.instIsConnectedRightResolutionWeakEquivalencesLocalizerMorphism, CofibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, CofibrantObject.instIsLeftDerivabilityStructureWeakEquivalencesLocalizerMorphism, FibrantObject.weakEquivalence_homMk_iff, CofibrantObject.instWeakEquivalenceIBifibrantResolutionObj, FibrantObject.instHasQuotientWeakEquivalencesHomRel, CofibrantObject.instWeakEquivalenceWWeakEquivalences, FibrantObject.instWeakEquivalenceWWeakEquivalences, CofibrantObject.localizerMorphism_functor, CofibrantObject.factorsThroughLocalization, CofibrantObject.instHasQuotientWeakEquivalencesHomRel, FibrantObject.instIsFibrantObjFunctorWeakEquivalencesLocalizerMorphism, CofibrantObject.instIsLocalizationCompιWeakEquivalences, FibrantObject.factorsThroughLocalization, CofibrantObject.weakEquivalence_toHoCat_map_iff, FibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, FibrantObject.instIsRightDerivabilityStructureWeakEquivalencesLocalizerMorphism, CofibrantObject.weakEquivalence_homMk_iff, CofibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism
instCategoryWithWeakEquivalencesOpposite 📖	CompOp	13 math math: instWeakEquivalenceOppositeOp, weakEquivalences_op, instHasFactorizationOppositeCofibrationsTrivialFibrationsOfTrivialCofibrationsFibrations, weakEquivalences_op_iff, instHasFactorizationOppositeTrivialCofibrationsFibrationsOfCofibrationsTrivialFibrations, weakEquivalences_unop_iff, trivialCofibrations_op, instIsStableUnderRetractsOppositeWeakEquivalences, trivialFibrations_eq_unop, trivialCofibrations_eq_unop, weakEquivalences_eq_unop, instHasTwoOutOfThreePropertyOppositeWeakEquivalences, trivialFibrations_op
trivialCofibrations 📖	CompOp	36 math math: mem_trivialCofibrations_iff, FibrantBrownFactorization.i_r_assoc, isStableUnderCoproductsOfShape_trivialCofibrations, FibrantBrownFactorization.instWeakEquivalenceR, instIsMultiplicativeTrivialCofibrations, FibrantBrownFactorization.mk'_i, trivialCofibrations_sub_cofibrations, FibrantBrownFactorization.instWeakEquivalencePTrivialCofibrationsFibrations, instIsStableUnderCobaseChangeTrivialCofibrations, instWeakEquivalenceITrivialCofibrationsFibrations, FibrantBrownFactorization.mk'_Z, trivialCofibrations_sub_weakEquivalences, instHasFactorizationOppositeTrivialCofibrationsFibrationsOfCofibrationsTrivialFibrations, PathObject.ofFactorizationData_p, ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations, PathObject.ofFactorizationData_p₁, trivialCofibrations_over_eq, instCofibrationITrivialCofibrationsFibrations, FibrantBrownFactorization.fibration_r, mem_trivialCofibrations, fibrations_llp, trivialCofibrations_op, PathObject.ofFactorizationData_P, trivialFibrations_eq_unop, instFibrationPTrivialCofibrationsFibrations, trivialCofibrations_rlp, ModelCategory.cm5a, instIsStableUnderRetractsTrivialCofibrationsOfCofibrationsOfWeakEquivalences, instHasFactorizationOverTrivialCofibrationsFibrations, FibrantBrownFactorization.mk'_r, trivialCofibrations_eq_unop, PathObject.ofFactorizationData_p₀, FibrantBrownFactorization.mk'_p, PathObject.ofFactorizationData_ι, trivialFibrations_op, FibrantBrownFactorization.i_r
trivialFibrations 📖	CompOp	36 math math: isStableUnderProductsOfShape_trivialFibrations, Cylinder.ofFactorizationData_i₀, Cylinder.ofFactorizationData_i₁, CofibrantBrownFactorization.instWeakEquivalenceICofibrationsTrivialFibrations, instFibrationPCofibrationsTrivialFibrations, instHasFactorizationOppositeCofibrationsTrivialFibrationsOfTrivialCofibrationsFibrations, trivialFibrations_sub_fibrations, Cylinder.ofFactorizationData_I, trivialFibrations_over_eq, Cylinder.ofFactorizationData_i, trivialFibrations_sub_weakEquivalences, CofibrantBrownFactorization.s_p, instIsMultiplicativeTrivialFibrations, trivialFibrations_llp, instIsStableUnderBaseChangeTrivialFibrations, trivialCofibrations_op, CofibrantBrownFactorization.cofibration_s, trivialFibrations_eq_unop, Cylinder.ofFactorizationData_π, CofibrantBrownFactorization.mk'_s, ModelCategory.cm5b, CofibrantBrownFactorization.mk'_p, CofibrantBrownFactorization.s_p_assoc, cofibrations_rlp, instWeakEquivalencePCofibrationsTrivialFibrations, trivialCofibrations_eq_unop, CofibrantBrownFactorization.mk'_Z, mem_trivialFibrations_iff, instCofibrationICofibrationsTrivialFibrations, mem_trivialFibrations, instHasFactorizationOverCofibrationsTrivialFibrations, instIsStableUnderRetractsTrivialFibrationsOfFibrationsOfWeakEquivalences, CofibrantBrownFactorization.instWeakEquivalenceS, trivialFibrations_op, ModelCategory.instIsWeakFactorizationSystemCofibrationsTrivialFibrations, CofibrantBrownFactorization.mk'_i
weakEquivalences 📖	CompOp	49 math math: BifibrantObject.inverts_iff_factors, CofibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, FibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, FibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, weakEquivalences_op, FibrantObject.instHasRightResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, CofibrantObject.instHasLeftResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, trivialCofibrations_sub_weakEquivalences, weakEquivalence_iff, instIsMultiplicativeFullSubcategoryWeakEquivalences, FibrantObject.localizerMorphism_functor, BifibrantObject.instIsLocalizationHoCatToHoCatWeakEquivalences, FibrantObject.instIsLocalizationCompιWeakEquivalences, CofibrantObject.instIsCofibrantObjFunctorWeakEquivalencesLocalizerMorphism, instRespectsIsoWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition, LeftHomotopyRel.factorsThroughLocalization, CofibrantObject.instIsConnectedLeftResolutionWeakEquivalencesLocalizerMorphism, trivialFibrations_sub_weakEquivalences, instHasTwoOutOfThreePropertyFullSubcategoryWeakEquivalences, mem_weakEquivalences, FibrantObject.instIsConnectedRightResolutionWeakEquivalencesLocalizerMorphism, CofibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, CofibrantObject.instIsLeftDerivabilityStructureWeakEquivalencesLocalizerMorphism, instIsStableUnderRetractsOppositeWeakEquivalences, RightHomotopyRel.factorsThroughLocalization, ModelCategory.cm3a, FibrantObject.instHasQuotientWeakEquivalencesHomRel, CofibrantObject.instWeakEquivalenceWWeakEquivalences, FibrantObject.instWeakEquivalenceWWeakEquivalences, CofibrantObject.localizerMorphism_functor, ModelCategory.cm2, CofibrantObject.factorsThroughLocalization, instHasTwoOutOfThreePropertyOverWeakEquivalences, CofibrantObject.instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences, CofibrantObject.instHasQuotientWeakEquivalencesHomRel, weakEquivalences_eq_unop, FibrantObject.instIsFibrantObjFunctorWeakEquivalencesLocalizerMorphism, CofibrantObject.instIsLocalizationCompιWeakEquivalences, instIsMultiplicativeWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition, WeakEquivalence.mem, FibrantObject.factorsThroughLocalization, CofibrantObject.HoCat.localizerMorphismResolution_functor, instHasTwoOutOfThreePropertyOppositeWeakEquivalences, FibrantObject.HoCat.localizerMorphismResolution_functor, FibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, FibrantObject.instIsRightDerivabilityStructureWeakEquivalencesLocalizerMorphism, instIsStableUnderRetractsOverWeakEquivalences, CofibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, weakEquivalences_over_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cofibration_iff 📖	mathematical	—	Cofibration cofibrations	—	—
cofibration_op_iff 📖	mathematical	—	Cofibration Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategoryWithCofibrationsOpposite Fibration	—	—
cofibration_unop_iff 📖	mathematical	—	Cofibration Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Fibration Opposite CategoryTheory.Category.opposite instCategoryWithFibrationsOpposite	—	—
cofibrations_eq_unop 📖	mathematical	—	cofibrations CategoryTheory.MorphismProperty.unop CategoryTheory.Category.toCategoryStruct fibrations Opposite CategoryTheory.Category.opposite instCategoryWithFibrationsOpposite	—	—
cofibrations_op 📖	mathematical	—	cofibrations Opposite CategoryTheory.Category.opposite instCategoryWithCofibrationsOpposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct fibrations	—	—
fibration_iff 📖	mathematical	—	Fibration fibrations	—	—
fibration_op_iff 📖	mathematical	—	Fibration Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategoryWithFibrationsOpposite Cofibration	—	—
fibration_unop_iff 📖	mathematical	—	Fibration Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Cofibration Opposite CategoryTheory.Category.opposite instCategoryWithCofibrationsOpposite	—	—
fibrations_eq_unop 📖	mathematical	—	fibrations CategoryTheory.MorphismProperty.unop CategoryTheory.Category.toCategoryStruct cofibrations Opposite CategoryTheory.Category.opposite instCategoryWithCofibrationsOpposite	—	—
fibrations_op 📖	mathematical	—	fibrations Opposite CategoryTheory.Category.opposite instCategoryWithFibrationsOpposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct cofibrations	—	—
instCofibrationOppositeOpOfFibration 📖	mathematical	—	Cofibration Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategoryWithCofibrationsOpposite	—	cofibration_op_iff
instCofibrationUnopOfFibrationOpposite 📖	mathematical	—	Cofibration Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	cofibration_unop_iff
instFibrationOppositeOpOfCofibration 📖	mathematical	—	Fibration Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategoryWithFibrationsOpposite	—	fibration_op_iff
instFibrationUnopOfCofibrationOpposite 📖	mathematical	—	Fibration Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	fibration_unop_iff
instHasTwoOutOfThreePropertyFullSubcategoryWeakEquivalences 📖	mathematical	—	CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category weakEquivalences instCategoryWithWeakEquivalencesFullSubcategory	—	CategoryTheory.MorphismProperty.instHasTwoOutOfThreePropertyInverseImage
instIsMultiplicativeFullSubcategoryWeakEquivalences 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category weakEquivalences instCategoryWithWeakEquivalencesFullSubcategory	—	CategoryTheory.MorphismProperty.IsMultiplicative.instInverseImage
instWeakEquivalenceHomFullSubcategory 📖	mathematical	—	WeakEquivalence CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	weakEquivalence_iff_of_objectProperty
instWeakEquivalenceMapFullSubcategoryι 📖	mathematical	—	WeakEquivalence CategoryTheory.Functor.obj CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.ι CategoryTheory.Functor.map	—	instWeakEquivalenceHomFullSubcategory
instWeakEquivalenceOppositeOp 📖	mathematical	—	WeakEquivalence Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategoryWithWeakEquivalencesOpposite	—	weakEquivalences_op_iff
instWeakEquivalenceUnopOfOpposite 📖	mathematical	—	WeakEquivalence Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	weakEquivalences_unop_iff
mem_cofibrations 📖	mathematical	—	cofibrations	—	Cofibration.mem
mem_fibrations 📖	mathematical	—	fibrations	—	Fibration.mem
mem_trivialCofibrations 📖	mathematical	—	trivialCofibrations	—	mem_cofibrations mem_weakEquivalences
mem_trivialCofibrations_iff 📖	mathematical	—	trivialCofibrations Cofibration WeakEquivalence	—	cofibration_iff weakEquivalence_iff
mem_trivialFibrations 📖	mathematical	—	trivialFibrations	—	mem_fibrations mem_weakEquivalences
mem_trivialFibrations_iff 📖	mathematical	—	trivialFibrations Fibration WeakEquivalence	—	fibration_iff weakEquivalence_iff
mem_weakEquivalences 📖	mathematical	—	weakEquivalences	—	WeakEquivalence.mem
trivialCofibrations_eq_unop 📖	mathematical	—	trivialCofibrations CategoryTheory.MorphismProperty.unop CategoryTheory.Category.toCategoryStruct trivialFibrations Opposite CategoryTheory.Category.opposite instCategoryWithFibrationsOpposite instCategoryWithWeakEquivalencesOpposite	—	—
trivialCofibrations_op 📖	mathematical	—	trivialCofibrations Opposite CategoryTheory.Category.opposite instCategoryWithCofibrationsOpposite instCategoryWithWeakEquivalencesOpposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct trivialFibrations	—	—
trivialCofibrations_sub_cofibrations 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra trivialCofibrations cofibrations	—	—
trivialCofibrations_sub_weakEquivalences 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra trivialCofibrations weakEquivalences	—	—
trivialFibrations_eq_unop 📖	mathematical	—	trivialFibrations CategoryTheory.MorphismProperty.unop CategoryTheory.Category.toCategoryStruct trivialCofibrations Opposite CategoryTheory.Category.opposite instCategoryWithCofibrationsOpposite instCategoryWithWeakEquivalencesOpposite	—	—
trivialFibrations_op 📖	mathematical	—	trivialFibrations Opposite CategoryTheory.Category.opposite instCategoryWithFibrationsOpposite instCategoryWithWeakEquivalencesOpposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct trivialCofibrations	—	—
trivialFibrations_sub_fibrations 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra trivialFibrations fibrations	—	—
trivialFibrations_sub_weakEquivalences 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra trivialFibrations weakEquivalences	—	—
weakEquivalence_iff 📖	mathematical	—	WeakEquivalence weakEquivalences	—	—
weakEquivalence_iff_of_objectProperty 📖	mathematical	—	WeakEquivalence CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category instCategoryWithWeakEquivalencesFullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.InducedCategory.Hom.hom	—	—
weakEquivalences_eq_unop 📖	mathematical	—	weakEquivalences CategoryTheory.MorphismProperty.unop CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite instCategoryWithWeakEquivalencesOpposite	—	—
weakEquivalences_op 📖	mathematical	—	weakEquivalences Opposite CategoryTheory.Category.opposite instCategoryWithWeakEquivalencesOpposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct	—	—
weakEquivalences_op_iff 📖	mathematical	—	WeakEquivalence Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategoryWithWeakEquivalencesOpposite	—	—
weakEquivalences_unop_iff 📖	mathematical	—	WeakEquivalence Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite instCategoryWithWeakEquivalencesOpposite	—	weakEquivalences_op_iff

HomotopicalAlgebra.CategoryWithCofibrations

Definitions

Name	Category	Theorems
cofibrations 📖	CompOp	—

HomotopicalAlgebra.CategoryWithFibrations

Definitions

Name	Category	Theorems
fibrations 📖	CompOp	—

HomotopicalAlgebra.CategoryWithWeakEquivalences

Definitions

Name	Category	Theorems
weakEquivalences 📖	CompOp	—

HomotopicalAlgebra.Cofibration

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem 📖	mathematical	—	HomotopicalAlgebra.cofibrations	—	—

HomotopicalAlgebra.Fibration

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem 📖	mathematical	—	HomotopicalAlgebra.fibrations	—	—

HomotopicalAlgebra.WeakEquivalence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem 📖	mathematical	—	HomotopicalAlgebra.weakEquivalences	—	—

---

← Back to Index