Theorems · Theorem · category theory

SSet.Truncated.HomotopicL.symm

∀ {X : SSet.Truncated 2} [X.Quasicategory₂]
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {f g : SSet.Truncated.Edge x y}, SSet.Truncated.HomotopicL f g → SSet.Truncated.HomotopicL g f

The left homotopy relation is symmetric.

Defined in

Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Cited by

0 results in Mathlib

Foundations

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

Assumes

SSet.Truncated.Quasicategory₂