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

For instance a smooth 0-type is then an object in the sheaf topos Sh(CartSp)Sh (CartSp)HSh(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)