I've spent some time recently going down this particular rabbit hole. The original motivation was replacing the current formulation of Applicative laws with the Monoidal-ish one, but one thing led to the other and I ended up making a post about the various sets of laws and related free theorems: https://github.com/alexfmpe/semantic-satiation/blob/main/src/Posts/001-appli...