We've mostly learned that ZFC set theory can be used as the foundation of mathematics. I remember having seen that there are 5 or 6 equivalent frameworks that can provide the same theoretical foundation. It appears to me that Russell's Type theory and HoTT might be among them, but I haven't been able to locate the others.
Do you happen to know of a book that presents the various systems and explains the differences between them?
With regard to your remark "I haven't been able to locate the others":
An equivalent logical foundation for mathematics is provided by Internal Set Theory (IST). This is discussed in detail in the monograph
IST is only one of the systems considered in that book; see there for variants such as BST, RIST, HST, etc.