Awodey and Voevodsky hit on connections between type theory and homotopy theory about the same time. It isn't clear how to find normal forms for dependent type theory with the univalence axiom added. Mathematicians of my acquaintance find curious the attraction of what appears to be another constructive type theory of interest primarily to (functional) programmers. To them it looks like a calculus for doing synthetic homotopy theory.
