首页    期刊浏览 2024年11月25日 星期一
登录注册

文章基本信息

  • 标题:From Cubes to Twisted Cubes via Graph Morphisms in Type Theory
  • 本地全文:下载
  • 作者:Gun Pinyo ; Nicolai Kraus
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2020
  • 卷号:175
  • 页码:1-18
  • DOI:10.4230/LIPIcs.TYPES.2019.5
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要: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).
  • 关键词:homotopy type theory; cubical sets; directed equality; graph morphisms
国家哲学社会科学文献中心版权所有