A survey article that we have written:
Urs Schreiber, Michael Shulman,
Quantum Gauge Field Theory in Cohesive Homotopy Type Theory
in
Ross Duncan, Prakash Panangaden (eds.)
Proceedings 9th Workshop on Quantum Physics and Logic, Brussels, Belgium, 10-12 October 2012
on the synthetic axiomatization of classical field theory/prequantum field theory within homotopy type theory in a flavor with three higher modalities added: cohesive homotopy type theory.
The formalization of cohesive homotopy type theory discussed in the article has been implemented in the Coq proof management system by Mike Shulman, the source code is here: Coq source code.
Related material for further reading includes:
A discussion with more emphasis on the differential cohomology hexagon which is axiomatized by cohesive homotopy type theory is in Differential generalized cohomology in Cohesive homotopy type theory.
More discussion of genuine synthetic quantum field theory, is at Quantization via Linear homotopy types.
For a survey of the general picture see at Synthetic Quantum Field Theory.
For a more detailed exposition of the physics involved see the pdf-document at Classical field theory via Cohesive homotopy types.
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).
Expositions of the general idea are in
Urs Schreiber, Prequantum physics in a cohesive topos, Talk at Quantum Physics and Logic 2011, (pdf)
Lecture notes on more aspects of physics with an eye towards string theory in the context of cohesive homotopy type theory is in
For further related references see at differential cohomology in a cohesive topos – References.
differential cohomology in a cohesive topos
Synthetic Quantum Field Theory
Quantum gauge field theory in Cohesive homotopy type theory
Last revised on February 23, 2015 at 17:53:34. See the history of this page for a list of all contributions to it.