Foundational theories, their uses, interactions and comparisons? 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. 
 A: This is more like a long comment. The only two major approaches to the foundations that you list are type theory and set theory. Let me explain.
First, make note of a naming convention:


*

*the axioms of group theory tell us what it looks like inside a group

*the axioms of category theory us what it looks like inside a category


etc.
Following this convention, you might think that set theories tell us what it looks like "inside" a set. But they don't (life is awfully boring inside a mere set!). Rather, they tell us something about what the universe of sets looks like. A similar statement can be made in regards to type theory; type theories describe universes of types.
Another important observation is the following. Using [insert your favourite set theory here], we can prove statements about the natural numbers. For example, $\mathrm{ZFC}$ proves that a variety of other formal systems are consistent; or in other words, that there does not exist a natural number $n$ such that so-and-so formal system proves a contradiction in $n$ or fewer steps. Type theories like Martin Lof type theory also have this ability.
On the other hand, neither the group theory axioms nor the category theory axioms tell us very much about the natural numbers. They just have no "foundational power." So I guess I would say that category theory is "ubiquitous" without really being "foundational." Don't be misguided; set theory and category theory solve very different problems. Set theories (and type theories) attempt to discern truth from falsehood, whereas category theory is a conceptual tool; the point is to conceptualize mathematics in a unified way. There's essentially no conflict between the two.
For these reasons and others, the only two major approaches to the foundations that you list are type theory and set theory. (That's not an exhaustive list; another example would be Lawvere's axiomatization of the "category of all categories.") I hope this comment has clarified a few things.
