Showing changes from revision #0 to #1:
Added | Removed | Changed
Cohesive homotopy type theory is a two-sorted dependent type theory of spaces and homotopy types, where there exist judgments
for spaces
for homotopy types
for points
for terms
for indexed spaces
for dependent types
for path spaces
for identity types
for mapping spaces
for function types
Cohesive homotopy type theory has the following additional judgments, 2 for turning spaces into homotopy types and the other two for turning homotopy types into spaces:
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
The underlying homotopy type and fundamental homotopy type are sometimes represented by the greek letters and respectively, but both are already used in dependent type theory to represent the context and the dependent/indexed product.
From these judgements one could construct the sharpmodality? as