Until now, I heard that there are some theories for building mathematical objects (or at least it is what it seems to my poor knowledge). Some of these are:
Set theory;
Logic;
Category theory;
Type Theory;
Homotopy Type Theory;
(Perhaps) Lambda calculus;
Etc.
Until now I know that these seems to be different trials of foundations for mathematical objects, both with it's strong and weak points: I've heard - for example - that type theory allows the computional implementation of mathematical objects, while set theory makes it a little harder.
I've seen some books, for example Goldblatt's Topoi: A categorical analysis of logic - It seems that some of these theories, as in this case Logic and Category theory do interact somehow. I believe that there may be more interaction between them.
I'm looking for some resource about foundational theories, their uses, interactions and comparisons.