Theorems · Definition · category theory

HomotopicalAlgebra.PathObject.RightHomotopy.precomp

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        {P : HomotopicalAlgebra.PathObject Y} →
          {f g : X ⟶ Y} →
            P.RightHomotopy f g →
              {Z : C} →
                (i : Z ⟶ X) →
                  P.RightHomotopy (CategoryTheory.CategoryStruct.comp i f) (CategoryTheory.CategoryStruct.comp i g)

Right homotopies are compatible with precomposition.

Defined in

Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Cited by

1 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext

Assumes

CategoryTheory.CategoryHomotopicalAlgebra.CategoryWithWeakEquivalences