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
Backround
Definition
Presentation over a site
Models
Differential cohesive homotopy type theory or elastic homotopy type theory is the (hypothetical) modal type theory obtained by adding to cohesive homotopy type theory an adjoint triple of idempotent (co)monadic modalities:
called
(Also called elastic homotopy theory $[$SS20, §3.1.2$]$, see at geometry of physics – categories and toposes the sections on elastic toposes and elastic $\infty$-toposes.)
By the discussion at cohesive (infinity,1)-topos – infinitesimal cohesion this language can express at least the following notions
No full formalization of such a type theory currently exists, and how to design such a theory is an open question in modal type theory.
Some work has been done on synthetic differential geometry in modal homotopy type theory.
Felix Cherubini (Cherubini18) has formalized some synthetic differential geometry using an abstract infinitesimal shape modality working in plain homotopy type theory.
David Jaz Myers (JazMyers22) formalized a synthetic theory of orbifolds working in a type theory extending cohesive homotopy type theory with axioms such as the Kock-Lawvere axiom to axiomatize the notion of infinitesimals and defines the infinitesimal shape modality and shape modality as localizations at the infinitesimals and reals respectively.
Felix Cherubini, Cartan Geometry in Modal Homotopy Type Theory, (arXiv:1806.05966)
David Jaz Myers, Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory (arXiv:2205.15887)
Last revised on December 5, 2022 at 05:05:17. See the history of this page for a list of all contributions to it.