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 $H$ which models cohesive homotopy type theory for a kind of smooth cohesion – such as $H=$ Smooth∞Grpd – as a smooth type. Or smooth homotopy type. Accordingly then an n-truncated object in $H$ is a smooth $n$-type.

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