Johan Lindberg: Properties of the category of local sets in Intuitionistic ramified type theory

Abstract: In [Pal17] Palmgren introduces a ramified type theory based on intuitionistic logic called IRTT, which is inspired by the modern formulation of Russell’s and Whitehead’s type theory in Principia Mathematica described in [KLN02]. IRTT contains a version of the reducibility axiom but can still be shown to be predicative by interpreting it in Martin-Löf type theory.

Palmgren also introduces a category of local sets (which are terms of powertypes) in IRTT, and expects this to form a natural notion of a predicative topos.

We establish some properties of this category and, in particular, show that it is a Π-pretopos with a natural numbers object. Extending IRTT with a principle allowing for inductive definitions (due to Palmgren) and a replacement axiom we show that the category of local sets form a ΠW-pretopos.

References:
[KLN02] F. Kamareddine, T. Laan, and R. Nederpelt. Types in Logic and Mathematics before
1940. Bulletin of Symbolic Logic (8), 2002.
[Pal17] E. Palmgren. A constructive examination of a Russell-style ramified type theory, 2017, arxiv.org/abs/1704.06812