Linear homotopy type theory: its origins and potential uses

Linear homotopy type theory has arisen out of the Sati-Schreiber program in theoretic physics, which seeks to formulate M-theory, the hypothetical theory of which 11-dimensional supergravity and the five string theories are all special limiting cases. But there are plenty of points of considerable interest arising from it for researchers working in other fields: mathematics, quantum computing, data analysis, and even philosophy. Indeed, linear HoTT has implications for the philosophy of quantum mechanics, by providing a logical calculus which unites the Everettian many-worlds interpretation with the Copenhagen interpretation.

In this talk, I shall be offering personal reflections on why people might be interested in this new type theory.