eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-09-24
5:1
5:18
10.4230/LIPIcs.TYPES.2019.5
article
From Cubes to Twisted Cubes via Graph Morphisms in Type Theory
Pinyo, Gun
1
https://orcid.org/0000-0002-8483-5261
Kraus, Nicolai
1
https://orcid.org/0000-0002-8729-4077
School of Computer Science, University of Nottingham, UK
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 higher groupoids. Bezem, Coquand, and Huber [Bezem et al., 2014] have presented a constructive model of univalence using a specific cube category, which we call the BCH cube category.
The higher categories encoded with the BCH cube 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 cube 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).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol175-types2019/LIPIcs.TYPES.2019.5/LIPIcs.TYPES.2019.5.pdf
homotopy type theory
cubical sets
directed equality
graph morphisms