Showing changes from revision #4 to #5:
Added | Removed | Changed
< differential cohesive homotopy type theory
Differential cohesive homotopy type theory is a three-sorted dependent type theory of spaces, infinitesimal neighborhoods, and homotopy types, where there exist judgments
for spaces
for infinitesimal neighborhoods
for homotopy types
for points
for infinitesimals
for terms
for fibrations
for infinitesimal fibrations
for dependent types
for sections
for infinitesimal sections
for dependent terms
Differential cohesive homotopy type theory has the following additional judgments, two for turning spaces into homotopy types, two for turning homotopy types into spaces, two for turning infinitesimal neighborhoods into homotopy types, two for turning homotopy types into infinitesimal neighborhoods, two for turning infinitesimal neighborhoods into spaces, and two for turning spaces into infinitesimal neighborhoods:
Every space has an underlying homotopy type
Every space has a fundamental homotopy type
Every homotopy type has a discrete space
Every homotopy type has an indiscrete space
Every infinitesimal neighborhood has an underlying homotopy type
Every infinitesimal neighborhood has a fundamental homotopy type
Every homotopy type has a discrete infinitesimal neighborhood
Every homotopy type has an indiscrete infinitesimal neighborhood
I am not sure what the official names of these functors are:
Every space has an infinitesimal neighborhood
Every space has an infinitesimal neighborhood
Every infinitesimal neighborhood has a space whereby that infinitesimal neighborhood is contracted away.
Every infinitesimal neighborhood has a space
From these judgements one could construct the reduction modality? as
the infinitesimal shape modality as
and the infinitesimal flat? modality as
for a space $S$.
Last revised on June 18, 2022 at 20:32:01. See the history of this page for a list of all contributions to it.