JoyalTrick

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

Statistics

Metric	Count
Definitions	0
Theorems hasLiftingProperty_of_joyalTrick, hasLiftingProperty_of_joyalTrickDual	2
Total	2

HomotopicalAlgebra.ModelCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLiftingProperty_of_joyalTrick 📖	—	CategoryTheory.HasLiftingProperty	—	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.CommSq.w CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.MorphismProperty.MapFactorizationData.fac CategoryTheory.Limits.colimit.ι_desc CategoryTheory.MorphismProperty.comp_mem CategoryTheory.MorphismProperty.of_isPushout CategoryTheory.IsPushout.of_hasPushout HomotopicalAlgebra.mem_cofibrations CategoryTheory.MorphismProperty.MapFactorizationData.hi HomotopicalAlgebra.weakEquivalence_iff CategoryTheory.MorphismProperty.of_postcomp CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toHasOfPostcompProperty CategoryTheory.MorphismProperty.MapFactorizationData.hp CategoryTheory.sq_hasLift_of_hasLiftingProperty HomotopicalAlgebra.cofibration_iff CategoryTheory.Limits.pushout.condition_assoc CategoryTheory.Category.comp_id CategoryTheory.whisker_eq CategoryTheory.CommSq.fac_left CategoryTheory.CommSq.fac_right
hasLiftingProperty_of_joyalTrickDual 📖	—	CategoryTheory.HasLiftingProperty	—	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.CommSq.w CategoryTheory.MorphismProperty.MapFactorizationData.fac_assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.comp_id CategoryTheory.MorphismProperty.comp_mem CategoryTheory.MorphismProperty.MapFactorizationData.hp CategoryTheory.MorphismProperty.of_isPullback CategoryTheory.IsPullback.of_hasPullback HomotopicalAlgebra.mem_fibrations HomotopicalAlgebra.weakEquivalence_iff CategoryTheory.MorphismProperty.of_precomp CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toHasOfPrecompProperty CategoryTheory.MorphismProperty.MapFactorizationData.hi CategoryTheory.sq_hasLift_of_hasLiftingProperty HomotopicalAlgebra.fibration_iff CategoryTheory.CommSq.fac_left_assoc CategoryTheory.Category.assoc CategoryTheory.Limits.pullback.condition CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.CommSq.fac_right

---

← Back to Index