Mathematics and Computation

A blog about mathematics for computers

A hott thesis

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.

How to comment on this blog: At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention, I will gladly respond. You are also welcome to contact me directly.