Backround
Definition
Presentation over a site
Models
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
By cohesive homotopy theory we mean homotopy theory equipped with structure/axioms of cohesion:
While bare homotopy theory is concerned (just) with geometrically discrete homotopy types/$\infty$-groupoids,
and while geometric homotopy theory ($\infty$-topos theory) generalizes this to “geometric homotopy types” ($\infty$-stacks) for extremely general notions of “geometry”,
cohesive homotopy theory is a form of geometric homotopy theory but constrained such that the notion of geometry it encodes satisfies basic properties familiar from differential topology and differential cohomology-theory.
Semantically, cohesive homotopy theory is modeled by cohesive $\infty$-toposes, while syntactically it is described by cohesive homotopy type theory.
Or rather, all this pertains to the default notion of “cohesion”. There are further enhancements such as to differential cohesion modeled by differential cohesive $\infty$-toposes, which reflects a richer notion of higher synthetic differential geometry.
See the references at
Created on January 2, 2023 at 12:15:33. See the history of this page for a list of all contributions to it.