The extended predicative Mahlo universe in Martin-Löf type theory
scientific article; zbMATH DE number 7942586