UnfoldLaws

Law equations for an Unfold[T, B, F] — the build-only / many optic (Optic[Unit, T, Unit, B, Forget[F]] whose real map is embed: F[B] => T).

Like GetterLaws, the primary law is constructor-correctness: the only observable behaviour of a build-only optic is embed, so it must equal whatever reference function the caller claims the unfold represents. The two coherence laws pin the fused andThen members to their specification — post-composition through a Review re-homes the assembled whole ((rev ∘ u).embed = rev.reverseGet ∘ u.embed) and pre-composition maps each part ((u ∘ rev).embed = u.embed ∘ map(rev.reverseGet)) — so an algebra assembled by optic composition cannot drift from the functions it was assembled from.

vestigialSingleton applies only to Applicative-carrier unfolds (built via Unfold.apply): the vestigial read side is pure(()), so a modify round-trip must equal embedding the singleton layer. Pattern-functor unfolds (built via Unfold.algebra) have no lawful read side at all — their vestigial to throws by specification, which is a behaviour check, not a law (see UnfoldSpec).