Theorems · Definition · category theory

HomotopicalAlgebra.PathObject.RightHomotopy.trans

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : HomotopicalAlgebra.ModelCategory C] →
        {P : HomotopicalAlgebra.PathObject Y} →
          [inst_2 : HomotopicalAlgebra.IsFibrant Y] →
            {f₀ f₁ f₂ : X ⟶ Y} →
              P.RightHomotopy f₀ f₁ →
                {P' : HomotopicalAlgebra.PathObject Y} →
                  [inst_3 : P'.IsGood] →
                    P'.RightHomotopy f₁ f₂ →
                      [CategoryTheory.Limits.HasPullback P.p₁ P'.p₀] → (P.trans P').RightHomotopy f₀ f₂

If f₀ : X ⟶ Y is homotopic to f₁ relative to a path object P, and f₁ is homotopic to f₂ relative to a good path object P', then f₀ is homotopic to f₂ relative to the path object P.trans P' when Y is fibrant.

Defined in

Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryHomotopicalAlgebra.ModelCategoryHomotopicalAlgebra.IsFibrantHomotopicalAlgebra.PathObject.IsGoodCategoryTheory.Limits.HasPullback