A survey article that we have written:
Urs Schreiber, Michael Shulman,
Quantum Gauge Field Theory in Cohesive Homotopy Type Theory
to appear in: Proceedings of QPL 2012
(pdf)
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.
There is also a refinement to genuine synthetic quantum field theory, see at Motivic quantization of local prequantum field theory and at Type-semantics for quantization
For a survey of the general picture see at Synthetic Quantum Field Theory.
For a more detailed exposition see 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