A hott thesis

• 23 August 2012
• Andrej Bauer
• Type theory, News, Tutorial

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.

Comments

Vishal Lama

24 August 2012 at 10:38

Thanks! Just the thing I was looking for.

Qwfwq

03 October 2012 at 22:52

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?

Andrej Bauer

03 October 2012 at 23:03

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.

Logic matters | Autrement qu'être Mathesis uni?ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA ???????? ???????

08 September 2017 at 18:22

[…] http://math.andrej.com/2012/08/23/a-hott-thesis/ […]