This thesis captures the ongoing development of twisted cubes, which is a modification of cubes (in a topological sense) where its homotopy type theory does not require paths or higher paths to be invertible. My original motivation to develop the twisted cubes was to resolve the incompatibility between cubical type theory and directed type theory. The development of twisted cubes is still in the early stages and the intermediate goal, for now, is to define a twisted cube category and its twisted cubical sets that can be used to construct a potential definition of (infinity, n)-categories. The intermediate goal above leads me to discover a novel framework that uses graph theory to transform convex polytopes, such as simplices and (standard) cubes, into base categories. Intuitively, an n-dimensional polytope is transformed into a directed graph consists 0-faces (extreme points) of the polytope as its nodes and 1-faces of the polytope as its edges. Then, we define the base category as the full subcategory of the graph category induced by the family of these graphs from all n-dimensional cases. With this framework, the modification from cubes to twisted cubes can formally be done by reversing some edges of cube graphs. Equivalently, the twisted n-cube graph is the result of a certain endofunctor being applied n times to the singleton graph; this endofunctor (called twisted prism functor) duplicates the input, reverses all edges in the first copy, and then pairwisely links nodes from the first copy to the second copy. The core feature of a twisted graph is its unique Hamiltonian path, which is useful to prove many properties of twisted cubes. In particular, the reflexive transitive closure of a twisted graph is isomorphic to the simplex graph counterpart, which remarkably suggests that twisted cubes not only relate to (standard) cubes but also simplices.
翻译:本论文阐述了扭曲立方体(一种在拓扑意义上对立方体的修正)的持续发展过程,其同伦类型论不要求路径或高阶路径可逆。我最初发展扭曲立方体的动机是为了解决立方体类型论与有向类型论之间的不兼容性。扭曲立方体的发展仍处于早期阶段,当前的中期目标是定义扭曲立方体范畴及相应的扭曲立方体集,以构建(∞, n)-范畴的潜在定义。上述中期目标促使我发现了一种创新框架,该框架利用图论将凸多面体(如单形体与标准立方体)转化为基范畴。直观而言,n维多面体被转化为有向图:以多面体的0-面(极点)为节点,1-面为边。随后,我们将基范畴定义为由所有n维情形下这些图族诱导的图范畴的全子范畴。在此框架下,从立方体到扭曲立方体的修正可通过反向立方体图中的若干边正式实现。等价地,扭曲n-立方体图是将某个自函子(称为扭曲棱镜函子)对单点图连续应用n次的结果;该自函子复制输入图,反转第一个副本的所有边,然后将第一个副本的节点与第二个副本的节点进行成对连接。扭曲图的核心特征是其唯一的哈密顿路径,这一性质有助于证明扭曲立方体的许多特性。特别地,扭曲图的自反传递闭包与单形图自反传递闭包同构,这显著表明扭曲立方体不仅关联标准立方体,也与单形体存在联系。