We now have a wide range of proof assistants available for compositional reasoning in monoidal or higher categories which are free on some generating signature. However, none of these allow us to represent categorical operations such as products, equalizers, and similar logical techniques. Here we show how the foundational mathematical formalism of one such proof assistant can be generalized, replacing the conventional notion of string diagram as a geometrical entity living inside an n-cube with a posetal variant that allows exotic branching structure. We show that these generalized diagrams have richer behaviour with respect to categorical limits, and give an algorithm for computing limits in this setting, with a view towards future application in proof assistants.

翻译：如今我们有多种证明助手可用于在自由生成签名上的幺半范畴或高阶范畴中进行组合推理。然而，这些工具均无法表示乘积、等化子等范畴运算及其类似逻辑技巧。本文展示了如何对其中一种证明助手的基础数学形式体系进行推广：将传统弦图作为嵌入n维立方体的几何实体的概念，替换为允许奇异分支结构的偏序变体。我们证明这些广义图表在范畴极限方面具有更丰富的性质，并给出在此框架下计算极限的算法，旨在为未来在证明助手中的应用奠定基础。