Skip to main content
fixed grammar and clarity
Source Link
François G. Dorais
  • 44.4k
  • 6
  • 150
  • 233

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 all started withbuilds on his analysis of KPM, but ML type theories with universes came in later in the game.)

I don't have the Palmgren'sPalmgren 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.

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 all started with his analysis of KPM, but ML type theories came in later.)

I don't have the Palmgren's paper you refer to, but I think the following paper is closely related:

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 Extending Martin-Löf type theory by one Mahlo-universe and further investigated by Rathjen in Realizing Mahlo set theory in type theory.

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.

Source Link
François G. Dorais
  • 44.4k
  • 6
  • 150
  • 233

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 all started with his analysis of KPM, but ML type theories came in later.)

I don't have the Palmgren's paper you refer to, but I think the following paper is closely related:

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 Extending Martin-Löf type theory by one Mahlo-universe and further investigated by Rathjen in Realizing Mahlo set theory in type theory.