My background in mathematical logic is as follows: I've taken a model theory class, which dealt exclusively with first-order logic, and I'm also familiar with simply typed lambda calculus from using it in an applied context. I've read a bit of the HoTT book, but I don't as yet understand it particularly well.
I'm interested in understanding mathematical logic better, in particular with regards to metalogic and foundations. However, what I don't really understand is: how are logical systems compared to one another? For instance, if you take something like FOL, it's just a framework—it doesn't include an axioms on its own. Something like HoTT, on the other hand, is both an underlying logic and an axiom system for mathematics. And simply typed lambda calculus seems like a system for formalizing algorithms, rather than one for making and proving mathematical statements (I know that there exists a correspondence between algorithms and proofs, although I'm not sure how it works, which is somewhat related to the question I'm asking here). These three systems seem so different in aims and function that it is not evident to me how they can be compared to one another. Yet I often hear claims that some theorem of metamathematics applies very widely, to all possible foundations. And I furthermore hear different logics compared in terms of their expressive power, and so on. And my question is thus: how is all this made rigorous? How can all these different logical systems be understood as "the same type of thing", such that they can be compared to one another and theorems can be applied to all of them at once and so on?