Universes in the Theory of Types and Names. - Markus Marzetta (CSL, 1992)

The m mu quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals. - Markus Marzetta; Thomas Strahm (Arch. Math. Log., 1998)