nLab
type

In modern logic, we understand that every variable should have a type, or domain of discourse. Untyped logic may be seen as simply a special case, in which there is only a single unique type. (Thus, untyped logic has one type, not no type.)

It is possible to build foundations of mathematics on type theory alone.