Internal ∞-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT

Kraus, Nicolai

Abstract

Using dependent type theory to formalise the syntax of dependent type theory is a very active topic of study and goes under the name of "type theory eating itself" or "type theory in type theory." Most approaches are at least loosely based on Dybjer's categories with families (CwF's) and come with a type Con of contexts, a type family Ty indexed over it modelling types, and so on. This works well in versions of type theory where the principle of unique identity proofs (UIP) holds. In homotopy type theory (HoTT) however, it is a long-standing and frequently discussed open problem whether the type theory "eats itself" and can serve as its own interpreter. The fundamental underlying difficulty seems to be that categories are not suitable to capture a type theory in the absence of UIP. In this paper, we develop a notion of ∞-categories with families (∞-CwF's). The approach to higher categories used relies on the previously suggested semi-Segal types, with a new construction of identity substitutions that allow for both univalent and non-univalent variations. The type-theoretic universe as well as the internalised (set-level) syntax are models, although it remains a conjecture that the latter is initial. To circumvent the known unsolved problem of constructing semisimplicial types, the definition is presented in two-level type theory (2LTT). Apart from introducing ∞-CwF's, the paper explains the shortcomings of 1-categories in type theory without UIP as well as the difficulties of and approaches to internal higher-dimensional categories.

Citation

Kraus, N. (2021, June). Internal ∞-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT. Presented at LICS'21 - ACM/IEEE Symposium on Logic in Computer Science, Rome, Italy

• Presentation Conference Type: Edited Proceedings
• Conference Name: LICS'21 - ACM/IEEE Symposium on Logic in Computer Science
• Start Date: Jun 29, 2021
• End Date: Jul 3, 2021
• Acceptance Date: Apr 1, 2021
• Online Publication Date: Jul 7, 2021
• Publication Date: 2021-07
• Deposit Date: Oct 3, 2024
• Publicly Available Date: Oct 10, 2024
• Publisher: Institute of Electrical and Electronics Engineers
• Peer Reviewed: Peer Reviewed
• Book Title: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
• ISBN: 978-1-6654-4896-3
• DOI: https://doi.org/10.1109/LICS52264.2021.9470667
• Public URL: https://nottingham-repository.worktribe.com/output/5748467
• Publisher URL: https://ieeexplore.ieee.org/document/9470667