Theorems · Definition · category theory

SSet.Truncated.HomotopicR

{X : SSet.Truncated 2} →
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })} →
    SSet.Truncated.Edge x y → SSet.Truncated.Edge x y → Prop

Two edges f and g are right homotopic if there is a CompStruct with (0, 1)-edge Edge.id, (1, 2)-edge f, and (0, 2)-edge g. We use Nonempty to have a Prop valued HomotopicR.

Defined in

Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Cited by

7 results in Mathlib

Foundations

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