I know the title is sort of misleading because we do have set-theoretic types in several languages:) From a theoretic view, set-theoretic types such as intersection, union, and negation may bring some troubles, as the proof object they do not encode the derivation, thus making it hard to find a logical part through the C-H correspondence, moreover, negation is not able to be encoded at all because the normal semantic of complement in set theory contradicts the rejection of the non-existing of the double negation elimination in the intuitionistic logic (Question: is this viewpoint correct? that the set-theoretic approach contrast fundamentally with the central of the BHK interpretation of the intuitionistic logic). But from a practical view, it seems that there aren't so many obstacles, and we don't face that many problems we need to be concerned about in the theory: we are doing neither proof verifications nor automated reasoning, so my problems are:
- Why set-theoretic types are relatively rare in the languages?
- Can we define the negation type
a: not Aif
ais not of type
A(if we only consider the practical part of this problem)?
- Is subtyping also a set-theoretic definition? Since the subtyping also does not record the derivation, if this is true, then is subtyping some meta-theoretic level notation, and we need to put intersection/union/negation types at the same level as the subtyping relation.
Postscriptum: I've read MLTT and some topology & category theory, not yet started reading the HoTT Book (I want to do this after I've read algebraic topology and some higher category theory, though I might be aware of the fact that the HoTT book does not require so many preliminaries)