Are Void and () isomorphic in the presence of laziness?

No, they are not equivalent. What your linked comment and answer are saying is something different: they are saying that different people have different opinions on how to think about undefined in a lazy setting. Some folks will consider Void to have zero possible values and () to have one, because there are no constructors for Void and one constructor (with no fields) for (); meanwhile, other folks will consider Void to have one possible value and () to have two, because undefined is a possible value of either type. These two types of folks don't disagree on any important facts; they only disagree on what kinds of things are interesting/useful to think about. But if you want to cater to both types of people, then you must discuss both ways of thinking when trying to add a field to a data type without changing its meaning -- because the word "meaning" itself has a different meaning to the two types of people.

In fact, it's somewhat common for a single person to hold both points of view! In different contexts, one or the other view is more useful or clear, and it's relatively common to code switch between the two ways of talking about the world.

For the question to make sense, we need to clarify what we mean by "isomorphic", i.e. we should choose a category to interpret Haskell programs in. There are two main options, and both yield a negative answer:

• We can pretend that all Haskell programs are total, and interpret them in the category Set of sets and functions. This approach is pursued in the paper Fast and loose reasoning is morally correct. In this setting, there are no bottom/undefined values, so Void should be interpreted as the empty set and () as the singleton set, which are of course not isomorphic (because there is no total function () → Void). If you upgrade from Haskell to Agda, you can actually prove that they are not isomorphic.
• We can take partiality and laziness into account (but ignore seq) and interpret Haskell programs in a suitable category of CPOs. In that case, Void should be interpreted as the terminal CPO 𝟙 = {⊥}, while () should be the lift of 𝟙, i.e. a CPO with two elements {⊥, ⊤}. These are again not isomorphic in any sense: there are (continuous, even strict) morphisms in both directions, but it is not possible for the round-trip () → Void → () to be the identity on (), because () has two elements while Void has only one (in your snippet, it sends ⊥ to ⊤).

See also Hask is not a category for related discussion.