Showing changes from revision #1 to #2: 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

  $$\frac{\Gamma }{\Gamma <span><del\; class="diffmod">\; ,</del><ins\; class="diffmod">\; ⊢</ins></span>S\mathrm{space}}$$ \frac{\Gamma}{\Gamma, \frac{\Gamma}{\Gamma \vdash S\ space}

• for homotopy types

  $$\frac{\Gamma }{\Gamma <span><del\; class="diffmod">\; ,</del><ins\; class="diffmod">\; ⊢</ins></span>T\mathrm{homotopy}\mathrm{type}}$$ \frac{\Gamma}{\Gamma, \frac{\Gamma}{\Gamma \vdash T\ homotopy\ type}

• for points

  $$\frac{\Gamma <span><del\; class="diffmod">\; ,</del><ins\; class="diffmod">\; ⊢</ins></span>S\mathrm{space}}{\Gamma <span><del\; class="diffmod">\; ,</del><ins\; class="diffmod">\; ⊢</ins></span>s:S}$$ \frac{\Gamma, \frac{\Gamma \vdash S\ space}{\Gamma, space}{\Gamma \vdash s:S}

• for terms

  $$\frac{\Gamma <span><del\; class="diffmod">\; ,</del><ins\; class="diffmod">\; ⊢</ins></span>T\mathrm{homotopy}\mathrm{type}}{\Gamma <span><del\; class="diffmod">\; ,</del><ins\; class="diffmod">\; ⊢</ins></span>t:T}$$ \frac{\Gamma, \frac{\Gamma \vdash T\ homotopy\ type}{\Gamma, type}{\Gamma \vdash t:T}

• for indexed fibrations spaces

  $$\frac{\Gamma <span><del\; class="diffmod">\; ,</del><ins\; class="diffmod">\; ⊢</ins></span>S\mathrm{space}}{\Gamma ,s:S⊢A(s)\mathrm{space}}$$ \frac{\Gamma, \frac{\Gamma \vdash S\ space}{\Gamma, s:S \vdash A(s)\ space}

• for dependent types

  $$\frac{\Gamma <span><del\; class="diffmod">\; ,</del><ins\; class="diffmod">\; ⊢</ins></span>T\mathrm{homotopy}\mathrm{type}}{\Gamma ,t:T⊢B(t)\mathrm{homotopy}\mathrm{type}}$$ \frac{\Gamma, \frac{\Gamma \vdash T\ homotopy\ type}{\Gamma, t:T \vdash B(t)\ homotopy\ type}

• for path sections spaces

  $$\frac{\Gamma <span><del\; class="diffmod">\; ,</del><ins\; class="diffmod">\; ⊢</ins></span>a:S,\mathrm{<span><del\; class="diffmod">\; b</del><ins\; class="diffmod">\; space</ins></span>}:S}{\Gamma ,s:S⊢a{=}_S(\mathrm{<span><del\; class="diffmod">\; b</del><ins\; class="diffmod">\; s</ins></span>})\mathrm{space}:A(s)}$$ \frac{\Gamma, \frac{\Gamma a:S, \vdash b:S}{\Gamma, S\ a space}{\Gamma, =_S s:S b\ \vdash space} a(s):A(s)}

• for identity dependent types terms

  $$\frac{\Gamma <span><del\; class="diffmod">\; ,</del><ins\; class="diffmod">\; ⊢</ins></span>a:T,\mathrm{<span><del\; class="diffmod">\; b</del><ins\; class="diffmod">\; homotopy</ins></span>}:\mathrm{<span><del\; class="diffmod">\; T</del><ins\; class="diffmod">\; type</ins></span>}}{\Gamma ,\mathrm{<span><del\; class="diffmod">\; a</del><ins\; class="diffmod">\; t</ins></span>}{=}_T:T⊢b(\mathrm{<span><del\; class="diffmod">\; homotopy</del><ins\; class="diffmod">\; t</ins></span>})\mathrm{type}:B(t)}$$ \frac{\Gamma, \frac{\Gamma a:T, \vdash b:T}{\Gamma, T\ a =_T b\ homotopy\ type} type}{\Gamma, t:T \vdash b(t):B(t)}

• 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{\Gamma ⊢S\mathrm{space}}{\Gamma ⊢p_{*}(S)\mathrm{homotopy}\mathrm{type}}$$ \frac{S\ \frac{\Gamma space}{p_*(S)\ \vdash S\ space}{\Gamma \vdash p_*(S)\ homotopy\ type}

• Every space has a fundamental homotopy type

  $$\frac{\Gamma ⊢S\mathrm{space}}{\Gamma ⊢p_{!}(S)\mathrm{homotopy}\mathrm{type}}$$ \frac{S\ \frac{\Gamma space}{p_!(S)\ \vdash S\ space}{\Gamma \vdash p_!(S)\ homotopy\ type}

• Every homotopy type has a discrete space

  $$\frac{\Gamma ⊢T\mathrm{homotopy}\mathrm{type}}{\Gamma ⊢p^{*}(T)\mathrm{space}}$$ \frac{T\ \frac{\Gamma \vdash T\ homotopy\ type}{p^*(T)\ type}{\Gamma \vdash p^*(T)\ space}

• Every homotopy type has an indiscrete space

  $$\frac{\Gamma ⊢T\mathrm{homotopy}\mathrm{type}}{\Gamma ⊢p^{!}(T)\mathrm{space}}$$ \frac{T\ \frac{\Gamma \vdash T\ homotopy\ type}{p^!(T)\ 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.