 Type theories are still in use, mostly in theoretical computer science, but these are type theories of functions, with complexity similar to or greater than the complexity of the system of PM, and fortunately outside the scope of this study.