Homotopy Type Theory cohesive homotopy type theory > history (Rev #1)

Cohesive homotopy type theory is a two-sorted dependent type theory of spaces and homotopy types, where there exist judgments

• for spaces

  $$\frac{\Gamma}{\Gamma, S\ space}$$

• for homotopy types

  $$\frac{\Gamma}{\Gamma, T\ homotopy\ type}$$

• for points

  $$\frac{\Gamma, S\ space}{\Gamma, s:S}$$

• for terms

  $$\frac{\Gamma, T\ homotopy\ type}{\Gamma, t:T}$$

• for indexed spaces

  $$\frac{\Gamma, S\ space}{\Gamma, s:S \vdash A(s)\ space}$$

• for dependent types

  $$\frac{\Gamma, T\ homotopy\ type}{\Gamma, t:T \vdash B(t)\ homotopy\ type}$$

• for path spaces

  $$\frac{\Gamma, a:S, b:S}{\Gamma, a =_S b\ space}$$

• for identity types

  $$\frac{\Gamma, a:T, b:T}{\Gamma, a =_T b\ homotopy\ type}$$

• for mapping spaces

  $$\frac{\Gamma, A\ space, B\ space}{\Gamma, A \to B\ space}$$

• for function types

  $$\frac{\Gamma, A\ homotopy\ type, B\ homotopy\ type}{\Gamma, A \to B\ homotopy\ type}$$

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

  $$\frac{S\ space}{p_*(S)\ homotopy\ type}$$

• Every space has a fundamental homotopy type

  $$\frac{S\ space}{p_!(S)\ homotopy\ type}$$

• Every homotopy type has a discrete space

  $$\frac{T\ homotopy\ type}{p^*(T)\ space}$$

• Every homotopy type has an indiscrete space

  $$\frac{T\ homotopy\ type}{p^!(T)\ space}$$

The underlying homotopy type and fundamental homotopy type are sometimes represented by the greek letters $\Gamma$ and $\Pi$ 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 sharp modality? as

the flat modality as

and the shape modality as

for a space $S$.

See also

• Topology