Intuitionistic type theory can be viewed in a similar way, only here the possibilities for introducing domains of quantification are richer, one can use \(\Sigma, \Pi, +, \I\) to construct new ones from old. (Section 3.1; Martin-Löf 1998 [1972]). Intuitionistic type theory has a straightforward set-theoretic interpretation as well, where \(\Sigma\), \(\Pi\) etc are interpreted as the corresponding set-theoretic constructions; see below. We can add to intuitionistic type theory unspecified individual domains just as in HOL. These are interpreted as sets as for HOL. Now we exhibit a difference from HOL: in intuitionistic type theory we can introduce unspecified family symbols. We can introduce \(T\) as a family of types over the individual domain \(S\):