"Set-theoretic type theory" is working with the lattice of all subsets of possible values, where a "type" is one of these subsets. This lattice has plenty of st

"Set-theoretic type theory" is working with the lattice of all subsets of possible values, where a "type" is one of these subsets. This lattice has plenty of structure, but sure individual subsets do not. The category of sets is different from this lattice, since it allows arbitrary functions between sets for its morphisms rather than just inclusions. "Set-theoretic types" have a meaningful notion of overlap. Usually types in other type system tend to be practically disjoint, like objects in a concrete category might be sets but the category itself doesn't give language to check whether the objects are disjoint sets.