Theorems · Theorem · category theory

SSet.Truncated.Edge.CompStruct.comp_unique

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

Given CompStruct f g h and CompStruct f' g' h' with the same vertices and edges such that f ≃ f' and g ≃ g', then the long diagonal edges h and h' are also homotopic.

Defined in

Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Cited by

1 results in Mathlib

Foundations

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

Assumes

SSet.Truncated.Quasicategory₂