∀ {V : SSet.Truncated 2}
  (x : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := SSet.OneTruncation₂._proof_1 })),
  SSet.Truncated.HomotopyCategory.homMk (SSet.Truncated.Edge.id x) =
    CategoryTheory.CategoryStruct.id (SSet.Truncated.HomotopyCategory.mk x)