dev.constructive.eo.laws.eo

E1 — optic.foldMap is a Monoid homomorphism on the target monoid (tested at Int with additive Monoid[Int], which is enough to witness the law).

C3/C4 — Iso ∘ Iso composition laws.

C1/C2 — Lens ∘ Lens composition laws.

D3 — optic.modifyA[Const[M, *]] is pointwise equal to optic.foldMap on the same function, with M = Int (additive).

D1 — optic.modifyA[Id] is pointwise equal to optic.modify.

Laws that pin down Optic.morph — EO's carrier-coercion extension.

A1/I1. Morph preserves modify: reshaping the carrier does not change what the optic does to the focus.

A2. Morph preserves get: for any carriers F / G that both expose Accessor, reshaping preserves the read path as well.

These two laws are the foundation of EO's "write once, reuse everywhere" claim about optics. If they failed, a user could not safely convert a Lens to an Optional or a Getter to a Fold without changing observable behaviour.

Optional ∘ Optional composition laws.

C5 — Prism ∘ Prism composition laws.

H3 — Iso put is the curried reverseGet ∘ pure.

B1 — Iso reverse is involutive on both get and reverseGet.

H1/H2/H4 — Lens transform / place / transfer mutually agree.