Loogle!

Result

Found 83 declarations mentioning HomotopicalAlgebra.fibrations.

• HomotopicalAlgebra.fibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] : CategoryTheory.MorphismProperty C
• HomotopicalAlgebra.cofibrations_eq_unop 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] : HomotopicalAlgebra.cofibrations C = (HomotopicalAlgebra.fibrations Cᵒᵖ).unop
• HomotopicalAlgebra.fibrations_eq_unop 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] : HomotopicalAlgebra.fibrations C = (HomotopicalAlgebra.cofibrations Cᵒᵖ).unop
• HomotopicalAlgebra.mem_fibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.Fibration f] : HomotopicalAlgebra.fibrations C f
• HomotopicalAlgebra.Fibration.mem 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y} {inst✝¹ : HomotopicalAlgebra.CategoryWithFibrations C} [self : HomotopicalAlgebra.Fibration f] : HomotopicalAlgebra.fibrations C f
• HomotopicalAlgebra.Fibration.mk 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [HomotopicalAlgebra.CategoryWithFibrations C] (mem : HomotopicalAlgebra.fibrations C f) : HomotopicalAlgebra.Fibration f
• HomotopicalAlgebra.fibration_iff 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HomotopicalAlgebra.CategoryWithFibrations C] : HomotopicalAlgebra.Fibration f ↔ HomotopicalAlgebra.fibrations C f
• HomotopicalAlgebra.cofibrations_op 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] : HomotopicalAlgebra.cofibrations Cᵒᵖ = (HomotopicalAlgebra.fibrations C).op
• HomotopicalAlgebra.fibrations_op 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithCofibrations C] : HomotopicalAlgebra.fibrations Cᵒᵖ = (HomotopicalAlgebra.cofibrations C).op
• HomotopicalAlgebra.trivialFibrations_sub_fibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] : HomotopicalAlgebra.trivialFibrations C ≤ HomotopicalAlgebra.fibrations C
• HomotopicalAlgebra.instIsMultiplicativeFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] : (HomotopicalAlgebra.fibrations C).IsMultiplicative
• HomotopicalAlgebra.instIsStableUnderBaseChangeFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] : (HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange
• HomotopicalAlgebra.instIsStableUnderRetractsTrivialFibrationsOfFibrationsOfWeakEquivalences 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.fibrations C).IsStableUnderRetracts] [(HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts] : (HomotopicalAlgebra.trivialFibrations C).IsStableUnderRetracts
• HomotopicalAlgebra.instIsMultiplicativeTrivialCofibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] : (HomotopicalAlgebra.trivialCofibrations C).IsMultiplicative
• HomotopicalAlgebra.instIsStableUnderCobaseChangeTrivialCofibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] : (HomotopicalAlgebra.trivialCofibrations C).IsStableUnderCobaseChange
• HomotopicalAlgebra.isStableUnderProductsOfShape_fibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] (J : Type w) : (HomotopicalAlgebra.fibrations C).IsStableUnderProductsOfShape J
• HomotopicalAlgebra.isStableUnderCoproductsOfShape_trivialCofibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] (J : Type w) : (HomotopicalAlgebra.trivialCofibrations C).IsStableUnderCoproductsOfShape J
• HomotopicalAlgebra.fibrations_llp 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] : (HomotopicalAlgebra.fibrations C).llp = HomotopicalAlgebra.trivialCofibrations C
• HomotopicalAlgebra.trivialCofibrations_rlp 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] : (HomotopicalAlgebra.trivialCofibrations C).rlp = HomotopicalAlgebra.fibrations C
• HomotopicalAlgebra.instIsMultiplicativeWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] [(HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts] [(HomotopicalAlgebra.weakEquivalences C).IsStableUnderComposition] : (HomotopicalAlgebra.weakEquivalences C).IsMultiplicative
• HomotopicalAlgebra.instRespectsIsoWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] [(HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts] [(HomotopicalAlgebra.weakEquivalences C).IsStableUnderComposition] : (HomotopicalAlgebra.weakEquivalences C).RespectsIso
• HomotopicalAlgebra.instCofibrationOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsIso 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] [CategoryTheory.IsIso f] : HomotopicalAlgebra.Cofibration f
• HomotopicalAlgebra.instWeakEquivalenceOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsWeakEquivalencesOfIsIso 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] [(HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts] [CategoryTheory.IsIso f] : HomotopicalAlgebra.WeakEquivalence f
• HomotopicalAlgebra.instFibrationCompOfIsStableUnderCompositionFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition] [hf : HomotopicalAlgebra.Fibration f] [hg : HomotopicalAlgebra.Fibration g] : HomotopicalAlgebra.Fibration (CategoryTheory.CategoryStruct.comp f g)
• HomotopicalAlgebra.instFibrationFstOfIsStableUnderBaseChangeFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [hg : HomotopicalAlgebra.Fibration g] : HomotopicalAlgebra.Fibration (CategoryTheory.Limits.pullback.fst f g)
• HomotopicalAlgebra.instFibrationSndOfIsStableUnderBaseChangeFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [hf : HomotopicalAlgebra.Fibration f] : HomotopicalAlgebra.Fibration (CategoryTheory.Limits.pullback.snd f g)
• HomotopicalAlgebra.instCofibrationITrivialCofibrationsFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f) : HomotopicalAlgebra.Cofibration h.i
• HomotopicalAlgebra.instFibrationPTrivialCofibrationsFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f) : HomotopicalAlgebra.Fibration h.p
• HomotopicalAlgebra.instWeakEquivalenceITrivialCofibrationsFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f) : HomotopicalAlgebra.WeakEquivalence h.i
• HomotopicalAlgebra.instFibrationMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct Y] [h : ∀ (i : J), HomotopicalAlgebra.Fibration (f i)] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] : HomotopicalAlgebra.Fibration (CategoryTheory.Limits.Pi.map f)
• HomotopicalAlgebra.instFibrationMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations_1 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] [h₁ : HomotopicalAlgebra.Fibration f₁] [h₂ : HomotopicalAlgebra.Fibration f₂] [CategoryTheory.Limits.HasBinaryProduct X₁ X₂] [CategoryTheory.Limits.HasBinaryProduct Y₁ Y₂] : HomotopicalAlgebra.Fibration (CategoryTheory.Limits.prod.map f₁ f₂)
• HomotopicalAlgebra.instWeakEquivalenceMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.Limits.HasCoproduct Y] [h : ∀ (i : J), HomotopicalAlgebra.Cofibration (f i)] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] [∀ (i : J), HomotopicalAlgebra.WeakEquivalence (f i)] : HomotopicalAlgebra.WeakEquivalence (CategoryTheory.Limits.Sigma.map f)
• HomotopicalAlgebra.ModelCategory.cm3b 📋 Mathlib.AlgebraicTopology.ModelCategory.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : HomotopicalAlgebra.ModelCategory C] : (HomotopicalAlgebra.fibrations C).IsStableUnderRetracts
• HomotopicalAlgebra.ModelCategory.cm5a 📋 Mathlib.AlgebraicTopology.ModelCategory.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : HomotopicalAlgebra.ModelCategory C] : (HomotopicalAlgebra.trivialCofibrations C).HasFactorization (HomotopicalAlgebra.fibrations C)
• HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] : (HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)
• HomotopicalAlgebra.ModelCategory.mk' 📋 Mathlib.AlgebraicTopology.ModelCategory.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasFiniteColimits C] [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty] [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] : HomotopicalAlgebra.ModelCategory C
• HomotopicalAlgebra.ModelCategory.mk 📋 Mathlib.AlgebraicTopology.ModelCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (categoryWithFibrations : HomotopicalAlgebra.CategoryWithFibrations C := by infer_instance) (categoryWithCofibrations : HomotopicalAlgebra.CategoryWithCofibrations C := by infer_instance) (categoryWithWeakEquivalences : HomotopicalAlgebra.CategoryWithWeakEquivalences C := by infer_instance) (cm1a : CategoryTheory.Limits.HasFiniteLimits C := by infer_instance) (cm1b : CategoryTheory.Limits.HasFiniteColimits C := by infer_instance) (cm2 : (HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty := by infer_instance) (cm3a : (HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts := by infer_instance) (cm3b : (HomotopicalAlgebra.fibrations C).IsStableUnderRetracts := by infer_instance) (cm3c : (HomotopicalAlgebra.cofibrations C).IsStableUnderRetracts := by infer_instance) (cm4a : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.WeakEquivalence i] [HomotopicalAlgebra.Fibration p], CategoryTheory.HasLiftingProperty i p := by intros; infer_instance) (cm4b : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.Fibration p] [HomotopicalAlgebra.WeakEquivalence p], CategoryTheory.HasLiftingProperty i p := by intros; infer_instance) (cm5a : (HomotopicalAlgebra.trivialCofibrations C).HasFactorization (HomotopicalAlgebra.fibrations C) := by infer_instance) (cm5b : (HomotopicalAlgebra.cofibrations C).HasFactorization (HomotopicalAlgebra.trivialFibrations C) := by infer_instance) : HomotopicalAlgebra.ModelCategory C
• HomotopicalAlgebra.isFibrant_iff_of_isTerminal 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [(HomotopicalAlgebra.fibrations C).RespectsIso] {X Y : C} (p : X ⟶ Y) (hY : CategoryTheory.Limits.IsTerminal Y) : HomotopicalAlgebra.IsFibrant X ↔ HomotopicalAlgebra.Fibration p
• HomotopicalAlgebra.instFibrationFstOfIsFibrant 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X Y : C) [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [CategoryTheory.Limits.HasBinaryProduct X Y] [hY : HomotopicalAlgebra.IsFibrant Y] : HomotopicalAlgebra.Fibration CategoryTheory.Limits.prod.fst
• HomotopicalAlgebra.instFibrationSndOfIsFibrant 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] (X Y : C) [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [CategoryTheory.Limits.HasBinaryProduct X Y] [hX : HomotopicalAlgebra.IsFibrant X] : HomotopicalAlgebra.Fibration CategoryTheory.Limits.prod.snd
• HomotopicalAlgebra.isFibrant_of_fibration 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition] {X Y : C} (p : X ⟶ Y) [HomotopicalAlgebra.Fibration p] [hY : HomotopicalAlgebra.IsFibrant Y] : HomotopicalAlgebra.IsFibrant X
• HomotopicalAlgebra.Cylinder.instIsFibrantIOfIsVeryGood 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A) [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition] [CategoryTheory.Limits.HasBinaryCoproduct A A] [CategoryTheory.Limits.HasTerminal C] [HomotopicalAlgebra.IsFibrant A] [P.IsVeryGood] : HomotopicalAlgebra.IsFibrant P.I
• HomotopicalAlgebra.Cylinder.instIsFibrantIOfFactorizationDataOfIsStableUnderCompositionFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Cylinder
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) (CategoryTheory.Limits.codiag A)) [CategoryTheory.Limits.HasTerminal C] [HomotopicalAlgebra.IsFibrant A] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition] : HomotopicalAlgebra.IsFibrant (HomotopicalAlgebra.Cylinder.ofFactorizationData h).I
• HomotopicalAlgebra.PathObject.instIsFibrantP 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition] [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [HomotopicalAlgebra.IsFibrant A] [P.IsGood] : HomotopicalAlgebra.IsFibrant P.P
• HomotopicalAlgebra.PathObject.instIsGoodSymmOfRespectsIsoFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A) [CategoryTheory.Limits.HasBinaryProducts C] [HomotopicalAlgebra.CategoryWithFibrations C] [P.IsGood] [(HomotopicalAlgebra.fibrations C).RespectsIso] : P.symm.IsGood
• HomotopicalAlgebra.PathObject.instIsVeryGoodSymmOfRespectsIsoFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A) [HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.CategoryWithCofibrations C] [(HomotopicalAlgebra.fibrations C).RespectsIso] [CategoryTheory.Limits.HasBinaryProducts C] [P.IsVeryGood] : P.symm.IsVeryGood
• HomotopicalAlgebra.PathObject.instFibrationP₀ 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition] [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [HomotopicalAlgebra.IsFibrant A] [P.IsGood] : HomotopicalAlgebra.Fibration P.p₀
• HomotopicalAlgebra.PathObject.instFibrationP₁ 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition] [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [HomotopicalAlgebra.IsFibrant A] [P.IsGood] : HomotopicalAlgebra.Fibration P.p₁
• HomotopicalAlgebra.PathObject.ofFactorizationData 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) (CategoryTheory.Limits.diag A)) : HomotopicalAlgebra.PathObject A
• HomotopicalAlgebra.PathObject.instIsCofibrantPOfFactorizationDataOfIsStableUnderCompositionCofibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) (CategoryTheory.Limits.diag A)) [CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.IsCofibrant A] [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition] : HomotopicalAlgebra.IsCofibrant (HomotopicalAlgebra.PathObject.ofFactorizationData h).P
• HomotopicalAlgebra.PathObject.instIsVeryGoodOfFactorizationData 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) (CategoryTheory.Limits.diag A)) : (HomotopicalAlgebra.PathObject.ofFactorizationData h).IsVeryGood
• HomotopicalAlgebra.PathObject.ofFactorizationData_P 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) (CategoryTheory.Limits.diag A)) : (HomotopicalAlgebra.PathObject.ofFactorizationData h).P = h.Z
• HomotopicalAlgebra.PathObject.ofFactorizationData_ι 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) (CategoryTheory.Limits.diag A)) : (HomotopicalAlgebra.PathObject.ofFactorizationData h).ι = h.i
• HomotopicalAlgebra.PathObject.ofFactorizationData_p₀ 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) (CategoryTheory.Limits.diag A)) : (HomotopicalAlgebra.PathObject.ofFactorizationData h).p₀ = CategoryTheory.CategoryStruct.comp h.p CategoryTheory.Limits.prod.fst
• HomotopicalAlgebra.PathObject.ofFactorizationData_p₁ 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) (CategoryTheory.Limits.diag A)) : (HomotopicalAlgebra.PathObject.ofFactorizationData h).p₁ = CategoryTheory.CategoryStruct.comp h.p CategoryTheory.Limits.prod.snd
• HomotopicalAlgebra.PathObject.ofFactorizationData_p 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] {A : C} (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) (CategoryTheory.Limits.diag A)) : (HomotopicalAlgebra.PathObject.ofFactorizationData h).p = h.p
• CochainComplex.Plus.modelCategoryQuillen.instIsStableUnderRetractsFibrations 📋 Mathlib.Algebra.Homology.ModelCategory.Injective
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : (HomotopicalAlgebra.fibrations (CochainComplex.Plus C)).IsStableUnderRetracts
• CochainComplex.Plus.modelCategoryQuillen.instHasFactorizationTrivialCofibrationsFibrations 📋 Mathlib.Algebra.Homology.ModelCategory.Injective
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] : (HomotopicalAlgebra.trivialCofibrations (CochainComplex.Plus C)).HasFactorization (HomotopicalAlgebra.fibrations (CochainComplex.Plus C))
• HomotopicalAlgebra.FibrantBrownFactorization.toMapFactorizationData 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} {f : X ⟶ Y} (self : HomotopicalAlgebra.FibrantBrownFactorization f) : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f
• HomotopicalAlgebra.FibrantBrownFactorization.r 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} {f : X ⟶ Y} (self : HomotopicalAlgebra.FibrantBrownFactorization f) : self.Z ⟶ X
• HomotopicalAlgebra.FibrantBrownFactorization.fibration_r 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} {f : X ⟶ Y} (self : HomotopicalAlgebra.FibrantBrownFactorization f) : HomotopicalAlgebra.Fibration self.r
• HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalenceR 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} (f : X ⟶ Y) (h : HomotopicalAlgebra.FibrantBrownFactorization f) : HomotopicalAlgebra.WeakEquivalence h.r
• HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalencePTrivialCofibrationsFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} (f : X ⟶ Y) (h : HomotopicalAlgebra.FibrantBrownFactorization f) [HomotopicalAlgebra.WeakEquivalence f] : HomotopicalAlgebra.WeakEquivalence h.p
• HomotopicalAlgebra.FibrantBrownFactorization.i_r 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} {f : X ⟶ Y} (self : HomotopicalAlgebra.FibrantBrownFactorization f) : CategoryTheory.CategoryStruct.comp self.i self.r = CategoryTheory.CategoryStruct.id X
• HomotopicalAlgebra.FibrantBrownFactorization.mk' 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} (f : X ⟶ Y) [HomotopicalAlgebra.IsFibrant X] [HomotopicalAlgebra.IsFibrant Y] (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) (CategoryTheory.Limits.prod.lift f (CategoryTheory.CategoryStruct.id X))) : HomotopicalAlgebra.FibrantBrownFactorization f
• HomotopicalAlgebra.FibrantBrownFactorization.i_r_assoc 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} {f : X ⟶ Y} (self : HomotopicalAlgebra.FibrantBrownFactorization f) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp self.i (CategoryTheory.CategoryStruct.comp self.r h) = h
• HomotopicalAlgebra.FibrantBrownFactorization.mk 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} {f : X ⟶ Y} (toMapFactorizationData : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f) (r : toMapFactorizationData.Z ⟶ X) (i_r : CategoryTheory.CategoryStruct.comp toMapFactorizationData.i r = CategoryTheory.CategoryStruct.id X := by cat_disch) (fibration_r : HomotopicalAlgebra.Fibration r := by infer_instance) : HomotopicalAlgebra.FibrantBrownFactorization f
• HomotopicalAlgebra.FibrantBrownFactorization.mk'_Z 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} (f : X ⟶ Y) [HomotopicalAlgebra.IsFibrant X] [HomotopicalAlgebra.IsFibrant Y] (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) (CategoryTheory.Limits.prod.lift f (CategoryTheory.CategoryStruct.id X))) : (HomotopicalAlgebra.FibrantBrownFactorization.mk' f h).Z = h.Z
• HomotopicalAlgebra.FibrantBrownFactorization.mk'_i 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} (f : X ⟶ Y) [HomotopicalAlgebra.IsFibrant X] [HomotopicalAlgebra.IsFibrant Y] (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) (CategoryTheory.Limits.prod.lift f (CategoryTheory.CategoryStruct.id X))) : (HomotopicalAlgebra.FibrantBrownFactorization.mk' f h).i = h.i
• HomotopicalAlgebra.FibrantBrownFactorization.mk'_r 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} (f : X ⟶ Y) [HomotopicalAlgebra.IsFibrant X] [HomotopicalAlgebra.IsFibrant Y] (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) (CategoryTheory.Limits.prod.lift f (CategoryTheory.CategoryStruct.id X))) : (HomotopicalAlgebra.FibrantBrownFactorization.mk' f h).r = CategoryTheory.CategoryStruct.comp h.p CategoryTheory.Limits.prod.snd
• HomotopicalAlgebra.FibrantBrownFactorization.mk'_p 📋 Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.ModelCategory C] {X Y : C} (f : X ⟶ Y) [HomotopicalAlgebra.IsFibrant X] [HomotopicalAlgebra.IsFibrant Y] (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) (CategoryTheory.Limits.prod.lift f (CategoryTheory.CategoryStruct.id X))) : (HomotopicalAlgebra.FibrantBrownFactorization.mk' f h).p = CategoryTheory.CategoryStruct.comp h.p CategoryTheory.Limits.prod.fst
• HomotopicalAlgebra.ModelCategory.hasLiftingProperty_of_joyalTrickDual 📋 Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty] [(HomotopicalAlgebra.trivialCofibrations C).HasFactorization (HomotopicalAlgebra.fibrations C)] [CategoryTheory.Limits.HasPullbacks C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition] [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] (h : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.WeakEquivalence p] [HomotopicalAlgebra.Fibration p], CategoryTheory.HasLiftingProperty i p) {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.Fibration p] [HomotopicalAlgebra.WeakEquivalence i] : CategoryTheory.HasLiftingProperty i p
• HomotopicalAlgebra.instIsStableUnderRetractsOppositeCofibrationsOfFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Opposite
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] [(HomotopicalAlgebra.fibrations C).IsStableUnderRetracts] : (HomotopicalAlgebra.cofibrations Cᵒᵖ).IsStableUnderRetracts
• HomotopicalAlgebra.instIsStableUnderRetractsOppositeFibrationsOfCofibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Opposite
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] [(HomotopicalAlgebra.cofibrations C).IsStableUnderRetracts] : (HomotopicalAlgebra.fibrations Cᵒᵖ).IsStableUnderRetracts
• HomotopicalAlgebra.instHasFactorizationOppositeCofibrationsTrivialFibrationsOfTrivialCofibrationsFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Opposite
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] [(HomotopicalAlgebra.trivialCofibrations C).HasFactorization (HomotopicalAlgebra.fibrations C)] : (HomotopicalAlgebra.cofibrations Cᵒᵖ).HasFactorization (HomotopicalAlgebra.trivialFibrations Cᵒᵖ)
• HomotopicalAlgebra.instHasFactorizationOppositeTrivialCofibrationsFibrationsOfCofibrationsTrivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Opposite
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.ModelCategory C] [(HomotopicalAlgebra.cofibrations C).HasFactorization (HomotopicalAlgebra.trivialFibrations C)] : (HomotopicalAlgebra.trivialCofibrations Cᵒᵖ).HasFactorization (HomotopicalAlgebra.fibrations Cᵒᵖ)
• HomotopicalAlgebra.instIsStableUnderRetractsOverFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Over
  {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.fibrations C).IsStableUnderRetracts] : (HomotopicalAlgebra.fibrations (CategoryTheory.Over S)).IsStableUnderRetracts
• HomotopicalAlgebra.fibrations_over_def 📋 Mathlib.AlgebraicTopology.ModelCategory.Over
  {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [HomotopicalAlgebra.CategoryWithFibrations C] : HomotopicalAlgebra.fibrations (CategoryTheory.Over S) = (HomotopicalAlgebra.fibrations C).over
• HomotopicalAlgebra.instHasFactorizationOverTrivialCofibrationsFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Over
  {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.trivialCofibrations C).HasFactorization (HomotopicalAlgebra.fibrations C)] : (HomotopicalAlgebra.trivialCofibrations (CategoryTheory.Over S)).HasFactorization (HomotopicalAlgebra.fibrations (CategoryTheory.Over S))
• HomotopicalAlgebra.ModelCategory.transport 📋 Mathlib.AlgebraicTopology.ModelCategory.Transport
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [HomotopicalAlgebra.ModelCategory D] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (e : C ≌ D) (h₁ : HomotopicalAlgebra.cofibrations C = (HomotopicalAlgebra.cofibrations D).inverseImage e.functor) (h₂ : HomotopicalAlgebra.fibrations C = (HomotopicalAlgebra.fibrations D).inverseImage e.functor) (h₃ : HomotopicalAlgebra.weakEquivalences C = (HomotopicalAlgebra.weakEquivalences D).inverseImage e.functor) : HomotopicalAlgebra.ModelCategory C
• SSet.modelCategoryQuillen.instIsMultiplicativeFibrations 📋 Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
  : (HomotopicalAlgebra.fibrations SSet).IsMultiplicative
• SSet.modelCategoryQuillen.instIsStableUnderRetractsFibrations 📋 Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
  : (HomotopicalAlgebra.fibrations SSet).IsStableUnderRetracts
• SSet.modelCategoryQuillen.fibrations_eq 📋 Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
  : HomotopicalAlgebra.fibrations SSet = SSet.modelCategoryQuillen.J.rlp

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c