Comment by sa1

I think they do, and as you mentioned you can explicitly remove such a restriction. Sets and types are once again two different kinds of objects in mathematical theory, and a set-theoretic type doesn’t seem to be based either on set theory or type theory.