Russel and Whitehead's type system never gained significant traction. It's primarily of historical interest. Once mathematicians became convinced that ZF set th

Russel and Whitehead's type system never gained significant traction. It's primarily of historical interest. Once mathematicians became convinced that ZF set theory over first order logic was plausibly consistent and expressive enough, such foundational issues became less important to the typical mathematician. Lately there's been a resurgence in foundations because of what new foundations like Homotopy Type Theory bring to the table. Funny how something as basic as equality can be revisited time and time again for thousands of years!