Egbert Rijke successfully defended his master thesis in Utrecht a couple of weeks ago. He published it on the *Homotopy type theory* blog (here is a direct link to the PDF file (revised)). The thesis is well written and it contains several new results, but most importantly, it is a gentle yet non-trivial introduction to homotopy type theory. If you are interested in the topic but do not know where to start, Egbert’s thesis might be perfect for you. As far as I know it is the first substantial piece of text written *in* (informal) homotopy type theory.

What I find most amazing about the work is that Egbert does not have to pretend to be a homotopy type theorist, like us old folks. His first contact with type theory *was* homotopy type theory, which impressed on his mind a new kind of geometric intuition about $\Pi$’s, $\Sigma$’s and $\mathrm{Id}$’s. If we perform enough such experiments on young bright students, strange things will happen.

Thanks! Just the thing I was looking for.

Not knowing anything about this topic, I was asking myself if “homotopy type theory” stands for “homotopy-type theory” (the theory of homotopy types) or “homotopy type-theory” (a homotopical version of Russel and whitehead’s Type Theory)? …Or perhaps both?

It is an interpretation of type theory in which types are understood as homotopy types, i.e., objects of a Quillen model category. Thus we can use type theory to prove theorems in homotopy theory, and we can use homotopy theory to discover things about type theory.