论文标题
通过依赖光学元件看到双重
Seeing double through dependent optics
论文作者
论文摘要
Tambara模块是单体类别之间的强大分配器。 Tambara在表示理论的背景下定义了它们，但是当被理解的Tambara模块提供了一种有用的模块化数据访问器时，很快就在应用程序中找到了自己的方式。为了满足这些应用的需求，Tambara理论已扩展到接受单类别类别的类别之间的分配因素。通过将光学概括为相关类型上下文的概括，我们通过将它们定义为水平自然变换来绘制Tambara模块理论的进一步扩展。在这种情况下，对与分解器表示有关的五街理论的定理和构造与分解器表示相关。这重现了Vertechi和Milewski最近提出的依赖光学的定义，并由作者及其合作者的先前工作暗示。
Tambara modules are strong profunctors between monoidal categories. They've been defined by Tambara in the context of representation theory, but quickly found their way in applications when it was understood Tambara modules provide a useful encoding of modular data accessors known as mixed optics. To suit the needs of these applications, Tambara theory has been extended to profunctors between categories receiving an action of a monoidal category. Motivated by the generalization of optics to dependently-typed contexts, we sketch a further extension of the theory of Tambara modules in the setting of actions of double categories (thus doubly indexed categories), by defining them as horizontal natural transformations. The theorems and constructions in Pastro-Street theory relevant to profunctor representation theorem for mixed optics are reobtained in this context. This reproduces the definition of dependent optics recently put forward by Vertechi and Milewski, and hinted at by previous work of the author and his collaborators.
