nLab differential homotopy type theory

under construction

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 June 15, 2021 at 19:32:07. See the history of this page for a list of all contributions to it.