  One such extension of Church’s simple type theory is obtained by adding universes (Martin-Löf 1970). Adding a universe is a reflection process: we add a type \(U\) whose objects are the types considered so far. For Church’s simple type theory we will have