Schreiber Quantization via Linear homotopy types


A set of notes

on the formalization of Motivic quantization of local prequantum field theory in the formal framework of dependent linear homotopy type theory, with application to the archetypical example of extended geometric quantization of 2d Chern-Simons theory.

To go along with talks I gave on the following occasions:

Related talks:

This is a companion of

Followup articles:

Related talks:



We discuss in the foundational logical framework of homotopy-type theory a natural formalization of secondary integral kernels in geometric stable homotopy theory. We observe that this yields a process of non-perturbative cohomological quantization of local prequantum field theory. We show that quantum anomaly cancellation amounts to realizing this as the boundary of a field theory that is given by genuine (primary) integral transforms. Recalling that traditional linear logic has categorical semantics in symmetric monoidal categories, such as that of Hilbert spaces, and hence serves to axiomatize quantum mechanics, e.g. Pratt (1992), Abramsky-Duncan (2005), Duncan (2006), what we consider is its refinement to linear homotopy-type theory which has categorical semantics in stable ∞-categories of bundles of stable homotopy-types, hence of generalized cohomology theories. We discuss how this provides a natural formalization of geometric quantization of local prequantum field theory, following (dcct, Nuiten (2013)) and closely related to Hopkins-Lurie (2014).

For the reader interested in technical problems of quantization we discuss how this formalization informs the discussion of quantum anomaly cancellation. For the reader inclined to the interpretation of quantum mechanics we exhibit quantum superposition and quantum interference as existential quantification in linear homotopy-type theory. For the reader inclined to ontological philosophy we provide a modal homotopy-type theory formalizing Hegelian metaphysics (Hegel (1812)) in refinement of the proposal in Lawvere (1991), Lawvere (1994) for a formal foundations of physics, Lawvere (1986), Lawvere (1997), lifted from classical mechanics to local quantum gauge field theory (Sch (2013c)).


The axiomatic characterization of local quantum field theory (QFT) on spacetimes/worldvolumes of arbitrary topology (see here for a review) had been completed in (Lurie 09) via a universal construction in monoidal higher category theory. While in the “bulk” of the worldvolume this describes topological QFT, the axiomatization also captures defects (domain walls) and boundaries (branes) and the corresponding boundary field theories may be geometric (non-topological) (dcct). Notably ordinary quantum mechanics is a boundary field theory of a 2d Poisson-Chern-Simons theory TQFT in this way (Nuiten 13, Bongers 13).

But modern quantum physics is more than quantum mechanics, and the quantum field theories of interest both in nature and in theory are not random examples of the axioms of local QFT, instead they arise via a process of “quantization” from geometric data. An axiomatic characterization also of pre-quantum data and of the quantization step has been proposed and studied in (dcct, Nuiten 13). This may be naturally formalized entirely in type theory – in its dependent and intensional flavor called homotopy type theory.

This note here gives a brief survey of the key aspects of quantization axiomatized in homotopy type theory this way.

The process is naturally divided into two stages: first, pre-quantum geometry (phase spaces and local Lagrangians) is naturally axiomatized in cohesive homotopy type theory (ScSh 12); second, quantization (geometric quantization and path integral quantization, in fact we find a subtle mix of both) is naturally axiomatized in linear homotopy type theory. The first step has been discussed in detail in (dcct, ScSh 12), see Classical field theory via Cohesive homotopy types for a quick exposition. The second step is worked out in various key examples in (Nuiten 13). There however the type-theoretic formalization is not discussed. The present note essentially points out how the quantization process in section 4 of (Nuiten 13) has a natural abstract formalization in linear homotopy type theory.

While we produced this note the preprint

appeared, which in its section 4.1 considers a special case of the abstract integral kernels of section 4.3 in the above note (namely the case of vanishing twist and realized in the model of local systems of stable homotopy types). This development seems to be motivated from serving as a building block in making precise the quantization prescription inducated in sections 3 and 8 of

Last revised on March 20, 2023 at 07:45:33. See the history of this page for a list of all contributions to it.