Type theory is a sort of axiomatisation of mathematical structures that is similar to (but not identical to: http://dl.acm.org/citation.cfm?id=512927.512938) set theory. As chas mentions (https://news.ycombinator.com/item?id=8780786), a lot of the modern mathematical perspective on type theory is via homotopy type theory.

Category theory is another such axiomatisation.

As with any pair of sufficiently powerful axiomatisations, any one of them can be formalised in any other of them, more or less naturally; for example, here's an n-category café hit when I Googled "category theory + type theory": https://golem.ph.utexas.edu/category/2013/03/category_theory....