×
Gambino, Nicola; Larrea, Marco Federico

Models of Martin-Löf type theory from algebraic weak factorisation systems. (English) Zbl 1527.18004

J. Symb. Log. 88, No. 1, 242-289 (2023).
Summary: We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-Löf type theory. This is done by showing that the comprehension category associated with a type-theoretic algebraic weak factorisation system satisfies the assumptions necessary to apply a right adjoint method for splitting comprehension categories. We then provide methods for constructing several examples of type-theoretic algebraic weak factorisation systems, encompassing the existing groupoid and cubical sets models, as well as new models based on normal fibrations.

Cited in 1 Document

MSC:

18D30 Fibered categories
18N45 Categories of fibrations, relations to \(K\)-theory, relations to type theory
03G30 Categorical logic, topoi

Keywords:

Martin-Löf theory; comprehension category; algebraic weak factorisation system

Software:

cubicaltt
Cite Review PDF
Full Text: DOI arXiv

References:

[1] Awodey, S. and Warren, M. A., Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society, vol. 146 (2009), pp. 45-55. · Zbl 1205.03065
[2] Barthel, T. and Riehl, E., On the construction of functorial factorizations for model categories. Algebraic & Geometric Topology, vol. 13 (2013), no. 2, pp. 1089-1124. · Zbl 1268.18001
[3] Van Den Berg, B. and Garner, R., Topological and simplicial models of identity types. ACM Transactions on Computational Logic, vol. 13 (2012), no. 1, p. 3. · Zbl 1352.03012
[4] Bezem, M. and Coquand, T., A Kripke model for simplicial sets. Theoretical Computer Science, vol. 574 (2015), pp. 86-91. · Zbl 1350.18020
[5] Bourke, J. and Garner, R., Algebraic weak factorisation systems I: Accessible AWFS. Journal of Pure and Applied Algebra, vol. 220 (2016), no. 1, pp. 108-147. · Zbl 1327.18004
[6] Bourke, J. and Garner, R., Algebraic weak factorisation systems II: Categories of weak maps. Journal of Pure and Applied Algebra, vol. 220 (2016), no. 1, pp. 148-174. · Zbl 1327.18005
[7] Cohen, C., Coquand, T., Huber, S., and Mörtberg, A., Cubical type theory: A constructive interpretation of the univalence axiom, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (T. Uustalu, editor), Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, 2018, pp. 5:1-5:34. · Zbl 1434.03036
[8] Conduché, F., Au sujet de l’existence d’adjoints à droite aux foncteurs “image réciproque” dans la catégorie des catégories. Comptes Rendus. Académie des Sciences, vol. 275 (1972), pp. A891-A894. · Zbl 0242.18012
[9] Curien, J.-L., Garner, R., and Hofmann, M., Revisiting the categorical interpretation of dependent type theory. Theoretical Computer Science, vol. 546 (2014), pp. 99-119. · Zbl 1433.03029
[10] Dybjer, P., Internal type theory, Types for Proofs and Programs, TYPES ’95 (S. Berardi and M. Coppo, editors), Lecture Notes in Computer Science, vol. 1185, Springer, Berlin, 1996. · Zbl 0852.00045
[11] Emmenegger, J., Pasquali, F., and Rosolini, G., Elementary fibrations of enriched groupoids. Mathematical Structures in Computer Science, to appear. · Zbl 07547338
[12] Gambino, N. and Garner, R., The identity type weak factorisation system. Theoretical Computer Science, vol. 409 (2008), no. 1, pp. 94-109. · Zbl 1157.68022
[13] Gambino, N. and Henry, S.. Towards a constructive simplicial model of univalent foundations, preprint, 2021, arXiv:1905.06281.
[14] Gambino, N. and Sattler, C., The Frobenius condition, right properness, and uniform fibrations. Journal of Pure and Applied Algebra, vol. 221 (2017), no. 12, pp. 3027-3068. · Zbl 1378.18002
[15] Garner, R., Understanding the small object argument. Applied Categorical Structures, vol. 17 (2009), no. 3, pp. 247-285. · Zbl 1173.55009
[16] Giraud, J., Cohomologie Non Abélienne, Springer, Berlin, 1971. · Zbl 0226.14011
[17] Grandis, M. and Tholen, W., Natural weak factorization systems. Archiv der Mathematik, vol. 42 (2006), no. 4, pp. 397-408. · Zbl 1164.18300
[18] Hofmann, M., On the interpretation of type theory in locally Cartesian closed categories, International Workshop on Computer Science Logic (Pacholski, L. and Tiuryn, J., editors), Springer, Berlin, 1994, pp. 427-441. · Zbl 1044.03544
[19] Hofmann, M. and Streicher, T., Lifting Grothendieck universes, unpublished manuscript, 1997, available from the second-named author’s web page.
[20] Hofmann, M. and Streicher, T., The groupoid interpretation of type theory, Twenty-Five Years of Constructive Type Theory (Venice, 1995), Oxford University Press, 1998, pp. 83-111. · Zbl 0930.03089
[21] Jacobs, B., Comprehension categories and the semantics of type dependency. Theoretical Computer Science, vol. 107 (1993), no. 2, pp. 169-207. · Zbl 0804.18007
[22] Jacobs, B., Categorical Logic and Type Theory, Elsevier, Amsterdam, 1999. · Zbl 0911.03001
[23] Larrea, M. F., Models of dependent type theory from algebraic weak factorisation systems, Ph.D. thesis, University of Leeds, 2018. Available at http://etheses.whiterose.ac.uk/23032.
[24] Lefanu Lumsdaine, P. and Warren, M. A., The local universes model: An overlooked coherence construction for dependent type theories. ACM Transactions on Computational Logic, vol. 16 (2015), no. 3, pp. 1-31. · Zbl 1354.03101
[25] Mac Lane, S., Natural associativity and commutativity. Rice University Studies, vol. 49 (1963), pp. 28-46. · Zbl 0244.18008
[26] Nordström, B., Petersson, K., and Smith, J., Chaper V: Martin-Löf type theory, Handbook of Logic in Computer Science (Abramsky, S., Gabbay, D. M., and Maibaum, T. S. E., editors), Oxford Logic Guides, Oxford University Press, Oxford, 2001, pp. 1-37.
[27] North, P. R., Type-theoretic weak factorization systems, preprint, 2019, arXiv:1906.00259.
[28] Orton, I. and Pitts, A. M., Axioms for modelling cubical type theory in a topos. Logical Methods in Computer Science, vol. 14 (2018), no. 4, pp. 1-33. · Zbl 1509.03054
[29] Riehl, E., Algebraic model structures. New York Journal of Mathematics, vol. 17 (2011), no. 173-231, p. 27. · Zbl 1222.55016
[30] Riehl, E. and Verity, D., The theory and practice of Reedy categories. Theory and Applications of Categories, vol. 29 (2014), no. 9, pp. 256-301. · Zbl 1302.55014
[31] Seely, R.A.G., Locally Cartesian closed categories and type theory. Mathematical Proceedings of the Cambridge Philosophical Society, vol. 95 (1984), pp. 33-48. · Zbl 0539.03048
[32] Streicher, T., Fibred categories à la Jean Bénabou, preprint, 2020, arXiv:1801.02927.
[33] Warren, M. A., Homotopy theoretic aspects of constructive type theory, Ph.D. thesis, Carnegie Mellon University, 2008.
[34] Van Den Woerkom, W. K., Algebraic models of type theory, M.Sc. thesis, Institute for Language, Logic and Computation, University of Amsterdam, 2021. Available at https://eprints.illc.uva.nl/1781/1/MoL-2021-02.text.pdf.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.