Abstract

The internal language of a category is a device to replace complex diagrammatic reasoning with simpler calculations performed inside a formal theory. A notable example is the Benabou-Mitchell language for elementary toposes (see [LS86]). In [Mai05], a stronger correspondence between various categorical structures (including elementary toposes) and their internal languages based on dependent type theory has been provided. We show how to extend such correspondence by designing an internal language in the sense of [Mai05] for Penon’s quasi-toposes. The internal language of arithmetic quasi-toposes will turn out to be the , impredicative version of the extensional level of the Minimalist Foundation in [M09]. From [MS25, MST25], we derive applications to the foundations of constructive mathematics, regarding in particular the compatibility between some classical, effective, and continuity principles.

This is a joint work with Maria Emilia Maietti.

1. [LS86] J. Lambek and P. J. Scott. Introduction to higher order categorical logic. Cambridge University Press, 1986.
2. [Mai05] M. E. Maietti. Modular correspondence between dependent type theories and categories including pretopoi and topoi. Mathematical Structures in Computer Science, 2005.
3. [Mai09] M. E. Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3):319–354, 2009.
4. [MS25] M. E. Maietti and P. Sabelli. Equiconsistency of the minimalist foundation with its classical version. Annals of Pure and Applied Logic, 2025.
5. [MST25] M. E. Maietti, P. Sabelli, and D. Trotta. Effectiveness and continuity in intuitionistic quasi-toposes of assemblies. Mathematical Structures in Computer Science, 2025.