Theorems · Definition · category theory

HomotopicalAlgebra.PathObject.RightHomotopy

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        HomotopicalAlgebra.PathObject Y → (X ⟶ Y) → (X ⟶ Y) → Type v

Given a path object P for X, two maps f and g in X ⟶ Y are homotopic relative to P when there is a morphism h : P.I ⟶ Y such that P.i₀ ≫ h = f and P.i₁ ≫ h = g.

Defined in

Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Cited by

14 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryHomotopicalAlgebra.CategoryWithWeakEquivalences