 The formalization of intuitionistic mathematics covers more than arithmetic. Large parts of analysis have been axiomatized from a constructive point of view (Kleene 1965, Troelstra 1973). The constructivity of these systems can be established using functional, type theoretic, or realizability interpretations, most of them based on or extensions of Gödel’s Dialectica interpretation (Gödel 1958, Kreisel 1959), Kleene realizability (Kleene 1965), or type theories (Martin-Löf 1984). In these interpretations the functionals underlying constructive statements, such as for example the function assigning a \(y\) to every \(x\) in \(\forall x\exists y A(x,y)\), are made explicit in various ways.