∀ {A : SSet.Truncated 2} [inst : A.Quasicategory₂]
  {x y z : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {f : SSet.Truncated.Edge x y} {g : SSet.Truncated.Edge y z} {h : SSet.Truncated.Edge x z},
  CategoryTheory.CategoryStruct.comp (SSet.Truncated.HomotopyCategory₂.homMk f)
        (SSet.Truncated.HomotopyCategory₂.homMk g) =
      SSet.Truncated.HomotopyCategory₂.homMk h →
    Nonempty (f.CompStruct g h)