Shamelessly copied [1] from tactics (go upvote him there) from the Haskell subreddit in case it's of interest to anyone here:

"Homotopy Type Theory is a recent advancement in the area of dependent types. Think Agda, Coq, Idris-style languages if you're familiar with them... otherwise think GADTs on supersteroids gone berserk.

Dependent types allow you to be extremely precise with your data types. You can talk about not just lists or lists of strings.... but also lists of strings of length n (for some natural number n). In the far future, it may be the key to getting fast-as-C performance (think removing bounds checking on arrays completely safely) and software verified correctness of a program simultaneously.

This isn't software, though. This is a math book.
There was a realization a few years ago that equality types (the ability to express x = y in the type system) gave rise to a mathematical structure called a weak ω-groupoid which was giving homotopy and category theorists a hard time. Homotopy Type Theory (HoTT) is a typed lambda calculus that makes studying these things easier. In fact, every data type corresponds to (a very boring) weak ω-groupoid.

What this allows mathematicians to do, though, is to create new interesting data types corresponding to more interesting examples of these things. You get a data type for a Circle, or a Sphere, or a Torus. You can define functions between them via recursion the same way you'd define a function on lists or trees. These new fancy data types are called higher inductive types, and while they don't (currently) have any use for programmers, they pay the meager salaries of long beards in the ivory tower.

The other novelty of the theory might be more interesting for programmers some day (at least if you believe dependent types will save the world).

A guy named Voevodsky proposed a new axiom called the Univalence Axiom that makes HoTT a substatial alternative to the former foundations of mathematics. The Univalence Axiom formalizes a practice mathematicans had been using for a long time, (despite its technical incompatibility with ZFC). tl;dr, the Univalence Axiom says that if two data types are isomorphic then they are equal.

Eventually, this axiom may allow a programmer to do some neat things. For instance, a programmer could write two versions of a program -- a naive version and a "fast" version. (Currently, all programmers only write the "fast" version). If you want to formally prove your "fast" program doesn't suck, it's nasty. However, it might even be humanly possible to prove some correctness about the naive version. The Univalence Axiom (once given "computational semantics") may be able to let us prove things about the dumb, slow, reference implementation of a program or library, then transfer that proof of correctness to the fast one.

To give a small example for anyone familiar with a dependently-typed language, you may notice that in Coq and Agda and whatever, the first data type you learn (and one you stick with for a long time) are the unary natural numbers. That is, you have 0, and 0+1, and 0+1+1, and 0+1+1+1, etc.. We use unary numbers because they are reaaaally easy to prove stuff about. But as any programmer might guess, actually doing anything with them is suicide. The Univalence Axiom would allow us to keep on working with unary numbers for all of our proofs, but then swap them out for actual, honest-to-God 2's complement representations when it comes time to run the program.

So there's that.

Not everyone cares about software correctness, though. But if you're sold on category theory, here's a neat trick. You probably know that equality becomes a hairy, nasty thing in category theory. Two objects can be equal or isomorphic. If you move onto 2-categories, two categories can be equal, isomorphic, or equivalent! And for higher category theory, you end up with even more notions of equaltiy, isomorphism, equivalence, etc, etc.

In a univalent foundation of category theory (which appears in the later chapters of this book), we see that all of these notions of equality collapse down into just one. If two things are isomorphic, then they are, by definition, equal to each other. You no longer have to worry about that stupid squiggle over your equals signs, because univalence means that every construction must respect the structure of your data. There are no leaky abstractions in your data types!"

[1] http://www.reddit.com/r/haskell/comments/1gr3uw/the_homotopy...