CMSA New Technologies in Mathematics: Homotopy type theory and the quest for extensionality
Michael Shulman - Dept. of Mathematics, University of San Diego
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.