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*.