Homotopy Type Theory differential cohesive homotopy type theory > history (Rev #5, changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

Contents

< differential cohesive homotopy type theory

Overview

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

    ΓΓSspace\frac{\Gamma}{\Gamma \vdash S\ space}
  • for infinitesimal neighborhoods

    ΓΓIinfinitesimalneighborhood\frac{\Gamma}{\Gamma \vdash I\ infinitesimal\ neighborhood}
  • for homotopy types

    ΓΓThomotopytype\frac{\Gamma}{\Gamma \vdash T\ homotopy\ type}
  • for points

    ΓSspaceΓs:S\frac{\Gamma \vdash S\ space}{\Gamma \vdash s:S}
  • for infinitesimals

    ΓIinfinitesimalneighborhoodΓi:I\frac{\Gamma \vdash I\ infinitesimal\ neighborhood}{\Gamma \vdash i:I}
  • for terms

    ΓThomotopytypeΓt:T\frac{\Gamma \vdash T\ homotopy\ type}{\Gamma \vdash t:T}
  • for fibrations

    ΓSspaceΓ,s:SA(s)space\frac{\Gamma \vdash S\ space}{\Gamma, s:S \vdash A(s)\ space}
  • for infinitesimal fibrations

    ΓIinfinitesimalneighborhoodΓi:IA(i)infinitesimalneighborhood\frac{\Gamma \vdash I\ infinitesimal\ neighborhood}{\Gamma i:I\vdash A(i)\ infinitesimal\ neighborhood}
  • for dependent types

    ΓThomotopytypeΓ,t:TB(t)homotopytype\frac{\Gamma \vdash T\ homotopy\ type}{\Gamma, t:T \vdash B(t)\ homotopy\ type}
  • for sections

    ΓSspaceΓ,s:Sa(s):A(s)\frac{\Gamma \vdash S\ space}{\Gamma, s:S \vdash a(s):A(s)}
  • for infinitesimal sections

    ΓIinfinitesimalneighborhoodΓi:Ia(i):A(i)\frac{\Gamma \vdash I\ infinitesimal\ neighborhood}{\Gamma i:I\vdash a(i):A(i)}
  • for dependent terms

    ΓThomotopytypeΓ,t:Tb(t):B(t)\frac{\Gamma \vdash T\ homotopy\ type}{\Gamma, t:T \vdash b(t):B(t)}

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

    ΓSspaceΓp *(S)homotopytype\frac{\Gamma \vdash S\ space}{\Gamma \vdash p_*(S)\ homotopy\ type}
  • Every space has a fundamental homotopy type

    ΓSspaceΓp !(S)homotopytype\frac{\Gamma \vdash S\ space}{\Gamma \vdash p_!(S)\ homotopy\ type}
  • Every homotopy type has a discrete space

    ΓThomotopytypeΓp *(T)space\frac{\Gamma \vdash T\ homotopy\ type}{\Gamma \vdash p^*(T)\ space}
  • Every homotopy type has an indiscrete space

    ΓThomotopytypeΓp !(T)space\frac{\Gamma \vdash T\ homotopy\ type}{\Gamma \vdash p^!(T)\ space}
  • Every infinitesimal neighborhood has an underlying homotopy type

    ΓIinfinitesimalneighborhoodΓq *(I)homotopytype\frac{\Gamma \vdash I\ infinitesimal\ neighborhood}{\Gamma \vdash q_*(I)\ homotopy\ type}
  • Every infinitesimal neighborhood has a fundamental homotopy type

    ΓIinfinitesimalneighborhoodΓq !(I)homotopytype\frac{\Gamma \vdash I\ infinitesimal\ neighborhood}{\Gamma \vdash q_!(I)\ homotopy\ type}
  • Every homotopy type has a discrete infinitesimal neighborhood

    ΓThomotopytypeΓq *(T)infinitesimalneighborhood\frac{\Gamma \vdash T\ homotopy\ type}{\Gamma \vdash q^*(T)\ infinitesimal\ neighborhood}
  • Every homotopy type has an indiscrete infinitesimal neighborhood

    ΓThomotopytypeΓq !(T)infinitesimalneighborhood\frac{\Gamma \vdash T\ homotopy\ type}{\Gamma \vdash q^!(T)\ infinitesimal\ neighborhood}

I am not sure what the official names of these functors are:

  • Every space has an infinitesimal neighborhood

    ΓSspaceΓi *(S)infinitesimalneighborhood\frac{\Gamma \vdash S\ space}{\Gamma \vdash i_*(S)\ infinitesimal\ neighborhood}
  • Every space has an infinitesimal neighborhood

    ΓSshapeΓi !(S)infinitesimalneighborhood\frac{\Gamma \vdash S\ shape}{\Gamma \vdash i_!(S)\ infinitesimal\ neighborhood}
  • Every infinitesimal neighborhood has a space whereby that infinitesimal neighborhood is contracted away.

    ΓIinfinitesimalneighborhoodΓi *(I)space\frac{\Gamma \vdash I\ infinitesimal\ neighborhood}{\Gamma \vdash i^*(I)\ space}
  • Every infinitesimal neighborhood has a space

    ΓIinfinitesimalneighborhoodΓi !(I)space\frac{\Gamma \vdash I\ infinitesimal\ neighborhood}{\Gamma \vdash i^!(I)\ space}

Modalities

From these judgements one could construct the reduction modality? as

(S)i !(i *(S))\mathfrak{R}(S) \coloneqq i_!(i^*(S))

the infinitesimal shape modality as

𝔍(S)i *(i *(S))\mathfrak{J}(S) \coloneqq i_*(i^*(S))

and the infinitesimal flat? modality as

&(S)i *(i !(S))\&(S) \coloneqq i_*(i^!(S))

for a space SS.

See also

Revision on June 18, 2022 at 20:32:01 by Anonymous?. See the history of this page for a list of all contributions to it.