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
Modalities
From these judgements one could construct the reductionmodality? as