LIPIcs.CSL.2017.8.pdf
- Filesize: 0.53 MB
- 16 pages
Document
Categorical Structures for Type Theory in Univalent Foundations
Authors
-
Part of:
Volume:
26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2017-08-16
Cite AsGet 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
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.
Keywords
- Categorical Semantics
- Type Theory
- Univalence Axiom
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- 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.
- 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.
- 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.
- John Cartmell. Generalised algebraic theories and contextual categories. Ph.D. Thesis, Oxford University, 1978. URL: http://www.cs.ru.nl/~spitters/Cartmell.pdf.
- 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.
- 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.
- 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.
-
Martin Hofmann. Syntax and semantics of dependent types. In Semantics and Logics of Computation, pages 79-130. Cambridge University Press, 1997.
-
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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. UniMath: Univalent Mathematics. URL: https://github.com/UniMat.