Schreiber Quantum gauge field theory in Cohesive homotopy type theory


A survey article that we have written:

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:



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

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.

Last revised on November 18, 2021 at 07:20:12. See the history of this page for a list of all contributions to it.