Contents

# 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

The $n$-sphere type is be defined as the suspension type of the $(n-1)$-sphere type or the iterated suspension of $S^0 := \mathbf{2}$. (a.k.a $\text{Bool}$).

$S^n := \Sigma^n S^0$