$\,$
This page collects material related to this thesis that I once advised:
Formalizing Cartan Geometry in Modal Homotopy Type Theory
PhD Thesis, KIT 2017
(thesis pdf, achived version: web, talk slides: pdf, HoTT-Agda code: DCHoTT-Agda.
on higher Cartan geometry formalized in modal homotopy type theory.
$\,$
This thesis implements a fragment of the axioms of differential cohesion (Schreiber 13) for synthetic differential geometry, formalized in homotopy type theory and implemented in the Agda proof management system:
A modal operator is introduced (see Schreiber 15 for exposition) which is interpreted as an “infinitesimal shape” modality $\Im$. For $X$ any homotopy type then the standard interpretation of the type $\Im X$ is the result of “identifying infinitesimally close points in $X$”.
(By synthetic PDE theory (Khavkine-Schreiber 17) the dependent types over $\Im X$ have the interpretation of being partial differential equations with free variables ranging in $X$. The linear dependent types over $\Im X$ are also known as D-modules, as used in geometric representation theory.)
Using this infinitesimal shape modality $\Im$ 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$ (Schreiber 13).
The main theorem of the thesis shows that the infinitesimal disk bundle of any such manifold $X$ is a fiber ∞-bundle which is associated to a principal ∞-bundle (Nikolaus-Schreiber-Stevenson 12): its frame bundle.
This solves the first of the three problems in modal type theory that had been posed in
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
For more exposition see also at Formalizing Cartan Geometry in Modal HoTT.
For further development concerning jet bundles and PDEs, see
$\,$
$\,$