Document Open Access Logo

Categorical Structures for Type Theory in Univalent Foundations

Authors Benedikt Ahrens, Peter LeFanu Lumsdaine, Vladimir Voevodsky

PDF
Thumbnail PDF

File

LIPIcs.CSL.2017.8.pdf
  • Filesize: 0.53 MB
  • 16 pages

Document Identifiers

Author Details

Benedikt Ahrens
Peter LeFanu Lumsdaine
Vladimir Voevodsky

Cite As Get BibTex

Benedikt Ahrens, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. Categorical Structures for Type Theory in Univalent Foundations. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CSL.2017.8

Abstract

In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in the setting of univalent foundations, where the relationships between them can be stated more transparently. Specifically, we construct maps between the different structures and show that these maps are equivalences under suitable assumptions.

We then analyze how these structures transfer along (weak and strong) equivalences of categories, and, in particular, show how they descend from a category (not assumed univalent/saturated) to its Rezk completion. To this end, we introduce relative universes, generalizing the preceding notions, and study the transfer of such relative universes along suitable structure.

We work throughout in (intensional) dependent type theory; some results, but not all, assume the univalence axiom. All the material of this paper has been formalized in Coq, over the UniMath library.

Subject Classification

Keywords
  • Categorical Semantics
  • Type Theory
  • Univalence Axiom

Metrics

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

References

  1. Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. Mathematical Structures in Computer Science, 25:1010-1039, 2015. http://arxiv.org/abs/1303.0584, URL: http://dx.doi.org/10.1017/S0960129514000486.
  2. Thorsten Altenkirch, James Chapman, and Tarmo Uustalu. Monads need not be endofunctors. Logical Methods in Computer Science, 11(1), 2015. URL: http://dx.doi.org/10.2168/LMCS-11(1:3)2015.
  3. Steve Awodey. Natural models of homotopy type theory. Mathematical Structures in Computer Science, pages 1-46, 2016. http://arxiv.org/abs/1406.3219, URL: http://dx.doi.org/10.1017/S0960129516000268.
  4. John Cartmell. Generalised algebraic theories and contextual categories. Ph.D. Thesis, Oxford University, 1978. URL: http://www.cs.ru.nl/~spitters/Cartmell.pdf.
  5. John Cartmell. Generalised algebraic theories and contextual categories. Ann. Pure Appl. Logic, 32:209-243, 1986. URL: http://dx.doi.org/10.1016/0168-0072(86)90053-9.
  6. Peter Dybjer. Internal type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers, volume 1158 of Lecture Notes in Computer Science, pages 120-134. Springer, 1995. URL: http://dx.doi.org/10.1007/3-540-61780-9_66.
  7. Marcelo Fiore. Discrete generalised polynomial functors, 2012. Slides from talk given at ICALP 2012. URL: http://www.cl.cam.ac.uk/~mpf23/talks/ICALP2012.pdf.
  8. Martin Hofmann. Syntax and semantics of dependent types. In Semantics and Logics of Computation, pages 79-130. Cambridge University Press, 1997. Google Scholar
  9. William A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 479-490. Academic Press, 1980. Reprint of 1969 article. Google Scholar
  10. Andrew M. Pitts. Categorical logic. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, Volume 5. Algebraic and Logical Structures, chapter 2, pages 39-128. Oxford University Press, 2000. URL: http://www.oup.co.uk/isbn/0-19-853781-6.
  11. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. The Univalent Foundations Program, Institute for Advanced Study, 2013. URL: http://homotopytypetheory.org/book.
  12. Benno van den Berg and Richard Garner. Topological and simplicial models of identity types. ACM Trans. Comput. Logic, 13(1):3:1-3:44, January 2012. URL: http://dx.doi.org/10.1145/2071368.2071371.
  13. Vladimir Voevodsky. A C-system defined by a universe category. Theory Appl. Categ., 30(37):1181-1215, 2015. URL: http://www.tac.mta.ca/tac/volumes/30/37/30-37.pdf.
  14. Vladimir Voevodsky. An experimental library of formalized mathematics based on the univalent foundations. Math. Structures Comput. Sci., 25(5):1278-1294, 2015. URL: http://dx.doi.org/10.1017/S0960129514000577.
  15. Vladimir Voevodsky. Subsystems and regular quotients of C-systems. In Conference on Mathematics and its Applications, (Kuwait City, 2014), number 658 in Contemporary Mathematics, pages 127-137, 2016. URL: http://arxiv.org/abs/1406.7413.
  16. Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. UniMath: Univalent Mathematics. URL: https://github.com/UniMat.
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