Abstract: This will be a two-part presentation on character formulas for representations of compact Lie groups. In the first part, Matthias Franz will present Weyl's formula. In the second part, Sean Fitzpatrick will present Kirillov's formula.

Abstract: The theory of types was introduced by Bertrand Russell as a foundation for mathematics that avoids Russell's paradox. A more refined theory was introduced by Martin-Löf in 1972, and this theory is the basis for much modern research on type theory. It was later realized that type theory also has an intrinsically homotopical interpretation, and describing this will be the long term goal of the seminar series.

In this talk, I will give an introduction to (non-homotopical) type theory, explaining how types can be thought of either as sets or as propositions, and give examples of how to do mathematics using type theory. I will also show how type theory is used in the proof assistant Coq, which has been used to formalize many non-trivial results. I will also discuss the intuitionistic logic that arises in type theory.