Gun Pinyo | arXiv Science

arXiv2023

Twisted Cubes and their Applications in Type Theory

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.

cs.LO↗

arXiv2019

From Cubes to Twisted Cubes via Graph Morphisms in Type Theory

Cube categories are used to encode higher-dimensional categorical structures. They have recently gained significant attention in the community of homotopy type theory and univalent foundations, where types carry the structure of such higher groupoids. Bezem, Coquand, and Huber have presented a constructive model of univalence using a specific cube category, which we call the BCH category. The higher categories encoded with the BCH category have the property that all morphisms are invertible, mirroring the fact that equality is symmetric. This might not always be desirable: the field of directed type theory considers a notion of equality that is not necessarily invertible. This motivates us to suggest a category of twisted cubes which avoids built-in invertibility. Our strategy is to first develop several alternative (but equivalent) presentations of the BCH category using morphisms between suitably defined graphs. Starting from there, a minor modification allows us to define our category of twisted cubes. We prove several first results about this category, and our work suggests that twisted cubes combine properties of cubes with properties of globes and simplices (tetrahedra).

cs.LO↗