The analogy between universes in type theory and the Mahlo hierarchy in set theory has been analyzed in many different ways by Michael Rathjen. (This builds on his analysis of KPM, but ML type theories with universes came in later in the game.)
I don't have the Palmgren paper you refer to, but I think the following paper is closely related to your questions:
Rathjen, Griffor, Palmgren, Inaccessibility in constructive set theory and type theory, Ann. Pure Appl. Logic 94 (1998), 181-200.
This is not the only way of relating universes in type theory and inaccessibles in set theory, another one is presented by Anton Setzer in Extending Martin-Löf type theory by one Mahlo-universe and further investigated by Rathjen in Realizing Mahlo set theory in type theory.
No comments:
Post a Comment