### 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: http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2738

### 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.

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

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

### 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 ﬁeld 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.

### 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.

### 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?

## 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.