Type Theory is a very foundational way of looking at logic and a very nice functional programming language. It is a strong generalization of, say, Haskell's system. Homotopy TT is a certain kind of TT that introduces a lot of structure to handle notions of equality and identity.