Professor Harper's own book (free! while in draft form), http://www.cs.cmu.edu/~rwh/plbook/book.pdf , is a better source for understanding the material in this post.

But, to be perfectly honest, I'm a systems-focused PL graduate student and have spent quite a bit of time studying this stuff and doubt that I could easily produce a more accessible version of this post. I tried (in the comments block here) and ran on to about two pages before realizing I had only covered the back story on his "trinity" analogy without even getting to this post itself. Someone far smarter than I probably could, but don't feel disappointed if you found this post mathematically challenging even if you normally follow PL theory. It took me a solid cup of coffee and a half an hour to deeply understand what he was saying.

Pierce's TAPL primarily covers the type side of this "trinity" and TAPL2 really only has one relevant chapter, covering Dependent Types.

Neither of which deal directly with Homotopy Type theory AFAIK.