[[!redirects space]] [[!redirects homotopy type]] [[!redirects indexed space]] [[!redirects indexed homotopy type]] [[!redirects shape]] 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, S\ space}$$ * for __homotopy types__ $$\frac{\Gamma}{\Gamma, T\ homotopy\ type}$$ * for __points__ $$\frac{\Gamma, S\ space}{\Gamma, s:S}$$ * for __terms__ $$\frac{\Gamma, T\ homotopy\ type}{\Gamma, t:T}$$ * for __indexed spaces__ $$\frac{\Gamma, S\ space}{\Gamma, s:S \vdash A(s)\ space}$$ * for __dependent types__ $$\frac{\Gamma, T\ homotopy\ type}{\Gamma, t:T \vdash B(t)\ homotopy\ type}$$ * for __path spaces__ $$\frac{\Gamma, a:S, b:S}{\Gamma, a =_S b\ space}$$ * for __identity types__ $$\frac{\Gamma, a:T, b:T}{\Gamma, a =_T b\ homotopy\ type}$$ * 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{S\ space}{p_*(S)\ homotopy\ type}$$ * Every space has a __fundamental homotopy type__ $$\frac{S\ space}{p_!(S)\ homotopy\ type}$$ * Every homotopy type has a __discrete space__ $$\frac{T\ homotopy\ type}{p^*(T)\ space}$$ * Every homotopy type has an __indiscrete space__ $$\frac{T\ homotopy\ type}{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. 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$. ## See also ## * [[Topology]]