Abstract: Continuing from last week's lecture, I will discuss some of the functorial properties of the index of transversally elliptic operators, and give some basic examples.

Abstract: HOTT is a new branch of mathematics arising from the unexpected encounter of logic with homotopy theory. It provides a new foundation of mathematics which can be implemented in a computerised proof assistant like Coq or Agda. I will briefly describe the history of the subject, from Martin-Löf, to Awodey, Warren and Voevodsky. I will describe HOTT in the language of category theory and discuss the geometric meaning of Voevodsky's univalence axiom.