Constructive Mathematics in Univalent Type Theory

Explore the foundations of constructive mathematics within the context of univalent type theory in this illuminating lecture delivered by Martin Hötzel Escardó. Delve into the intricate relationship between types, sets, and constructions as part of the Hausdorff Trimester Program. Over the course of one hour, gain insights into the fundamental principles and applications of this mathematical approach, laying the groundwork for a deeper understanding of modern mathematical foundations and their implications in computer science and logic.

Martin Hötzel Escardó: Constructive Mathematics in Univalent Type Theory (Lecture I)