Homotopy Type Theory differential cohesive homotopy type theory > history (changes)

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

Contents

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

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

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

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

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

$\frac{\Gamma \vdash I\ infinitesimal\ neighborhood}{\Gamma \vdash i:I}$
• 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 infinitesimal fibrations

$\frac{\Gamma \vdash I\ infinitesimal\ neighborhood}{\Gamma i:I\vdash A(i)\ infinitesimal\ neighborhood}$
• 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 infinitesimal sections

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

$\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

$\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}$
• Every infinitesimal neighborhood has an underlying homotopy type

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

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

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

$\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

$\frac{\Gamma \vdash S\ space}{\Gamma \vdash i_*(S)\ infinitesimal\ neighborhood}$
• Every space has an infinitesimal neighborhood

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

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

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

Modalities

From these judgements one could construct the reduction modality? as

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

the infinitesimal shape modality as

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

and the infinitesimal flat? modality as

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

for a space $S$.