From Cubes to Twisted Cubes via Graph Morphisms in Type Theory

Pinyo, Gun; Kraus, Nicolai

Abstract

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).

Citation

Pinyo, G., & Kraus, N. (2019, June). From Cubes to Twisted Cubes via Graph Morphisms in Type Theory. Paper presented at TYPES 2019, Oslo, Norway

• Presentation Conference Type: Conference Paper (unpublished)
• Conference Name: TYPES 2019
• Start Date: Jun 11, 2019
• End Date: Jun 14, 2019
• Deposit Date: Jul 15, 2020
• Publicly Available Date: Aug 7, 2020
• Keywords: Logic in Computer Science
• Public URL: https://nottingham-repository.worktribe.com/output/2461870
• Related Public URLs: https://cas.oslo.no/types2019/
• Additional Information: Article no. 5