A categorical structure of realizers for the Minimalist Foundation

We provide a categorical presentation of a realizability interpretation a ̀ la Kleene for the Minimalist Foundation. This interpretation is predicative since it is made in Feferman’s predicative theory of inductive definitions ÎD1. Our final aim is to provide a candidate for a predicative version of Hyland’s effective topos [1]. The Minimalist Foundation (for short MF) is a predicative foundation for constructive mathematics. It was ideated by M. E. Maietti and G. Sambin in [7] and then completed in [3] by M. E. Maietti. It is called minimalist since it is intended to constitute a common core among the most relevant constructive and classical foundations, introduced both in type theory, in category theory and in axiomatic set theory. One of its novelties is that it consists of two levels: an intensional level (mTT) which should be a (type) theory with enough decidable properties to be a base for a proof-assistant and for extraction of computational contents from its proofs, and an extensional level (emTT) formulated in a language as close as possibl