Lawvere theories

Yes, having a Signature x -> x as operations is definitely easier to work with, and extending signatures and laws in a tower of varieties evidently works, too.

In your Variety class, I can see why Requirements var x is a useful context for lawful. But I fail to see why the same constraint should be needed for the operations. Why would a Semigroup need to have an Eq instance?

The Variety class has a less tight coupling between the signature and the laws; they could be entirely unrelated types. In contrast, Lawvere takes the signature as part of the skeleton of the category the laws are written in.