Theorems · Inductive type · category theory

HomotopicalAlgebra.PrepathObject.RightHomotopy

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

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

Defined in

Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Cited by

15 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.Category