Showing changes from revision #9 to #10:
Added  Removed  Changed
Contents
Overview
Cohesive homotopy type theory is a twosorted dependent type theory of spaces and homotopy types, where there exist judgments

for spaces
$\frac{\Gamma}{\Gamma \vdash S\ space}$

for homotopy types
$\frac{\Gamma}{\Gamma \vdash T\ homotopy\ type}$

for points
$\frac{\Gamma \vdash S\ space}{\Gamma \vdash s:S}$

for terms
$\frac{\Gamma \vdash T\ homotopy\ type}{\Gamma \vdash t:T}$

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

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

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

for dependent terms
$\frac{\Gamma \vdash T\ homotopy\ type}{\Gamma, t:T \vdash b(t):B(t)}$
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{\Gamma \vdash S\ space}{\Gamma \vdash p_*(S)\ homotopy\ type}$

Every space has a fundamental homotopy type
$\frac{\Gamma \vdash S\ space}{\Gamma \vdash p_!(S)\ homotopy\ type}$

Every homotopy type has a discrete space
$\frac{\Gamma \vdash T\ homotopy\ type}{\Gamma \vdash p^*(T)\ space}$

Every homotopy type has an indiscrete space
$\frac{\Gamma \vdash T\ homotopy\ type}{\Gamma \vdash 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.
Modalities
From these judgements one could construct the sharp? modality? as
$\sharp(S) \coloneqq p^!(p_*(S))$
the flat? modality as
$\flat(S) \coloneqq p^*(p_*(S))$
and the shape modality as
$\esh(S) \coloneqq p^*(p_!(S))$
for a space $S$.
Other types
Path spaces
$\frac{\Gamma, a:S, b:S}{\Gamma \vdash a =_S b\ space}$
Identity types
$\frac{\Gamma, a:T, b:T}{\Gamma \vdash a =_T b\ homotopy\ type}$
Mapping spaces
$\frac{\Gamma, A\ space, B\ space}{\Gamma \vdash A \to B\ space}$
Function types
$\frac{\Gamma, A\ homotopy\ type, B\ homotopy\ type}{\Gamma \vdash A \to B\ homotopy\ type}$
Section spaces
$\frac{\Gamma, s:S \vdash A(s)\ space}{\Gamma \vdash \prod_{s:S} A(s)\ space}$
Dependent function types
$\frac{\Gamma, t:T \vdash A(t)\ homotopy\ type}{\Gamma \vdash \prod_{t:T} A(t)\ homotopy\ type}$
Product spaces
$\frac{\Gamma, A\ space, B\ space}{\Gamma \vdash A \times B\ space}$
Pair types
$\frac{\Gamma, A\ homotopy\ type, B\ homotopy\ type}{\Gamma \vdash A \times B\ homotopy\ type}$
Total spaces
$\frac{\Gamma, s:S \vdash A(s)\ space}{\Gamma \vdash \sum_{s:S} A(s)\ space}$
Dependent pair types
$\frac{\Gamma, t:T \vdash A(t)\ homotopy\ type}{\Gamma \vdash \sum_{t:T} A(t)\ homotopy\ type}$
Unit space
$\frac{\Gamma}{\Gamma \vdash \mathbb{1}\ space}$
Unit type
$\frac{\Gamma}{\Gamma \vdash \mathbb{1}\ homotopy\ type}$
Other properties
The fundamental homotopy type of the unit space is equivalent to the unit type.
$p_!(\mathbb{1}) \cong \mathbb{1}$
The product of the fundamental homotopy types of spaces $A$ and $B$ is equivalent to the fundamental homotopy type of the product of spaces $A$ and $B$:
$p_!(A \times B) \cong p_!(A) \times p_!(B)$