逻辑结构化半严格高阶范畴的Posetal图示
摘要：在一些生成签名上，我们现在有一系列可用于单调或高品类的组合推理的证明助手。然而，这些助手都不允许我们表示范畴操作，如积、等值器和类似的逻辑技术。本文展示了一个这样的证明助手的基础数学形式如何被泛化，用具有允许异类分支结构的泛义的偏序概念来替代传统的在n-立方体内生活的几何实体的链图的概念。我们展示了这些广义图在范畴极限方面具有更丰富的行为，并给出了在此设置中计算极限的算法，以期在未来的证明助手中应用。
作者：Chiara Sarti and Jamie Vicary
论文ID：2305.11637
分类：Category Theory
分类简称：math.CT
提交时间：2023-07-11