 Formalizations that are meant to serve as a foundation for constructive mathematics are either of a set-theoretic (Aczel 1978, Myhill 1975) or type-theoretic (Martin-Löf 1984) nature. The former theories are adaptations of Zermelo-Fraenkel set theory to a constructive setting, while in type theory the constructions implicit in constructive statements are made explicit in the system. Set theory could be viewed as an extensional foundation of mathematics whereas type theory is in general an intensional one. 