Category theory, type theory, and homotopy type theory

Category theory may have "type-theoretical flavour", in the sense that category theory deals with objects of different categories and analyses functions (functors) between categories. However, category theory is not a foundational framework and by itself does not aspire to play the role of an alternative foundation for mathematics.

Type theory may aspire to be an alternative foundation. While it seemed to be (almost) forgotten after its introduction by Russell and Whitehead, its connection to computers brought it back to life. The idea of "constructive computation" may be suitably formulated in type-theory (as a logical framework), with the intuitionistic position  - and since a computer program is by definition "constructive", this framework has had its proponents.

Recently, there has been some effort to connect and merge type theory as a logical framework with mathematical ideas of category theory, especially homotopy theory. This synthesis is called Homotopy Type Theory, and has beem sometimes proposed as an alternative (constructivist) framework for whole mathematics.

Read the links below (preferably in the order given) to get some idea regarding these notions.

In addition, you can read a paper by Philip Wadler, "Propositions as Types", which explains the connection between type theory and logical syntax.