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