What type theory?

Goal. I would like to tell you a bit about my favorite theorems, ideas or concepts in mathematics and why I like them so much. This time. What type theory? Or: HoTT = Ho TT. Disclaimer. Nobody is perfect, and I might have said something silly. If there is any doubt, then please check the references. Slides. TeX files for the presentation. Thumbnail. Main discussion. ://