Speaker: Michael Shulman – Dept. of Mathematics, University of San Diego

Title: Homotopy type theory and the quest for extensionality

Abstract: Over the past decades, dependent type theory has proven to be a powerful framework for verified software and formalized mathematics.  However, its treatment of equality has always been somewhat uncomfortable.  Recently, homotopy type theory has made progress towards a more useful notion of equality, which natively implements both isomorphism-invariance in mathematics and representation-independence in programming. This progress is based on ideas from abstract homotopy theory and higher category theory, and with the development of cubical type theories it can be implemented as a true programming language.  In this talk, I will survey these developments and their potential applications, and suggest some directions for further improvement.