Gerhard Jaeger Universes in explicit mathematics In one form or the other, universes play an important role in many (sub)systems of set theory and analysis and in various formalizations of constructive mathematics. One aspect of universes is that they expand the set or type formation principles in a very natural and perspicuous way and provide great proof-theoretic strength. These two talks will be centered around universes in Feferman's explicit mathematics. We begin with introducing some minimal requirements for universes, compare these to related approaches in other areas of proof theory and discuss several crucial ontological aspects of universes. Later we will make use of universes for calibrating theories of explicit mathematics going in strength beyond the famous theory $T_0$. By omitting the principle of inductive generation we obtain, in addition, natural metapredicative systems of explicit mathematics. Furthermore, the notion of Mahloness in explicit mathematics - in its metapredicative and impredicative form - will be presented. If time is left, then we also want to indicate how to proceed to even stronger theories.