nLab differential homotopy type theory

Idea

under construction

Context

Cohesive $\infty$-Toposes

cohesive topos

cohesive (∞,1)-topos

cohesive homotopy type theory

Structures in a cohesive $(\infty,1)$-topos

structures in a cohesive (∞,1)-topos

Structures with infinitesimal cohesion

infinitesimal cohesion?

Idea

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

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

called

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

Last revised on August 30, 2017 at 10:09:42. See the history of this page for a list of all contributions to it.