# nLab differential cohesive homotopy type theory

Contents

under construction

# Contents

## 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

(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

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.

## References

Last revised on December 5, 2022 at 05:05:17. See the history of this page for a list of all contributions to it.