The received Hilbert-style axiomatic foundations of mathematics has been designed by Hilbert and his followers as a tool for metatheoretical research. Foundations of mathematics of this type fail to satisfactory perform more basic and more practically oriented functions of theoretical foundations such as verification of mathematical constructions and proofs. Using alternative foundations of mathematics such as the univalent foundations is compatible with using the received set-theoretic foundations for metamathematical purposes provided the two foundations are mutually interpretable. Changes in foundations of mathematics do not, generally, disqualify mathematical theories based on older foundations but allow for reconstruction of these theories on new foundations. Mathematics is one but its foundations are many. © Springer Nature Switzerland AG 2024.