HOMOTOPY TYPE THEORY SEMINAR

Organiser: Kobi Kremnizer

Currently, mathematics is formally based on set theory. Set mathematics is suitable for studying properties invariant under isomorphisms of structured sets. Category theory and Homotopy theory study properties invariant under equivalences. Set theory is an inconvenient language for dealing with the notion of equivalence. In recent years, it was discovered that intensional dependent type theory (Martin-Löf type theory) is a language which is very suitable for formalizing homotopy theory and higher category theory. The main researchers involved in this are Vladimir Voevodsky and Steve Awodey. Martin-Löf developed his version of type theory as a foundation for constructive mathematics. It is also the basis of interactive theorem provers such as Coq. The aim of this seminar is to study the various aspects of intensional type theory: structure, homotopical and higher categorical semantics, uses as foundation for mathematics and more. It should be of interest to mathematicians, computer scientists and philosophers.

Introduction to homotopy type theory
Homotopy types
Homotopy theories and model categories
Infinity groupoids and homotopy types
Topos theory and categorical semantics
Strict n-categories, operads and Trimble's definition of n-category