Theorems · Definition · category theory

HomotopicalAlgebra.CofibrantBrownFactorization.mk.noConfusion

{C : Type u_1} →
  {inst : CategoryTheory.Category.{v_1, u_1} C} →
    {inst_1 : HomotopicalAlgebra.ModelCategory C} →
      {X Y : C} →
        {f : X ⟶ Y} →
          {P : Sort u} →
            {toMapFactorizationData :
                (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f} →
              {s : Y ⟶ toMapFactorizationData.Z} →
                {s_p :
                    autoParam
                      (CategoryTheory.CategoryStruct.comp s toMapFactorizationData.p =
                        CategoryTheory.CategoryStruct.id Y)
                      HomotopicalAlgebra.CofibrantBrownFactorization.s_p._autoParam} →
                  {cofibration_s :
                      autoParam (HomotopicalAlgebra.Cofibration s)
                        HomotopicalAlgebra.CofibrantBrownFactorization.cofibration_s._autoParam} →
                    {toMapFactorizationData' :
                        (HomotopicalAlgebra.cofibrations C).MapFactorizationData
                          (HomotopicalAlgebra.trivialFibrations C) f} →
                      {s' : Y ⟶ toMapFactorizationData'.Z} →
                        {s_p' :
                            autoParam
                              (CategoryTheory.CategoryStruct.comp s' toMapFactorizationData'.p =
                                CategoryTheory.CategoryStruct.id Y)
                              HomotopicalAlgebra.CofibrantBrownFactorization.s_p._autoParam} →
                          {cofibration_s' :
                              autoParam (HomotopicalAlgebra.Cofibration s')
                                HomotopicalAlgebra.CofibrantBrownFactorization.cofibration_s._autoParam} →
                            { toMapFactorizationData := toMapFactorizationData, s := s, s_p := s_p,
                                  cofibration_s := cofibration_s } =
                                { toMapFactorizationData := toMapFactorizationData', s := s', s_p := s_p',
                                  cofibration_s := cofibration_s' } →
                              (toMapFactorizationData ≍ toMapFactorizationData' → s ≍ s' → P) → P

Defined in

Mathlib.AlgebraicTopology.ModelCategory.BrownLemma

Cited by

1 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound