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

CMSA EVENTS

Speaker:

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.

Zoom: https://harvard.zoom.us/j/99018808011?pwd=SjRlbWFwVms5YVcwWURVN3R3S2tCUT09