This talk will summarize a type-theoretic foundation for mathematics presented in a recently posted arxiv manuscript. In this system each type is associated with an equality relation in correspondence with the standard notions of isomorphism in mathematics. The main result is an abstraction theorem stating that isomorphic objects are inter-substitutable in well-typed contexts.

If you are interested in meeting with David, please contact Dexter Kozen (kozen@cs.cornell.edu).