University Seminar: Logic Across Disciplines-   Homotopy Type Theory, the confluence of logic and space

Abstract:  In this talk we will learn how to express ourselves in the language of Homotopy Type Theory and see how it is represents the natural merging of logic and space. We will take some time to consider how identity types, and in particular univalence, free us from certain artificial restrictions of classical logic(s) and foundational systems and give rise to a rich and pleasing theory. Time permitting, we will discuss the role of Univalent Foundations and how Homotopy Type Theory in particular may be leveraged as a foundational system to the direct advantage of the working mathematician.