Document Open Access Logo

From Cubes to Twisted Cubes via Graph Morphisms in Type Theory

Authors Gun Pinyo , Nicolai Kraus

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2019.5.pdf
  • Filesize: 0.55 MB
  • 18 pages

Document Identifiers

Author Details

Gun Pinyo
  • School of Computer Science, University of Nottingham, UK
Nicolai Kraus
  • School of Computer Science, University of Nottingham, UK

Funding

  • Kraus, Nicolai: The Royal Society, grant No. URF\R1\191055.

Acknowledgements

We would like to thank Paolo Capriotti and Jakob von Raumer. Both offered many suggestions during fruitful exchanges. In particular, the initial observation on which Theorem 21 is based was suggested by them, and the idea of considering graph morphisms was found in one of our many interesting discussions. We are also grateful to the participants of TYPES'19 in Oslo and the summer school on HTT/UF in Leeds. We thank in particular Emily Riehl, Christian Sattler, and Steve Awodey for their help and their comments. Special thanks go to Andreas Nuyts, who has pointed out a mistake in an earlier draft of this paper, and to the anonymous reviewers for their careful reading and comments.

Cite As Get BibTex

Gun Pinyo and Nicolai Kraus. From Cubes to Twisted Cubes via Graph Morphisms in Type Theory. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.TYPES.2019.5

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

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • homotopy type theory
  • cubical sets
  • directed equality
  • graph morphisms

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. I. R. Aitchison. The geometry of oriented cubes. ArXiv e-prints, 2010. URL: http://arxiv.org/abs/1008.1714.
  2. Thorsten Altenkirch and Ambrus Kaposi. Towards a Cubical Type Theory without an Interval. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 3:1-3:27, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.3.
  3. Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, and Daniel R. Licata. Cartesian cubical type theory. URL: https://github.com/dlicata335/cart-cube/blob/master/cart-cube.pdf.
  4. Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. Two-level type theory and applications. ArXiv e-prints, 2019. URL: http://arxiv.org/abs/1705.03307.
  5. Rosa Antolini. Geometric realisations of cubical sets with connections, and classifying spaces of categories. Applied Categorical Structures, 2002. Google Scholar
  6. Steve Awodey. A cubical model of homotopy type theory. Annals of Pure and Applied Logic, 2018. Google Scholar
  7. Hans-Joachim Baues and Günther Wirsching. Cohomology of small categories. Journal of pure and applied algebra, 38(2-3):187-211, 1985. See also URL: https://ncatlab.org/nlab/show/category+of+factorizations.
  8. Marc Bezem, Thierry Coquand, and Simon Huber. A model of type theory in cubical sets. 19th International Conference on Types for Proofs and Programs (TYPES 2013), 2014. Google Scholar
  9. Ulrik Buchholtz and Edward Morehouse. Varieties of cubical sets. Relational and Algebraic Methods in Computer Science, 2017. Google Scholar
  10. Paolo Capriotti. Models of Type Theory with Strict Equality. PhD thesis, School of Computer Science, University of Nottingham, Nottingham, UK, 2016. Available online at URL: https://arxiv.org/abs/1702.04912.
  11. Paolo Capriotti and Nicolai Kraus. Univalent higher categories via complete semi-segal types. Proceedings of the ACM on Programming Languages, 2(POPL'18):44:1-44:29, December 2017. Full version available at https://arxiv.org/abs/1707.03693. URL: https://doi.org/10.1145/3158132.
  12. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: A constructive interpretation of the univalence axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:34, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  13. Nicola Gambino and Christian Sattler. The frobenius condition, right properness, and uniform fibrations. Journal of Pure and Applied Algebra, 221(12):3027-3068, 2017. Google Scholar
  14. Philip S Hirschhorn. Model categories and their localizations. American Mathematical Soc., 2009. Google Scholar
  15. Simon Huber. Cubical Interpretations of Type Theory. PhD thesis, Department of Computer Science and Engineering, University of Gothenburg, 2016. Google Scholar
  16. Chris Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of univalent foundations (after voevodsky). ArXiv e-prints, November 2012. To appear in the Journal of the European Mathematical Society. URL: http://arxiv.org/abs/1211.2851.
  17. F William Lawvere. Equality in hyperdoctrines and comprehension schema as an adjoint functor. Applications of Categorical Algebra, 17:1-14, 1970. See also URL: https://ncatlab.org/nlab/show/twisted+arrow+category.
  18. Daniel R Licata and Robert Harper. 2-dimensional directed type theory. Electronic Notes in Theoretical Computer Science, 276:263-289, 2011. Google Scholar
  19. Jacob Lurie. Higher Topos Theory. Annals of Mathematics Studies. Princeton University Press, Princeton, 2009. Also avaialabe online at http://arxiv.org/abs/math/0608040; see also https://ncatlab.org/nlab/show/join+of+categories.
  20. Clive Newstead. Cubical sets. URL: http://math.cmu.edu/~cnewstea/notes/cubicalsets.pdf.
  21. Paige Randall North. Towards a directed homotopy type theory. Electronic Notes in Theoretical Computer Science, 347:223-239, 2019. Google Scholar
  22. Andreas Nuyts. Towards a directed homotopy type theory based on 4 kinds of variance. Master’s thesis, KU Leuven, 2015. Google Scholar
  23. I. Orton and A. M. Pitts. Axioms for modelling cubical type theory in a topos. Logical Methods in Computer Science, 2018. Special issue for CSL 2016. Google Scholar
  24. Charles Rezk. A model for the homotopy theory of homotopy theory. Transactions of the American Mathematical Society, 2001. Google Scholar
  25. Emily Riehl and Michael Shulman. A type theory for synthetic ∞-categories. Higher Structures, 1(1), 2017. URL: https://journals.mq.edu.au/index.php/higher_structures/article/view/36.
  26. Michael Shulman. The univalence axiom for elegant Reedy presheaves. Homology, Homotopy and Applications, 2015. URL: https://doi.org/10.4310/HHA.2015.v17.n2.a6.
  27. Michael Shulman. Univalence for inverse diagrams and homotopy canonicity. Mathematical Structures in Computer Science, 2015. Google Scholar
  28. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  29. Vladimir Voevodsky. Univalent foundations project. A modified version of an NSF grant application, 2010. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact