In this talk, I introduce a type-theoretic framework that allows us to formalise various branches of mathematics based on different logical foundations ("mathematical pluralism").

The framework considers logic-enriched type theories, in the sense of Aczel and Gambino, in a logical framework and gives a uniform type-theoretic foundation for formalisation of mathematics. As an example, we show how the first-order classical logic and a notion of predicative set can be considered in the framework for formalisation of Weyl's predicative mathematics.