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:

$Red \dashv ʃ_{inf} \dashv \flat_{inf}$

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 January 5, 2013 22:15:56
by Urs Schreiber
(89.204.138.93)