dev.constructive.eo.laws.data

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

Affine is the carrier behind Optional: a sum of a "no write path" case (Fst[X]) and a tuple-like "got the focus" case ((Snd[X], A)). The laws pin down its two main type-class instances:

• ForgetfulFunctor[Affine] — identity and composition.
• ForgetfulTraverse[Affine, Applicative] at Id — identity.

The AssociativeFunctor[Affine, X, Y] instance is already exercised by Optional ∘ Optional at the optic level (see dev.constructive.eo.laws.eo.OptionalComposeLaws); re-stating its associativity equations as a standalone law class would duplicate that coverage without adding signal.

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.