ModifyFLaws

Carrier-level laws for ModifyF[X, A].

ModifyF[X, A] wraps a pair (Fst[X], Snd[X] => A) — the first component carries "outer state", the second a builder closure that eventually produces the focused A. Its ForgetfulFunctor instance post-composes the builder with the function argument.

Because ModifyF holds a function, structural == cannot witness equality. The laws below therefore assert extensional equality: after applying a law-relevant transformation, the first component and the builder's output on a test input must match the expected values.

The ForgetfulTraverse[ModifyF, Distributive] instance is intentionally not exercised here — writing a standalone law for the distributive-traverse path requires picking a concrete distributive functor (Id is distributive, so the identity law collapses to a tautology). The traverse identity is already exercised through the ModifyLaws discipline suite that consumes this carrier.