nLab differential cohesive homotopy type theory

under construction

Idea

Differential cohesive homotopy type theory or elastic homotopy type theory is the (hypothetical) modal type theory obtained by adding to cohesive homotopy type theory an adjoint triple of idempotent (co)monadic modalities:

$$\Re \dashv \Im \dashv \&$$

called

• reduction modality$\dashv$ infinitesimal shape modality $\dashv$ infinitesimal flat modality.

(Also called elastic homotopy theory $[$SS20, §3.1.2$]$, see at geometry of physics – categories and toposes the sections on elastic toposes and elastic $\infty$-toposes.)

By the discussion at cohesive (infinity,1)-topos – infinitesimal cohesion this language can express at least the following notions

• reduced type, infinitesimal path ∞-groupoid, de Rham space, jet bundle, D-geometry, ∞-Lie algebra (synthetically), Lie differentiation, hence “Formal Moduli Problems and DG-Lie Algebras” , formally etale morphism, formally smooth morphism, formally unramified morphism, smooth etale ∞-groupoid?, hence ∞-orbifold? etc.

No full formalization of such a type theory currently exists, and how to design such a theory is an open question in modal type theory.

Partial Realizations

Some work has been done on synthetic differential geometry in modal homotopy type theory.

Felix Cherubini (Cherubini18) has formalized some synthetic differential geometry using an abstract infinitesimal shape modality working in plain homotopy type theory.

David Jaz Myers (JazMyers22) formalized a synthetic theory of orbifolds working in a type theory extending cohesive homotopy type theory with axioms such as the Kock-Lawvere axiom to axiomatize the notion of infinitesimals and defines the infinitesimal shape modality and shape modality as localizations at the infinitesimals and reals respectively.

Related concepts

• cohesive homotopy type theory

• super homotopy type theory

• differential cohesive (infinity,1)-topos

• differential geometry

References

• Felix Cherubini, Cartan Geometry in Modal Homotopy Type Theory, (arXiv:1806.05966)

• David Jaz Myers, Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory (arXiv:2205.15887)