# nLab sphere type

Contents

### Context

#### Spheres

n-sphere

low dimensional n-spheres

# Contents

## Idea

Sphere types are the axiomatization of the homotopy type of the (shape of) the spheres in the context of homotopy type theory.

## Definition

For $n = 0$, the 0-sphere-type is defined to the boolean domain $\mathbf{2}$ (or “Bit”, see there):

(1)$S^0 \,\coloneqq\, \mathbf{2} \,.$

By induction on the natural number $n$: For $n \geq 1$, the $n$-sphere type is be defined as

• the (un-reduced) suspension type $\mathrm{S}(-)$ of the $(n-1)$-sphere type $S^{n-1}$;

or equivalently

• the $n$-fold iterated suspension type $\mathrm{S}^n(-)$ of $S^0$ (1):
$S^n \;\coloneqq\; \mathrm{S} S^{n-1} \;=\; \mathrm{S}^n S^0 \,.$