differential geometry in modal HoTT

[Urs Schreiber <urs.sc...@googlemail.com>]

Felix Wellen just handed in a PhD thesis that some readers here might
find of interest, on the formalization of higher synthetic
differential geometry in HoTT:

Felix Wellen,
"Formalizing Cartan Geometry in Modal Homotopy Type Theory"
PhD Thesis, KIT 2017

thesis pdf:   http://www.math.kit.edu/iag3/~wellen/media/diss.pdf,
talk slides:  https://ncatlab.org/schreiber/files/wellenDGinHoTT.pdf
HoTT-Agda code:  https://github.com/felixwellen/DCHoTT-Agda
background links:  https://ncatlab.org/schreiber/print/thesis+Wellen


The thesis implements a fragment of the axioms of differential
cohesion for synthetic differential geometry, formalized in homotopy
type theory and implemented in the Agda. Specifically, a modal
operator is introduced which is interpreted as an “infinitesimal
shape” modality ℑ. For X a homotopy type the standard interpretation
of the type ℑX is the result of “identifying infinitesimally close
points in X”.

(By synthetic PDE theory the dependent types over ℑX have the
interpretation of being partial differential equations with free
variables ranging in X. The linear depenent types over ℑX are also
known as D-modules, as used in geometric representation theory.)

Using this infinitesimal shape modality ℑ the thesis presents a
formalization of the concept of manifold in the type theory. Via the
homotopy theoretic interpretation of the type theory the
interpretation of such “manifold types” is really as étale ∞-stacks X.

The main theorem shows that the infinitesimal disk bundle of any such
manifold X is a fiber ∞-bundle which is associated to an principal
∞-bundle: its frame bundle.

Classically, the concept of frame bundle is the foundation of all
genuine geometry, via Cartan geometry: Equipping the frame bundle of a
manifold X with torsion-free G-structure means to equip X with a
flavor of geometry, depending on the choice of G, such as,
(pseudo-)Riemannian geometry, conformal geometry, complex geometry,
symplectic geometry etc. pp. The moduli stacks of all given
G-structures on a given manifold are of central interest in the
classical theory, such as the moduli stacks of complex structures, or
the moduli stacks of conformal structures.

In order to lift classical Cartan geometry from classical manifolds to
higher Cartan geometry on étale ∞-stacks, the thesis closes by
formalizing the concept of torsion-free G-structure on manifold types.
Due to the homotopy-theoretic interpretation this is really a
formalization of higher (∞-group) G-structures on étale ∞-stacks,
including also examples such as string structures or Fivebrane
structures. Finally the thesis demonstrates the construction of the
(higher) moduli stacks of such torsion-free G-structures

This solves the first of the three problems in modal type theory that
had been posed in

U.S.: "Some thoughts on the future of modal homotopy type theory",
talk at Homotopy Type Theory and Univalent Foundations - Mini-Symposium,
within the German Mathematical Society meeting Sept 2015, Hamburg
https://ncatlab.org/schreiber/files/SchreiberDMV2015b.pdf

For more exposition see also here:
https://ncatlab.org/schreiber/print/Formalizing+Cartan+Geometry+in+Modal+HoTT


Best wishes,
urs