扭曲的立方体及其在类型理论中的应用
摘要：扭曲立方体的发展和演进，这是对立方体（在拓扑意义上）的修改，其同伦类型理论不要求路径或高阶路径是可逆的。我发展扭曲立方体最初的动机是为了解决立方体类型理论和定向类型理论之间的不兼容性。扭曲立方体的发展仍处于早期阶段，目前的中间目标是定义一个扭曲立方体范畴及其扭曲立方集合，以构建(无穷，n)范畴的潜在定义。上述中间目标导致我发现了一个新颖的框架，利用图论将凸多面体（如单纯形和（标准）立方体）转化为基础范畴。直观地说，将n维多面体转化为一个有向图，其节点是多面体的0面（极端点），边是多面体的1面。然后，我们将基础范畴定义为由所有n维情况下的这些图的族诱导的图范畴的全子范畴。使用这个框架，从立方体到扭曲立方体的修改可以通过翻转立方体图中的一些边来正式完成。等价地，扭曲n-立方图是将某个自函子（称为扭曲棱柱函子）应用n次于单位图的结果；这个自函子复制输入，翻转第一个副本中的所有边，并将第一个副本的节点与第二个副本的节点成对地连接。扭曲图的核心特征是其唯一的汉密尔顿路径，这对于证明扭曲立方体的许多特性非常有用。特别地，扭曲图的自反传递闭包与单纯形图对应，这表明扭曲立方体不仅与（标准）立方体相关，还与单纯形相关。
作者：Gun Pinyo
论文ID：2307.01327
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-06