dev.constructive.eo.laws.eo

Associativity of andThen: the two bracketings of a three-optic chain behave identically. The spec materialises both leftNested = (a ∘ b) ∘ c and rightNested = a ∘ (b ∘ c) because the law trait can't call .andThen itself (the carrier's leftover X is abstract here — the same reason dev.constructive.eo.laws.typeclass.AssociativeFunctorLaws takes a materialised composed).

• associativeModify holds for any ForgetfulFunctor[F] carrier.
• associativeGet additionally requires Accessor[F] (a total-read carrier).

No andThen identity unit law (o ∘ id == o == id ∘ o) is stated: core ships no identity-optic constructor (no Iso.id / Optic.id), so there is nothing lawful to compose against. Add the unit law here if such a constructor lands.

Compose-coherence for folding. For composed = outer.andThen(inner), composed.foldMap(f)(s) == outer.foldMap(a => inner.foldMap(f)(a))(s) — folding the whole chain equals folding each outer focus through the inner fold. Keyed by CanFold on all three legs (every readable family; the primary surface of Fold and Traversal).

Compose-coherence for total read. For composed = outer.andThen(inner), composed.get(s) == inner.get(outer.get(s)) — reading through the whole chain equals reading the outer focus, then the inner. Keyed by CanGet on all three legs (Lens / Iso / Getter and their total-read composites).

Compose-coherence for partial read. For composed = outer.andThen(inner), composed.getOption(s) == outer.getOption(s).flatMap(inner.getOption) — the Kleisli law over Option. Keyed by CanGetOption on all three legs (Prism / Optional / AffineFold and their partial-read composites).

Compose-coherence for building. For composed = outer.andThen(inner), composed.reverseGet(c) == outer.reverseGet(inner.reverseGet(c)) — building through the chain equals building the inner focus, then re-homing it via the outer. Keyed by CanReverseGet on all three legs (Iso / Prism / Review and their build composites).

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. Both composedGet and composedReverseGet are inherited from the capability layer.

C1/C2 — Lens ∘ Lens composition laws. composedGet is inherited from ComposedGetLaws; composedReplace is the Lens-specific write-seam law.

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. composedGetOption is inherited from the capability layer; composedModifyIdentity is the Optional-specific write-seam law.

C5 — Prism ∘ Prism composition laws. Both composedGetOption and composedReverseGet are inherited from the capability layer.

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.