∀ {X Y : SSet.Truncated 2}
  (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := SSet.Truncated.Edge.tensor._proof_1 }))
  {y₀ y₁ : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e : SSet.Truncated.Edge y₀ y₁),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).map
      (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (SSet.Truncated.HomotopyCategory.mk x))
        (SSet.Truncated.HomotopyCategory.homMk e)) =
    SSet.Truncated.HomotopyCategory.homMk ((SSet.Truncated.Edge.id x).tensor e)