Arnold Grigoryan made a presentation entitled "Univalent Foundations and Constructive Type Theory"

On the 4th of October Arnold Grigoryan (NRU HSE) gave a talk on the topic of "Univalent Foundations and Constructive Type Theory" at the workshop «From the Logical Point of View». 

Abstract

The Univalent Foundations program was initiated by Vladimir Voevodsky to develop a new type theory that is suitable for the formalization of mathematics. Inter alia, the result was the emergence of a homotopy interpretation of the Martin-Löf type theory, the central topic that will be covered in the presentation. The first part focuses on an introduction to type theory and its constructive interpretation. Then I will present the axiom of univalence and show its relation to the type of identity. At the end of the presentation, it is planned to discuss the problems of the univalent theory of types, as well as the logical and philosophical significance of the axiom of univalence.