Optics have gained popularity in recent years. They appear in differential categories, compositional game theory, bidirectional accessors, process dependency and causality. At the same time, they remain a bit mysterious: why are they so effective? We claim that, apart from their usual monoidal tensor (⊗), optics have a second, hidden, monoidal tensor (⊲). This tensor structure is the crucial ingredient for some applications of optics, but it hides in plain sight because it is non-representable: the tensor of two objects is not again an object, but only a presheaf. Once we can clearly see this second tensor, optics become a non-representable duoidal algebra that is the universal such one over a monoidal category in a precise sense.

Abstract

We introducePhoto the normal produoidal category of monoidal contexts over an arbitrary monoidal category. In the same sense that a monoidal morphism represents a process, a monoidal context represents an incomplete process: a piece of a decomposition, possibly containing missing parts. We characterize monoidal contexts in terms of universal properties. In particular, symmetric monoidal contexts coincide with monoidal lenses, endowing them with a novel universal property. We apply this algebraic structure to the analysis of multi-party interaction protocols in arbitrary theories of processes.

@inproceedings{earnshaw24:produoidal,
  author       = {Matt Earnshaw and
                  James Hefford and
                  Mario Román},
  editor       = {Aniello Murano and
                  Alexandra Silva},
  title        = {The {Produoidal} {Algebra} of {Process} {Decomposition}},
  booktitle    = {32nd {EACSL} Annual Conference on Computer Science Logic, {CSL} 2024,
                  February 19-23, 2024, Naples, Italy},
  series       = {LIPIcs},
  volume       = {288},
  pages        = {25:1--25:19},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2024},
  url          = {https://doi.org/10.4230/LIPIcs.CSL.2024.25},
  doi          = {10.4230/LIPICS.CSL.2024.25},
}

See also.