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.

3 thoughts on “A hott thesis

  1. 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?

  2. 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.

Leave a Reply

Your email address will not be published. Required fields are marked *

67 − 63 =

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>