Abstract

Palmgren’s Intuitionistic Ramified Type Theory (IRTT) can be seen as ramified (or predicative) version of the internal set theory of an elementary topos. This theory has a straightforward interpretation, using setoids, in intensional Martin-Löf type theory with a cumulative sequence of universes. Palmgren proposed that this would be a natural approach for obtaining a predicative notion of an elementary topos.

In this talk I will report on ongoing work investigating categorical properties of IRTT and its relation to the proposed notions of predicative toposes given thus far. The phrase ramified local set theories (RLST), rather than IRTT, has been chosen primarily to better conform with the local set theories of Bell, but also includes some modifications of Palmgren’s original theory. I will generalize the notions of hyperdoctrine and tripos to the ramified case to obtain structures that can faithfully interpret the ramified languages of IRTT and RLST and, conversely, whose internal logic are languages of the same kind.

If time allows, I will discuss the tripos-to-topos construction in this setting and its various free components as identified and studied by Maietti, Rosolini and Pasquali, and possible connections with minimalist foundations.