Monoidal Context and Produoidal Structure

Monoidal context theory holds that a context, a term with a hole, carries a genuine algebraic structure that is not premonoidal but produoidal. A context both admits a subterm dropped into its hole and sequences one context after another, and the two tensors realizing these operations make contexts the objects while optics emerge as the normalized shape a context takes once its interface is exposed.

Categorical methods meet secure computation across three strands, each of which wants a calculus of contexts. Composable cryptography follows the constructive-cryptography lineage of arXiv:2105.05949, where a protocol is a resource transformer and security is a simulation between resources. Graded monads track information flow and differential privacy, whereas state-separating proofs decompose a game into interacting packages. In every strand an adversary or a caller is a term with a hole into which the system under study is plugged, so the question is what categorical structure a context algebra carries.

The answer is produoidal, not premonoidal. A premonoidal category has one tensor that fails interchange, whereas a produoidal category carries two interacting promonoidal structures. One tensor, “before/after”, sequences a context in time, and the other, “context/hole”, splits a context into an outer shell and an inner slot. Neither is an honest monoidal product. Each is instead a promonoidal structure, a functor valued in profunctors given by a family with a unit, so composition is mediated by profunctors rather than by objects. The two structures do not commute on the nose. Instead they are laced together by laxators, coherence maps under which sequencing distributes over hole-splitting only up to a canonical comparison. This laxness forbids the naive premonoidal reading and carries the real content.

The concrete generators are monoidal spliced arrows. A context is a formal splice built from a morphism into the hole and a morphism out of it, with the hole marked by . Splicing composes by nesting one context into the hole of another and by tensoring two contexts side by side, and these are precisely the two produoidal tensors. Raw spliced arrows carry redundant bookkeeping, since the same hole can be presented with different amounts of surrounding wire, so the free structure overcounts.

The top-down characterization removes that redundancy through a splice–contour adjunction and a normalization monad. Contour walks the boundary of an open diagram to read off its splice presentation, and splice reassembles a term from that data, so the two form an adjunction whose induced monad on the produoidal category is idempotent. An idempotent monad is a reflective localization whose algebras are the already-normal objects, and free normalization applies it once. The normal forms are the contexts in which the hole’s residual context has been quotiented away, and that quotient is exactly the existential coend quotient defining an optic.

Therefore optics are the normalized monoidal contexts. In the produoidal presentation the hole carries an interface and a residue, and the Grothendieck-style gluing of interface over residue, together with the coend-like quotient effected by normalization, reproduces the optic coend . The machinery underneath is standard half-representable duoidal category theory, with one tensor representable and the other given by Day convolution, and the coend performing the profunctor composition. The payoff for the study strands is a single vocabulary. An operadic view of nesting and a double-categorical view of the two directions of composition combine with a lens-shaped normal form, making “a term with a hole, filled and sequenced” one structure rather than three ad-hoc calculi for cryptographic contexts.