Abstract. We define a type theory MLM, which has proof theoretical strength slightly greater then Rathjens theory KPM. This is achieved by replacing the universe in Martin-Lfs Type Theory by a new universe V having the property that for every function f, mapping families of sets in V to families of sets in V, there exists a universe inside V closed under f. We show that the proof theoretical strength of MLM is . This is slightly greater than , and shows that V can be considered to be a Mahlo-universe. Together with [Se96a] it follows .