CMSA New Technologies in Mathematics: Homotopy type theory and the quest for extensionality


View Calendar
April 21, 2021 3:00 pm - 4:00 pm
via Zoom Video Conferencing

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.