# nLab smooth homotopy type

## Idea

In view of the congruence of the notions of homotopy type and type in homotopy type theory it makes sense to refer to an object in an cohesive (∞,1)-topos $\mathbf{H}$ which models cohesive homotopy type theory for a kind of smooth cohesion – such as $\mathbf{H} =$ Smooth∞Grpd – as a smooth type. Or smooth homotopy type. Accordingly then an n-truncated object in $\mathbf{H}$ is a smooth $n$-type.

For instance a smooth 0-type is then an object in the sheaf topos $Sh(CartSp) \hookrightarrow Sh_\infty(CartSp) \simeq \mathbf{H}$. (Also sometumes called a smooth space.)

Revised on May 4, 2013 20:37:42 by Urs Schreiber (150.212.92.50)