 An intuitionistic typed theory of sets is readily obtained by simply adopting the intuitionistic versions of the axioms of TST as axioms. An Axiom of Infinity would be wanted to ensure that an interpretation of Heyting arithmetic could be embedded in the theory; it might be simplest to provide type 0 with the primitives of Heyting arithmetic (just as the earliest versions of TST had the primitives of classical arithmetic provided for type 0). We believe that this would give a quite comfortable environment for doing constructive mathematics.