 Church’s simple type theory usually starts with base types “i” (individuals/entities) and “o” (Booleans) only and then iteratively defines all function types (such as “\(\text{i} = &gt; \text{o}\)”,  “\(\text{i}=&gt;\text{i}\)”, “\(\text{o}=&gt;\text{o}\)”, “\(\text{i}=&gt;(\text{i}=&gt;\text{o})\)”, etc.) starting from those. But in fact one can have arbitrary many base types \(i_1\), \(i_2\), \(i_3\),…, \(i_n\) and apply an analogous construction. These base types \(i_1\), \(i_2\), \(i_3\),…, \(i_n\) can be considered as sorts.