License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2019.5
URN: urn:nbn:de:0030-drops-130694
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13069/
Go to the corresponding LIPIcs Volume Portal

Pinyo, Gun ; Kraus, Nicolai

From Cubes to Twisted Cubes via Graph Morphisms in Type Theory

pdf-format:
LIPIcs-TYPES-2019-5.pdf (0.6 MB)

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

BibTeX - Entry

@InProceedings{pinyo_et_al:LIPIcs:2020:13069,
  author =	{Gun Pinyo and Nicolai Kraus},
  title =	{{From Cubes to Twisted Cubes via Graph Morphisms in Type Theory}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{5:1--5:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Marc Bezem and Assia Mahboubi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13069},
  URN =		{urn:nbn:de:0030-drops-130694},
  doi =		{10.4230/LIPIcs.TYPES.2019.5},
  annote =	{Keywords: homotopy type theory, cubical sets, directed equality, graph morphisms}
}

Keywords: homotopy type theory, cubical sets, directed equality, graph morphisms
Collection: 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Issue Date: 2020
Date of publication: 24.09.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI