JetBrains Research unites scientists working in challenging new disciplines

Seminar: Basic concepts of homotopy type theory

In this talk, we will discuss differences between homotopy and ordinary type theories. We will consider several constructions defined in HoTT (such as propositional truncation, quotient types, and the univalence axiom) and give some examples of their applications. In particular, we will consider a sorting function for lists of totally ordered elements, which shows that it is useful to define the disjunction as the join of types.

Presenter: Valery Isaev

23.09.2019, 17:15.

Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg

State University, Stary Peterhof, Universitetski pr., 28