Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

April 29, 2014

Homotopy Type Theory: Unified Foundations of Mathematics and Computation

Posted by David Corfield

Congratulations to Mike for being a part of a research team who will receive $7. 5 million to carry on the good work of the IAS Univalent Foundations program. Homotopy Type Theory: Unified Foundations of Mathematics and Computation will run for five years, organised by Steve Awodey at CMU. (Technical portion of the grant proposal is here.)

I hope they’re allowed to use some of that funding to spill into physics a little.

Posted at April 29, 2014 12:48 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2738



8 Comments & 0 Trackbacks

Re: Homotopy Type Theory: Unified Foundations of Mathematics and Computation

thanks for the press – but that general, college press release is not exactly intended for this, more informed, readership. We’ll make some sort of official announcement soon. For now, let me just say that my name may be listed as the lead PI, but this is definitely a group effort.

Posted by: Steve Awodey on April 29, 2014 2:54 PM | Permalink | Reply to this

Re: Homotopy Type Theory: Unified Foundations of Mathematics and Computation

Coincidently, the announcement came just as I’m putting the finishing touches on my own (tiny by comparison) grant application for a homotopy type theory inspired project, so hopefully a good omen.

Posted by: David Corfield on April 29, 2014 3:09 PM | Permalink | Reply to this

Re: Homotopy Type Theory: Unified Foundations of Mathematics and Computation

Congratulations, Steve, Mike and all! That’s an amazing achievement.

Posted by: Tom Leinster on April 30, 2014 8:31 AM | Permalink | Reply to this

Re: Homotopy Type Theory: Unified Foundations of Mathematics and Computation

Looking through the grant proposal, I see

We propose to investigate models of homotopy type theory, and to apply these models to synthetically incorporate many other kinds of mathematics. A notable example is synthetic differential geometry and differential cohomology, which can provide a formal context for quantum gauge field theory.

So that answers my hope expressed in the post.

By the way, interesting things about differential cohomology are being record by Urs at the nLab at the moment, e.g., see differential cohomology diagram.

Posted by: David Corfield on April 30, 2014 10:35 AM | Permalink | Reply to this

Re: Homotopy Type Theory: Unified Foundations of Mathematics and Computation

Yes, congratulations! This is wonderful news.

It would be great to see the MURI launch with an introductory workshop aimed at graduate students and non-experts in related fields — to expand the pool of researchers working on this project and to enable interested bystanders to describe it more knowledgeably to colleagues.

Posted by: Emily Riehl on April 30, 2014 8:13 PM | Permalink | Reply to this

Re: Homotopy Type Theory: Unified Foundations of Mathematics and Computation

We do have plans for workshops/conferences, but nothing detailed yet.

Posted by: Mike Shulman on May 1, 2014 6:22 AM | Permalink | Reply to this

Re: Homotopy Type Theory: Unified Foundations of Mathematics and Computation

Could HOTT be also useful for physics? Category theory is the theory of structures/relations, therefore it should clearly be useful to (re)formulate physics in this framework. Could HOTT be a deeper framework in this respect, and why?

If yes, does HOTT admits a formalization with linear logic?

Posted by: okefoz on May 7, 2014 1:29 PM | Permalink | Reply to this

Re: Homotopy Type Theory: Unified Foundations of Mathematics and Computation

Posted by: David Corfield on May 7, 2014 5:05 PM | Permalink | Reply to this

Post a New Comment