A General Construction of Strict Models in HoTT
Abstract
Homotopy type theory (HoTT) provides a natural setting for studying the metatheory of type theory, as it comes with additional extensionality principles compared to ordinary Martin-Löf type theory. In particular, it is especially suitable for developing semantics of type theory, where one distinguishes two kinds of models: strict models, which give us sound interpretations, and pseudomodels. Pseudomodels are useful as they occur prevalently and can be turned into strict models by constructions called strictifications. However, the commonly used strictifications do not translate well to HoTT, as they require assumptions that are generally not satisfied by concrete examples of models. We show how to carry out the universe model construction, due to Voevodsky, in HoTT. Under this construction, every pseudomodel together with a universe type closed under enough type formers gives rise to a strict model. We also show how to interpret type formers in the resulting model assuming that the universe is closed under them. Finally, we demonstrate that this construction generalises existing instances of strict set models in the literature, and we apply it to more examples, yielding presheaf models and assembly models of type theory in HoTT. Our results are formalised in Rocq using the UniMath library.
Related
- Functoriality of the KSGNS Construction for Intertwiners of Strict Positive C*-Correspondences
- The third symmetric product of a set is a set in HoTT
- Construction of parametrized families of general pseudo-bimagic and bimagic squares
- A General Construction of Codes from Drinfeld Modules
- Strict weak Hörmander conditions for hypoellipticity and structure equations
BibTeX
@misc{najmaei2026general,
title = {{A General Construction of Strict Models in HoTT}},
author = {Niyousha Najmaei and Niels van der Weide},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.28370},
eprint = {2610.28370},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.28370},
}
RIS
TY - UNPB
TI - A General Construction of Strict Models in HoTT
AU - Niyousha Najmaei
AU - Niels van der Weide
PY - 2026
DA - 2026/10/20
PB - arXiv
DO - 10.48550/arxiv.2610.28370
UR - https://arxiv.org/abs/2610.28370
AB - Homotopy type theory (HoTT) provides a natural setting for studying the metatheory of type theory, as it comes with additional extensionality principles compared to ordinary Martin-Löf type theory. In particular, it is especially suitable for developing semantics of type theory, where one distinguishes two kinds of models: strict models, which give us sound interpretations, and pseudomodels. Pseudomodels are useful as they occur prevalently and can be turned into strict models by constructions called strictifications. However, the commonly used strictifications do not translate well to HoTT, as they require assumptions that are generally not satisfied by concrete examples of models. We show how to carry out the universe model construction, due to Voevodsky, in HoTT. Under this construction, every pseudomodel together with a universe type closed under enough type formers gives rise to a strict model. We also show how to interpret type formers in the resulting model assuming that the universe is closed under them. Finally, we demonstrate that this construction generalises existing instances of strict set models in the literature, and we apply it to more examples, yielding presheaf models and assembly models of type theory in HoTT. Our results are formalised in Rocq using the UniMath library.
ER -