In the last year, I have written my master thesis on homotopy type theory under supervision of Andrej Bauer in Ljubljana, to whom I went on an exchange, and Jaap van Oosten and Benno van den Berg in Utrecht. Their reactions, and Steve’s, have encouraged me to share it here on the HoTT blog. So here it is:
hott.pdf (revised version)
In this blog post I give a brief outline of the things I included in my thesis:
- Since I had no knowledge of type theory before I started on this project, and none of my fellow students have it neither, I have written my thesis as an introduction and a short chapter on pre-homotopy type theory is also included.
- In chapter 2 the theory of identity types is presented, with most of the material of the Coq repositories included. Some noteworthy things from this chapter are: theorems which state the equivalence of the spaces of “data needed to construct a section of P” and of sections of P for each dependent type over an inductively defined type (the uniqueness up to equivalence of an inductively defined space is derived from such theorems), two applications of the Univalence axiom and the type theoretical Yoneda Lemma, about which I have posted before. Another thing is that I have tried to write fluently about homotopy type theory.
- In chapter 3 higher inductive types are introduced. After the definition of a hit, there is again a theorem which states the equivalence of the spaces “data needed to construct a section of P” and of sections of P, so these carry over to the higher inductive types. Once there is a general way of saying what the higher inductive types are, it should be possible to deduce such a theorem in more generality. In this chapter there are also the proofs that the fundamental groupoid of the circle is the integers (see Shulman’s post) and that the omega-sphere is contractible (Brunerie).