nLab
smooth homotopy type

Context

Differential geometry

differential geometry

synthetic differential geometry

Axiomatics

Models

Concepts

Theorems

Applications

Cohesive \infty-Toposes

cohesive topos

cohesive (∞,1)-topos

cohesive homotopy type theory

Backround

Definition

Presentation over a site

Structures in a cohesive (,1)(\infty,1)-topos

structures in a cohesive (∞,1)-topos

Structures with infinitesimal cohesion

infinitesimal cohesion?

Models

Contents

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 a cohesive (∞,1)-topos H\mathbf{H} such as as Smooth∞Grpd as a smooth homotopy type or smooth infinity-groupoid. 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} of smooth sets.

References

Revised on November 6, 2014 07:58:13 by Urs Schreiber (89.92.25.218)