differential homotopy type theory

> under construction

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** = **propositions as types** +**programs as proofs** +**relation type theory/category theory**

**structures in a cohesive (∞,1)-topos**

**infinitesimal cohesion?**

*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

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

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.

Revised on August 30, 2017 10:09:42
by Max S. New
(129.10.110.48)