  We observe here that Myhill’s constructive set theory had distinguished notions of function, natural number and set; it thus closely represented a constructive tradition in which functions and natural numbers are conceptually independent from sets. Another fundamental step in the development of constructive set theory was Friedman’s “Set-theoretical foundations for constructive analysis” (Friedman 1977). Here, among other systems, a system called B is defined which has further restrictions on the set-theoretic principles compared with Myhill’s (in particular, it has no set induction). It also has a restricted form of the axiom of dependent choice. System B is there shown to be expressive enough to represent the constructive analysis of Bishop (1967) whilst being at the same time proof-theoretically very weak (due to the absence of set induction). System B is in fact a conservative extension of arithmetic (thus it is well below the limit of predicativity given the natural numbers briefly recalled in section  1.3).  Myhill and Friedman’s systems were subsequently modified by Aczel, to obtain a system, CZF (Constructive Zermelo-Fraenkel), that is fully compatible with the ZF language (Aczel 1978, 1982, 1986; Aczel and Rathjen 2001; 2010). CZF also included no choice principles. Aczel gave an interpretation of CZF in Martin-Löf type theory with the aim of corroborating the constructive nature of the set theory. He also strengthened some of the principles of Myhill’s system (namely, collection and exponentiation) on the ground that the stronger versions are still validated by the interpretation in type theory.