Quantum Gauge Field Theory in Cohesive Homotopy Type Theory
Posted by Urs Schreiber
Readers of this blog know that Mike Shulman and myself have had extensive discussion, over many months, about cohesive homotopy type theory. Mike has connected this to his other work on homotopy type theory as explained in his post Internalizing the External, or The Joys of Codiscreteness, and I have been trying to see how much of quantum gauge field theory can be formalized in this axiomatics, discussed for instance in the post Prequantization in cohohesive homotopy type theory.
Now, the call for submissions to
QPL 2012
Quantum Physics and Logic
10-12 October 2012, Brussels, Belgium
(website)
made us think that this may be a good occasion to finally write up something together, even if it is just an “extended abstract”. This we have done now:
Urs Schreiber and Michael Shulman, Quantum gauge field theory in Cohesive homotopy type theory (pdf, 12 pages)
Abstract. We implement in the formal language of homotopy type theory a new set of axioms called cohesion. Then we indicate how the resulting cohesive homotopy type theory naturally serves as a formal foundation for central concepts in gauge quantum field theory. This is a brief survey of work by the authors developed in detail elsewhere (Sh, Sc).
Maybe you’d enjoy having a look and dropping us a comment. It’s a brief survey (given the size constraints demanded for submissions of this form) of a collection of central constructions and their relations, which hopefully serves to indicate how the two seemingly disparate subjects of the title are in fact closely related.
Last year at QPL 2011 I had given an invited talk also within this general subject, the slides are still available at Prequantum Physics in a Cohesive ∞-Topos and might serve as further introduction to what I am discussing with Mike here.