#Contents# * table of contents {:toc} ## 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$. ## See also ## * [[cohesive homotopy type theory]] category: not redirected to nlab yet