What are some examples of types that can't be derived set theoretically?
There are several type-theoretic constructions that cannot be easily handled with set theory. Note that when we say "set theory" we mean that we intend to interpret types as sets and type-theoretic functions as set-theoretic functions. In particular, the set-theoretic interpretation of types requires that a function type A → B must be interpreted as the set of all set-theoretic functions from A to B.

If our type theory has general recursion then it cannot be interpreted set-theoretically. General recursion allows us to define, for any type A, the fixed-point operator fix : (A → A) → A

fix f = f (fix f)


but the only sets which have such a fixed-point operator are the singletons. For example, if we take A to have two elements, then it will have a function without fixed point (the one that swaps the elements).

Another reason that set theory may not be sufficient is polymorphism, as you indicated. Here the reasons are perhaps a bit technical and it is best to read the famous paper Polymorphism is not set-theoretic by John Reynolds. Beware: reasoning about how one might get away with a polymorphic identity function is not proof that set theory models polymorphism. In any case, your suggestion to use universes is not going to work for System F. You can have an identity function that works for one universe, but to make it work for all universes you will have to make it universe-polymorphic, and so you're back to square one.

A third reason that a type theory may not be set-theoretic is that it allows constructions of types that do not exist in set theory. For example, in many programming languages we can define recursive types (Haskell and ML are like this) such as

type t = bool + (t -&gt; t)


The set-theoretic counterpart of this is a set T such that
$$T \cong 2 + T^T$$
but such a set $T$ does not exist, because the cardinality of $2 + T^T$ is strcictly larger than the cardinality of $T$.

A fourth reason that a type theory may not be set-theoretic is that it may contain constructs that prevent this. For example, we could have a type theory with a timeout construct which works as follows: timeout k x e computes e for at most k steps (where "step" need to be suitably defined). If e finishes with result y within k steps then the overall result is y, otherwise the overall result is the "fallback" value x. From a programming point of view, this is a reasonable construct that can actually be implemented. However, as soon as we have timeout we can write down functions that do not exist in set theory. One such function is the modulus of continuity which witnesses the fact that "all functions are continuous". In set theory there are many discontinuous functions.

Lastly, if we take "spartan" type theory without any special features (no general recursion, no polymorphism, no recursive types, etc.) then it is set theoretic. You need to extend type theory in some fashion to break the set-theoretic interpretation.