Schreiber thesis Wellen


This page collects material related to this thesis that I once advised:

on basics of differential geometry (smooth manifolds and G-structures) generalized to higher Cartan geometry and formalized in modal homotopy type theory (modal homotopy type theory, cohesive 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 shapemodality \Im. For XX any homotopy type then the standard interpretation of the type X\Im X is the result of “identifying infinitesimally close points in XX”.

(By synthetic PDE theory (Khavkine-Schreiber 17) the dependent types over X\Im X have the interpretation of being partial differential equations with free variables ranging in XX. The linear dependent types over X\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 XX (Schreiber 13).

The main theorem of the thesis shows that the infinitesimal disk bundle of any such manifold XX 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 XX with torsion-free G-structure means to equip XX with a flavor of geometry, depending on the choice of GG, such as (pseudo-)Riemannian geometry, conformal geometry, complex geometry, symplectic geometry etc. pp. The moduli stacks of all given GG-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) GG-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 exposition see

and tutorial 6 in:

  • Dan Licata, Felix Wellen, Synthetic Mathematics in Modal Dependent Type Theories, tutorial at Types, Homotopy Theory and Verification (2018)

    Tutorial 1, Dan Licata: A Fibrational Framework for Modal Simple Type Theories (recording)

    Tutorial 2, Felix Wellen: The Shape Modality in Real cohesive HoTT and Covering Spaces (recording)

    Tutorial 3, Dan Licata: Discrete and Codiscrete Modalities in Cohesive HoTT (recording)

    Tutorial 4, Felix Wellen, Discrete and Codiscrete Modalities in Cohesive HoTT, II (recording)

    Tutorial 5, Dan Licata: A Fibrational Framework for Modal Dependent Type Theories (recording)

    Tutorial 6, Felix Wellen: Differential Cohesive HoTT, (recording)


    Dan Licata, Synthetic Mathematics in Modal Dependent Type Theories, notes for tutorial at Types, Homotopy Theory and Verification, 2018 (pdf)



For more exposition see also at Formalizing Cartan Geometry in Modal HoTT and at geometry of physics – manifolds and orbifolds.

For more higher differential geometry-background see

For further development concerning jet bundles and PDEs, see



Last revised on June 18, 2022 at 08:46:02. See the history of this page for a list of all contributions to it.