Homotopy type theory

Abstract

The thesis introduces homotopy type theory, which refers to a new interpretation of Martin-Löf type theory. All the main recent results, such as strong function extensionality from weak, weak extensionality from univalence, and the notion of higher inductive types including the proof that the fundamental group of the circle is the integers using univalence, are included. Along with those results, there are new results such as a type theoretical yoneda lemma and various correspondence theorems for inductively defined types including higher inductive types.

My other supervisors are Andrej Bauer (University of Ljubljana) and Benno van den Berg (Utrecht)